From 1f6616953547afd3e1a5764c52cdabc160ffbf1c Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 27 Dec 2024 18:21:14 +0100 Subject: [PATCH 1/3] move y2l to tools directory to avoid aux filesystem problems on Windows --- .gitignore | 4 +++- README.md | 2 +- src/Makefile | 2 +- {aux => tools}/y2l/0README_FIRST | 0 {aux => tools}/y2l/Artistic | 0 {aux => tools}/y2l/README | 0 {aux => tools}/y2l/y2l | 0 {aux => tools}/y2l/y2l.man | 0 {aux => tools}/y2l/y2lman.html | 0 9 files changed, 5 insertions(+), 3 deletions(-) rename {aux => tools}/y2l/0README_FIRST (100%) rename {aux => tools}/y2l/Artistic (100%) rename {aux => tools}/y2l/README (100%) rename {aux => tools}/y2l/y2l (100%) rename {aux => tools}/y2l/y2l.man (100%) rename {aux => tools}/y2l/y2lman.html (100%) diff --git a/.gitignore b/.gitignore index b4c8bc1..1f0ab2c 100644 --- a/.gitignore +++ b/.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 \ No newline at end of file +ott.install diff --git a/README.md b/README.md index dc94dfa..60acfb9 100644 --- a/README.md +++ b/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 diff --git a/src/Makefile b/src/Makefile index dfbfcf3..16b87c7 100644 --- a/src/Makefile +++ b/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 [^ ]*//' > $@ diff --git a/aux/y2l/0README_FIRST b/tools/y2l/0README_FIRST similarity index 100% rename from aux/y2l/0README_FIRST rename to tools/y2l/0README_FIRST diff --git a/aux/y2l/Artistic b/tools/y2l/Artistic similarity index 100% rename from aux/y2l/Artistic rename to tools/y2l/Artistic diff --git a/aux/y2l/README b/tools/y2l/README similarity index 100% rename from aux/y2l/README rename to tools/y2l/README diff --git a/aux/y2l/y2l b/tools/y2l/y2l similarity index 100% rename from aux/y2l/y2l rename to tools/y2l/y2l diff --git a/aux/y2l/y2l.man b/tools/y2l/y2l.man similarity index 100% rename from aux/y2l/y2l.man rename to tools/y2l/y2l.man diff --git a/aux/y2l/y2lman.html b/tools/y2l/y2lman.html similarity index 100% rename from aux/y2l/y2lman.html rename to tools/y2l/y2lman.html From ae6dc6a27d2ca2c54c4c1eaada2bcf224d5abac5 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 27 Dec 2024 18:57:04 +0100 Subject: [PATCH 2/3] fix up doc/Makefile to work with recent pandoc and README.md updates --- doc/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/Makefile b/doc/Makefile index 0b255c5..95c7e88 100644 --- a/doc/Makefile +++ b/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 From 10e01872bda7b6a05e7a8433fff527483009ffb9 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 27 Dec 2024 19:27:48 +0100 Subject: [PATCH 3/3] update revision history for nov-dec 2024 --- revision_history.txt | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/revision_history.txt b/revision_history.txt index c07147d..157a6ba 100644 --- a/revision_history.txt +++ b/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