From 3aca640eaf8cb10d473c64bd1ee7c462ab2236f4 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 1 Nov 2019 20:13:36 +0000
Subject: More work on GDB interface

The following now works to run sail on every HVC call with hafnium

function gdb_init() -> unit = {
  // Connect to QEMU via GDB
  sail_gdb_qemu("");
  sail_gdb_symbol_file("hafnium.elf.sym");
  sail_gdb_send("break-insert sync_lower_exception")
}

function gdb() -> unit = {
  gdb_init();
  while true do {
    sail_gdb_send("exec-continue");
    sail_gdb_sync()
  }
}
---
 doc/Makefile     | 7 ++++++-
 doc/internals.md | 8 ++++----
 doc/manual.tex   | 3 +++
 3 files changed, 13 insertions(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/Makefile b/doc/Makefile
index 5ec1f10b..315eaaaa 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -69,8 +69,12 @@ code_myreplicatebits.tex: examples/my_replicate_bits.sail
 grammar.tex: ../language/sail.ott
 	ott -pp_grammar -tex_wrap false -tex_suppress_category I -tex_suppress_category D -tex_suppress_ntr terminals -tex_suppress_ntr formula -tex_suppress_ntr judgement -tex_suppress_ntr user_syntax -tex_suppress_ntr dec_comm -sort false -generate_aux_rules false  -picky_multiple_parses true -i ../language/sail.ott -o grammar.tex
 
+internals.tex: internals.md
+	pandoc $< -f markdown -t latex --listings -o $@
+	sed -i.bak -f pandocfix.sed $@
+
 LATEXARG=manual.tex
-manual.pdf: grammar.tex introduction.tex usage.tex types.tex code_riscv.tex riscv.tex manual.tex manual.bib tutorial.tex code_myreplicatebits.tex
+manual.pdf: grammar.tex introduction.tex usage.tex types.tex code_riscv.tex riscv.tex manual.tex manual.bib tutorial.tex internals.tex code_myreplicatebits.tex
 	pdflatex ${LATEXARG}
 	bibtex manual
 	pdflatex ${LATEXARG}
@@ -83,6 +87,7 @@ clean:
 	-rm manual.pdf
 	-rm -rf code_riscv/
 	-rm -f code_riscv.tex
+	-rm -f internals.tex
 	-rm -rf code_myreplicatebits/
 	-rm -f code_myreplicatebits.tex
 	-rm -f *.aux
diff --git a/doc/internals.md b/doc/internals.md
index 6ba60fa6..6422f227 100644
--- a/doc/internals.md
+++ b/doc/internals.md
@@ -10,7 +10,7 @@ by [Lem](https://github.com/rems-project/lem), which allows the Sail
 OCaml source to seamlessly interoperate with parts written in
 Lem. Although we do not make much use of this, in principle it allows
 us to implement parts of Sail in Lem, which would enable them to be
-verified in Isabelle or HOL.
+verified in Isabelle or HOL4.
 
 The Sail AST looks something like:
 
@@ -35,13 +35,13 @@ which attaches an annotation to each node in the AST, consisting of an
 arbitrary type that parameterises the AST, and a location identifying
 the position of the AST node in the source code:
 
-```
+```OCaml
 type 'a annot = l * 'a
 ```
 
 There are various types of locations:
 
-```
+```OCaml
 type l =
   | Unknown
   | Unique of int * l
@@ -184,7 +184,7 @@ which invokes the backend for each target, e.g. for OCaml:
 ```
 
 There is also a `Sail.prover_regstate` function that allows the
-register state to be Set up in a prover-agnostic way for each of the
+register state to be set up in a prover-agnostic way for each of the
 theorem-prover targets.
 
 ## Type Checker
diff --git a/doc/manual.tex b/doc/manual.tex
index 38b14322..f3578784 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -105,6 +105,9 @@
 
 \include{tutorial}
 
+\lstset{language={},escapechar=\`}
+\include{internals}
+
 % Remove for now since incomplete
 %\include{types}
 
-- 
cgit v1.2.3