From b4eca882b6692b6374dfff8517f9f5a5cc4970f5 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 5 Aug 2019 15:10:32 -0700
Subject: Update grammar in the Terms section of Gallina chapter Update
 doc_grammar tool

The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
  grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
  rsts using instructions embedded in the rsts

Running doc_grammar is currently a manual step.

The grammar updates in the rst files have been manually reviewed.
---
 Makefile.doc | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index 041f26f0b4..8e958532f0 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -227,6 +227,45 @@ install-doc-sphinx:
 		$(INSTALLLIB) doc/sphinx/_build/$$d/$$f $(FULLDOCDIR)/sphinx/$$d/$$f;\
 	done; done)
 
+######################################################################
+# doc_grammar tool
+######################################################################
+
+DOC_GRAMCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex))
+
+$(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/tools/docgram/doc_grammar.ml
+	$(SHOW)'OCAMLC -a $@'
+	$(HIDE)$(OCAMLC) -I coqpp $^ -package str -linkall -linkpkg -o $@
+
+# user-contrib/*/*.mlg omitted for now (e.g. ltac2)
+PLUGIN_MLGS := $(wildcard plugins/*/*.mlg)
+OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg
+DOC_MLGS := */*.mlg $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS)))
+DOC_EDIT_MLGS := doc/tools/docgram/*.edit_mlg
+DOC_RSTS := doc/sphinx/*.rst doc/sphinx/*/*.rst
+
+doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
+	$(SHOW)'DOC_GRAM'
+	$(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS)
+
+#todo: add a dependency of sphinx on updated_rsts when we're ready
+doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: $(DOC_GRAM) $(DOC_EDIT_MLGS)
+	$(SHOW)'DOC_GRAM_RSTS'
+	$(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS)
+
+doc/tools/docgram/updated_rsts: doc/tools/docgram/orderedGrammar
+
+.PHONY: doc_gram doc_gram_verify doc_gram_rsts
+
+doc_gram: doc/tools/docgram/fullGrammar
+
+doc_gram_verify: doc/tools/docgram/fullGrammar
+	$(SHOW)'DOC_GRAM_VERIFY'
+	$(HIDE)$(DOC_GRAM) -short -no-warn -verify $(DOC_MLGS) $(DOC_RSTS)
+
+doc_gram_rsts: doc/tools/docgram/updated_rsts
+
+
 # For emacs:
 # Local Variables:
 # mode: makefile
-- 
cgit v1.2.3