move y2l to tools directory to avoid Windows aux issues

.gitignore

@@ -9,6 +9,8 @@ grammar_lexer.o
 grammar_parser.ml
 grammar_parser.mli
 grammar_parser.output
+grammar_parser.tex
+grammar_parser.mly-y2l
 version.tex
 *byte
 *opt
@@ -17,4 +19,4 @@ bin/
 ocamlgraph-1.7
 .merlin
 make_merlin.sh
-ott.install
+ott.install

README.md

@@ -240,7 +240,6 @@ There is a [plugin for VSCode](https://marketplace.visualstudio.com/items?itemNa
 
 directory                | description
 -----------------------  | -------------------------------------------------
-`aux/`                   | auxiliary code (y2l) used to build the user guide
 `bin/`                   | the Ott binary
 `built_doc/`             | the user guide, in html, pdf, and ps
 `coq/`                   | auxiliary files for Coq
@@ -252,6 +251,7 @@ directory                | description
 `menhir/`                | auxiliary files for menhir
 `regression/`            | regression-test machinery
 `tests/`                 | various small example Ott files
+`tools/`                 | auxiliary code (y2l) used to build the user guide
 `src/`                   | the (OCaml) Ott sources
 `Makefile`               | a Makefile for the examples
 `LICENCE`                | the BSD-style licence terms

doc/Makefile

@@ -448,8 +448,8 @@ install-top2-built: top2.html top2.ps top2.pdf
 # markdown processing and in the latex user guide
 README.tex: ../README.md
 	rm -rf README.tex
-	cat ../README.md | sed -e 's/|//g' > README.tmp.md
-	pandoc  README.tmp.md -o README.tmp.tex
+	cat ../README.md | sed -e 's/|//g' -e '/docker/d' > README.tmp.md
+	pandoc --no-highlight README.tmp.md -o README.tmp.tex
 	cat README.tmp.tex | sed -e 's/section{Ott}/section{Getting started with Ott (the README)}/g' | sed -e 's/href/ahref/g' | sed -e 's/\\noalign{\\medskip}//g' > README.tex
 	chmod ugo-w README.tex
 

revision_history.txt

@@ -569,3 +569,9 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l
 2024-04 @palmskog: Coq 8.19 compatibility
 
 2024-09 @palmskog: output simplified HOL4 Inductive syntax for trindemossen-1 and later, modernise HOL4 libraries
+
+2024-11 @bacam: fix marshalling
+
+2024-12 @palmskog: add explicit locality to generated Coq Hint commands
+
+2024-12 @palmskog: move y2l to non-aux directory to avoid Windows problems, fix doc build

src/Makefile

@@ -241,7 +241,7 @@ coq-lib:
 
 # magic to tex-ify our yacc parser
 
-Y2L=../aux/y2l/y2l  
+Y2L=../tools/y2l/y2l
 
 %.mly-y2l : %.mly
 	cat $< | tr -d \' | grep -v '%start' | grep -v '%type' | sed -e 's/%prec [^ ]*//' > $@