diff options
| author | Jim Fehrle | 2019-08-05 15:10:32 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-11-20 08:53:00 -0800 |
| commit | b4eca882b6692b6374dfff8517f9f5a5cc4970f5 (patch) | |
| tree | ed72a4b0a4cc67c4a988349fb28e0600e7f03ea7 /Makefile.doc | |
| parent | 4aa756934eb37c6b6d70eddf2b46871bb8ff0956 (diff) | |
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.
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 39 |
1 files changed, 39 insertions, 0 deletions
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 |