diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/10858-stuck-classed.md | 12 | ||||
| -rw-r--r-- | doc/dune | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 17 | ||||
| -rw-r--r-- | doc/tools/docgram/README.md | 15 | ||||
| -rw-r--r-- | doc/tools/docgram/dune | 30 |
5 files changed, 66 insertions, 10 deletions
diff --git a/doc/changelog/02-specification-language/10858-stuck-classed.md b/doc/changelog/02-specification-language/10858-stuck-classed.md new file mode 100644 index 0000000000..c7186f2c1d --- /dev/null +++ b/doc/changelog/02-specification-language/10858-stuck-classed.md @@ -0,0 +1,12 @@ +- **Changed:** + Typeclass resolution, accessible through :tacn:`typeclasses eauto`, + now suspends constraints according to their modes + instead of failing. If a typeclass constraint does not match + any of the declared modes for its class, the constraint is postponed, and + the proof search continues on other goals. Proof search does a fixed point + computation to try to solve them at a later stage of resolution. It does + not fail if there remain only stuck constraints at the end of resolution. + This makes typeclasses with declared modes more robust with respect to the + order of resolution. + (`#10858 <https://github.com/coq/coq/pull/10858>`_, + fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). @@ -14,7 +14,7 @@ unreleased.rst (env_var SPHINXWARNOPT)) (action - (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index af4e9051bb..7abeca7815 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -385,8 +385,10 @@ few other commands related to typeclasses. .. tacn:: typeclasses eauto :name: typeclasses eauto - This tactic uses a different resolution engine than :tacn:`eauto` and - :tacn:`auto`. The main differences are the following: + This proof search tactic implements the resolution engine that is run + implicitly during type-checking. This tactic uses a different resolution + engine than :tacn:`eauto` and :tacn:`auto`. The main differences are the + following: + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in the new proof engine (as of Coq 8.6), meaning that backtracking is @@ -422,6 +424,17 @@ few other commands related to typeclasses. resolution with the local hypotheses use full conversion during unification. + + The mode hints (see :cmd:`Hint Mode`) associated to a class are + taken into account by :tacn:`typeclasses eauto`. When a goal + does not match any of the declared modes for its head (if any), + instead of failing like :tacn:`eauto`, the goal is suspended and + resolution proceeds on the remaining goals. + If after one run of resolution, there remains suspended goals, + resolution is launched against on them, until it reaches a fixed + point when the set of remaining suspended goals does not change. + Using `solve [typeclasses eauto]` can be used to ensure that + no suspended goals remain. + + When considering local hypotheses, we use the union of all the modes declared in the given databases. diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index fc6d0ace0d..8f325f957a 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -1,12 +1,13 @@ # Grammar extraction tool for documentation -`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it in -chunks into `.rst` files. The tool currently inserts Sphinx -`productionlist` constructs. It also generates a file with `prodn` constructs -for the entire grammar, but updates to `tacn` and `cmd` constructs must be done -manually since the grammar doesn't have names for them as it does for -nonterminals. There is an option to report which `tacn` and `cmd` were not -found in the `.rst` files. `tacv` and `cmdv` constructs are not processed at all. +`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and +inserts it in chunks into `.rst` files. The tool currently inserts +Sphinx `productionlist` and `prodn` constructs (`productionlist` are +gradually being replaced by `prodn` in the manual). Updates to `tacn` +and `cmd` constructs must be done manually since the grammar doesn't +have names for them as it does for nonterminals. There is an option +to report which `tacn` and `cmd` were not found in the `.rst` files. +`tacv` and `cmdv` constructs are not processed at all. The mlg grammars present several challenges to generating an accurate grammar for documentation purposes: diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune new file mode 100644 index 0000000000..3afa21f2cf --- /dev/null +++ b/doc/tools/docgram/dune @@ -0,0 +1,30 @@ +(executable + (name doc_grammar) + (libraries coq.clib coqpp)) + +(env (_ (binaries doc_grammar.exe))) + +(rule + (targets fullGrammar) + (deps + ; Main grammar + (glob_files %{project_root}/parsing/*.mlg) + (glob_files %{project_root}/toplevel/*.mlg) + (glob_files %{project_root}/vernac/*.mlg) + ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc) + (glob_files %{project_root}/plugins/btauto/*.mlg) + (glob_files %{project_root}/plugins/cc/*.mlg) + (glob_files %{project_root}/plugins/derive/*.mlg) + (glob_files %{project_root}/plugins/extraction/*.mlg) + (glob_files %{project_root}/plugins/firstorder/*.mlg) + (glob_files %{project_root}/plugins/funind/*.mlg) + (glob_files %{project_root}/plugins/ltac/*.mlg) + (glob_files %{project_root}/plugins/micromega/*.mlg) + (glob_files %{project_root}/plugins/nsatz/*.mlg) + (glob_files %{project_root}/plugins/omega/*.mlg) + (glob_files %{project_root}/plugins/rtauto/*.mlg) + (glob_files %{project_root}/plugins/setoid_ring/*.mlg) + (glob_files %{project_root}/plugins/syntax/*.mlg)) + (action + (chdir %{project_root} (run doc_grammar -short -no-warn %{deps}))) + (mode promote)) |