Support building an anonymised version of manual. Fix sail example in manual. Remove incomplete types chapter from manual per AA's recommendation.

5 files changed, 33 insertions, 7 deletions

diff --git a/Makefile b/Makefile
index bfbf6bef..9a6dd42a 100644
--- a/Makefile
+++ b/Makefile
@@ -53,6 +53,17 @@ apply_header:
 	headache -c etc/headache_config -h LICENCE `ls src/lem_interp/*.lem`
 	$(MAKE) -C arm apply_header
 
+anon_dist:
+	$(MAKE) clean
+	headache -c etc/headache_config -h etc/anon_header `ls mips/*.sail`
+	headache -c etc/headache_config -h etc/anon_header `ls cheri/*.sail`
+	headache -c etc/headache_config -h etc/anon_header `ls src/Makefile*`
+	headache -c etc/headache_config -h etc/anon_header `ls src/*.ml*`
+	headache -c etc/headache_config -h etc/anon_header `ls src/lem_interp/*.ml`
+	headache -c etc/headache_config -h etc/anon_header `ls src/lem_interp/*.lem`
+	headache -c etc/headache_config -h etc/anon_header `ls arm/*.sail`
+	tar cvzf sail.tar.gz .
+
 clean:
 	for subdir in src arm ; do\
 	  $(MAKE) -C "$$subdir" clean;\
diff --git a/doc/Makefile b/doc/Makefile
index b5a74dd6..ae542571 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -65,11 +65,15 @@ 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
 
+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
-	pdflatex manual.tex
+	pdflatex ${LATEXARG}
 	bibtex manual
-	pdflatex manual.tex
-	pdflatex manual.tex
+	pdflatex ${LATEXARG}
+	pdflatex ${LATEXARG}
+
+anon_man: LATEXARG='\def\ANON{}\input{manual.tex}'
+anon_man: manual.pdf
 
 clean:
 	-rm manual.pdf
diff --git a/doc/examples/my_replicate_bits.sail b/doc/examples/my_replicate_bits.sail
index c9972cd6..8c3c9458 100644
--- a/doc/examples/my_replicate_bits.sail
+++ b/doc/examples/my_replicate_bits.sail
@@ -17,10 +17,14 @@ val operator >> = {
 
 val "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
+val zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
 overload operator | = {or_vec}
 
 val my_replicate_bits : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm)
 
+val zeros = "zeros" : forall 'n. atom('n) -> bits('n)
+
 function my_replicate_bits(n, xs) = {
   ys = zeros(n * length(xs));
   foreach (i from 1 to n) {
diff --git a/doc/introduction.tex b/doc/introduction.tex
index 5969f34f..9e268de5 100644
--- a/doc/introduction.tex
+++ b/doc/introduction.tex
@@ -114,12 +114,12 @@ except vector, float, and load-multiple instructions, without
 exceptions; for ARMv8 this is for the A64 fragment.
 
 The ARMv8 (hand) model is hand-written based on the ARMv8-A
-specification document~\cite{armarmv8,FGP16}, principally by Flur.
+specification document~\cite{armarmv8,FGP16}, principally by \anonymise{Flur}.
 
 The Power model is based on an automatic extraction of pseudocode and
 decoding data from an XML export of the Framemaker document source of
 the IBM Power manual~\cite{Power2.06,micro2015}, with manual patching
-as necessary, principally by Kerneis and Gray.
+as necessary, principally by \anonymise{Kerneis and Gray}.
 
 The ARMv8 (ASL) model is based on an automatic translation of ARM's
 machine-readable public v8.3 ASL specification\footnote{ARM v8-A
@@ -135,7 +135,7 @@ which in turn drew on MIPS4000 and MIPS32~\cite{MIPS4000,MIPS32-I}.
 %
 The CHERI model is based on that and the CHERI ISA reference manual
 version~5~\cite{UCAM-CL-TR-891}. These two are both principally by
-Norton-Wright; they cover all basic user and kernel mode MIPS features
+\anonymise{Norton-Wright}; they cover all basic user and kernel mode MIPS features
 sufficient to boot FreeBSD, including a TLB, exceptions and a basic
 UART for console interaction. ISA extensions such as floating point
 are not covered. The CHERI model supports either 256-bit capabilities
diff --git a/doc/manual.tex b/doc/manual.tex
index 3b75b26a..d28719a4 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -64,9 +64,15 @@
 
 \title{The Sail instruction-set semantics specification language}
 
+\ifdefined\ANON
+\author{Anonymous}
+\newcommand\anonymise[1]{\emph{redacted}}
+\else
 \author{Alasdair Armstrong \and Thomas Bauereiss \and Brian Campbell \and
   Shaked Flur \and Kathryn E. Gray \and Robert Norton-Wright \and Christopher Pulte \and
   Peter Sewell}
+\newcommand\anonymise[1]{#1}
+\fi
 
 \maketitle
 
@@ -80,7 +86,8 @@
 
 \include{tutorial}
 
-\include{types}
+% Remove for now since incomplete
+%\include{types}
 
 \bibliographystyle{unsrt}
 \bibliography{manual}