diff options
| -rw-r--r-- | .github/CODEOWNERS | 2 | ||||
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | CREDITS | 13 | ||||
| -rw-r--r-- | dev/doc/build-system.txt | 8 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 2 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 | ||||
| -rw-r--r-- | doc/changelog/README.md | 27 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 4 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 4 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | plugins/cc/README | 2 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 2 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
15 files changed, 52 insertions, 52 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 4789d9b6fa..6c6e4bdfcb 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -320,6 +320,8 @@ azure-pipelines.yml @coq/ci-maintainers /test-suite/unit-tests/src/ @jfehrle # Secondary maintainer @SkySkimmer +/test-suite/success/Compat*.v @JasonGross + ########## Developer tools ########## /dev/tools/backport-pr.sh @Zimmi48 diff --git a/.gitignore b/.gitignore index 587a6191ab..ad5204847c 100644 --- a/.gitignore +++ b/.gitignore @@ -135,7 +135,7 @@ ide/protocol/xml_lexer.ml coqpp/coqpp_parse.ml coqpp/coqpp_parse.mli -# .ml4 / .mlp files +# .mlg / .mlp files g_*.ml @@ -101,6 +101,7 @@ of the Coq Proof assistant during the indicated time: Daniel de Rauglaudre (INRIA, 1996-1998, 2012, 2016) Olivier Desmettre (INRIA, 2001-2003) Gilles Dowek (INRIA, 1991-1994) + Jim Fehrle (2018-now) Amy Felty (INRIA, 1993) Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-2008) Emilio Jesús Gallego Arias (MINES ParisTech 2015-now) @@ -116,12 +117,13 @@ of the Coq Proof assistant during the indicated time: Matej Košík (INRIA, 2015-2017) Leonidas Lampropoulos (University of Pennsylvania, 2018) Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, - INRIA-PPS then IRIF, 2009-now) + INRIA-PPS then IRIF, 2009-2018) Yao Li (ORCID: https://orcid.org/0000-0001-8720-883X, University of Pennsylvania, 2018) Yishuai Li (ORCID: https://orcid.org/0000-0002-5728-5903 U. Penn, 2018-2019) Patrick Loiseleur (Paris Sud, 1997-1999) + Andreas Lynge (Aarhus University, 2019) Evgeny Makarov (INRIA, 2007) Gregory Malecha (Harvard University 2013-2015, University of California, San Diego 2016) @@ -140,16 +142,15 @@ of the Coq Proof assistant during the indicated time: LRI, 1997-2006) Pierre-Marie Pédrot (INRIA-PPS, 2011-2015, INRIA-Ascola, 2015-2016, University of Ljubljana, 2016-2017, - MPI-SWS, 2017-2018) - Clément Pit-Claudel (MIT, 2015-2018) + MPI-SWS, 2017-2018, INRIA 2018-now) + Clément Pit-Claudel (MIT, 2015-now) Matthias Puech (INRIA-Bologna, 2008-2011) - Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-now) + Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-2016) Clément Renard (INRIA, 2001-2004) Talia Ringer (University of Washington, 2019) - Andreas Lynge (Aarhus University, 2019) Claudio Sacerdoti Coen (INRIA, 2004-2005) Amokrane Saïbi (INRIA, 1993-1998) - Vincent Semeria (2018) + Vincent Semeria (2018-now) Vincent Siles (INRIA, 2007) Élie Soubiran (INRIA, 2007-2010) Matthieu Sozeau (INRIA, 2005-now) diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index a14781a058..b8987b7086 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -89,7 +89,7 @@ enables partial recalculation of dependencies (only the dependencies of changed files are recomputed). If you add a dependency to a Coq camlp5 extension (grammar.cma or -q_constr.cmo), then see sections ".ml4 files" and "new files". +q_constr.cmo), then see sections ".mlg files" and "new files". Cleaning Targets ---------------- @@ -113,13 +113,13 @@ Targets for cleaning various parts: - docclean: clean documentation -.ml4/.mlp files +.mlg/.mlp files --------------- There is now two kinds of preprocessed files : - a .mlp do not need grammar.cma (they are in grammar/) - - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), - except coqide_main.ml4 and its specific rule + - a .mlg is now always preprocessed with grammar.cma (and q_constr.cmo), + except coqide_main.mlg and its specific rule This classification replaces the old mechanism of declaring the use of a grammar extension via a line of the form: diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index e5e4f740bd..096ffe6a1c 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -20,7 +20,7 @@ Special components grammar : Camlp5 syntax extensions. The file grammar/grammar.cma is used - to pre-process .ml4 files containing EXTEND constructions, + to pre-process .mlg files containing EXTEND constructions, either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND. This grammar.cma incorporates many files from other directories (mainly parsing/), plus some specific files in grammar/. diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 601d52ddda..2f5c7128e2 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -727,7 +727,7 @@ Conflicts exists between integers and constrs. \nlsep \TERM{setoid_replace} ~\tacconstr ~\KWD{with} ~\tacconstr \nlsep \TERM{setoid_rewrite} ~\NT{orient} ~\tacconstr \nlsep \TERM{subst} ~\STAR{\NT{ident}} -%% eqdecide.ml4 +%% eqdecide.mlg \nlsep \TERM{decide}~\TERM{equality} ~\OPTGR{\tacconstr~\tacconstr} \nlsep \TERM{compare}~\tacconstr~\tacconstr %% eauto diff --git a/doc/changelog/README.md b/doc/changelog/README.md index 2891eb207e..3e0970a656 100644 --- a/doc/changelog/README.md +++ b/doc/changelog/README.md @@ -7,25 +7,28 @@ otherwise important infrastructure changes, and important bug fixes should get a changelog entry. Compatibility-breaking changes should always get a changelog entry, -which should explain what compatibility-breakage is to expect. +which should explain what compatibility breakage is to expect. Pull requests changing the ML API in significant ways should add an entry in [`dev/doc/changes.md`](../../dev/doc/changes.md). ## How to add an entry? ## -You should create a file in one of the sub-directories. The name of -the file should be `NNNNN-identifier.rst` where `NNNNN` is the number -of the pull request on five digits and `identifier` is whatever you -want. - -This file should use the same format as the reference manual (as it -will be copied in there). You may reference the documentation you just -added with `:ref:`, `:tacn:`, `:cmd:`, `:opt:`, `:token:`, etc. See +Run `./dev/tools/make-changelog.sh`: it will ask you for your PR +number, and to choose among the predefined categories. Afterward, +fill in the automatically generated entry with a short description of +your change (which should describe any compatibility issues in +particular). You may also add a reference to the relevant fixed +issue, and credit reviewers, co-authors, and anyone who helped advance +the PR. + +The format for changelog entries is the same as in the reference +manual. In particular, you may reference the documentation you just +added with `:ref:`, `:tacn:`, `:cmd:`, `:opt:`, `:token:`, etc. See the [documentation of the Sphinx format](../sphinx/README.rst) of the manual for details. -The entry should be written using the following structure: +Here is a summary of the structure of a changelog entry: ``` rst - Description of the changes, with possible link to @@ -35,7 +38,3 @@ The entry should be written using the following structure: [ and `#ISSUE2 <https://github.com/coq/coq/issues/ISSUE2>`_],] by Full Name[, with help / review of Full Name]). ``` - -The description should be kept rather short and the only additional -required meta-information are the link to the pull request and the -full name of the author. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 0148925247..b6fcf9da22 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -198,21 +198,21 @@ Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2) with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. -The 61 contributors to this version are David A. Dalrymple, Tanaka -Akira, Benjamin Barenblat, Yves Bertot, Frédéric Besson, Lasse -Blaauwbroek, Martin Bodin, Joachim Breitner, Tej Chajed, Frédéric -Chapoton, Arthur Charguéraud, Cyril Cohen, Lukasz Czajka, Christian -Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Gaëtan Gilbert, Matěj -Grabovský, Simon Gregersen, Jason Gross, Samuel Gruetter, Hugo Herbelin, -Jasper Hugunin, Mirai Ikebuchi, Emilio Jesus Gallego Arias, Chantal -Keller, Matej Košík, Vincent Laporte, Olivier Laurent, Larry Darryl Lee -Jr, Pierre Letouzey, Nick Lewycky, Yao Li, Yishuai Li, Xia Li-yao, Assia -Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, Guillaume -Melquiond, Kayla Ngan, Sam Pablo Kuper, Karl Palmskog, Clément -Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Ryan -Scott, Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, -Enrico Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo -Winterhalter, Beta Ziliani and Théo Zimmermann. +The 61 contributors to this version are Tanaka Akira, Benjamin +Barenblat, Yves Bertot, Frédéric Besson, Lasse Blaauwbroek, Martin +Bodin, Joachim Breitner, Tej Chajed, Frédéric Chapoton, Arthur +Charguéraud, Cyril Cohen, Lukasz Czajka, David A. Dalrymple, Christian +Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesus Gallego +Arias, Gaëtan Gilbert, Matěj Grabovský, Simon Gregersen, Jason Gross, +Samuel Gruetter, Hugo Herbelin, Jasper Hugunin, Mirai Ikebuchi, +Chantal Keller, Matej Košík, Sam Pablo Kuper, Vincent Laporte, Olivier +Laurent, Larry Darryl Lee Jr, Nick Lewycky, Yao Li, Yishuai Li, Assia +Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, +Guillaume Melquiond, Kayla Ngan, Karl Palmskog, Pierre-Marie Pédrot, +Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Ryan Scott, +Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, Enrico +Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo Winterhalter, +Xia Li-yao, Beta Ziliani and Théo Zimmermann. Many power users helped to improve the design of the new features via the issue and pull request system, the |Coq| development mailing list, diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 47ecfb9db0..9e219bd503 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -62,7 +62,7 @@ A simple example of a ``_CoqProject`` file follows: theories/foo.v theories/bar.v -I src/ - src/baz.ml4 + src/baz.mlg src/bazaux.ml src/qux_plugin.mlpack @@ -111,7 +111,7 @@ decide how to build them. In particular: + |Coq| files must use the ``.v`` extension + |OCaml| files must use the ``.ml`` or ``.mli`` extension + |OCaml| files that require pre processing for syntax - extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension + extensions (like ``VERNAC EXTEND``) must use the ``.mlg`` extension + In order to generate a plugin one has to list all |OCaml| modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib`` file). diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 279815d671..181418d3d8 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -408,10 +408,8 @@ object (self) | _ -> () method apply_unicode_binding () = - (* Auxiliary method to reach the beginning of line or the - nearest space before the iterator. *) let rec get_line_start iter = - if iter#starts_line || Glib.Unichar.isspace iter#char then iter + if iter#starts_line then iter else get_line_start iter#backward_char in (* Main action *) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index e0d63a723e..0a41bba8ce 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -597,7 +597,7 @@ let unfreeze (grams, lex) = (** No need to provide an init function : the grammar state is statically available, and already empty initially, while the lexer state should not be reset, since it contains - keywords declared in g_*.ml4 *) + keywords declared in g_*.mlg *) let parser_summary_tag = Summary.declare_summary_tag "GRAMMAR_LEXER" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 10f78a5a72..ca5adf8ab3 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -108,7 +108,7 @@ end - "f" constr(x) (developer gives an EXTEND rule) | - | macro-generation in tacextend.ml4/vernacextend.ml4/argextend.ml4 + | macro-generation in tacextend.mlg/vernacextend.mlg/argextend.mlg V [GramTerminal "f"; GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")] diff --git a/plugins/cc/README b/plugins/cc/README index c616b5daab..7df7b971e8 100644 --- a/plugins/cc/README +++ b/plugins/cc/README @@ -9,7 +9,7 @@ Files : - ccalgo.ml : congruence closure algorithm - ccproof.ml : proof generation code -- cctac.ml4 : the tactic itself +- cctac.mlg : the tactic itself - CCSolve.v : a small Ltac tactic based on congruence Known Bugs : the congruence tactic can fail due to type dependencies. diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index ef012e5092..f47a14cdc7 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,7 +9,7 @@ (************************************************************************) (* This file uses the (non-compressed) union-find structure to generate *) -(* proof-trees that will be transformed into proof-terms in cctac.ml4 *) +(* proof-trees that will be transformed into proof-terms in cctac.mlg *) open CErrors open Constr diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index d37d2bea94..08253e5a8f 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -266,7 +266,7 @@ CMIFILES = \ $(CMOFILES:.cmo=.cmi) \ $(MLIFILES:.mli=.cmi) # the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just -# a .ml4 file +# a .mlg file CMXSFILES = \ $(MLPACKFILES:.mlpack=.cmxs) \ $(CMXAFILES:.cmxa=.cmxs) \ |