diff options
| -rw-r--r-- | .github/CODEOWNERS | 6 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 3 | ||||
| -rw-r--r-- | CONTRIBUTING.md | 23 | ||||
| -rw-r--r-- | dev/ci/README.md | 7 | ||||
| -rw-r--r-- | doc/sphinx/biblio.bib | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 37 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4202.v | 10 | ||||
| -rw-r--r-- | theories/FSets/FSetAVL.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 2 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 2 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 2 |
12 files changed, 64 insertions, 40 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 20d49e675f..5be434c8b7 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -42,11 +42,7 @@ # Trick to avoid getting review requests # each time someone modifies the dev changelog -/doc/ @maximedenes -# Secondary maintainer @silene @Zimmi48 - -/doc/tools/coqrst/ @maximedenes -# Secondary maintainer @cpitclaudel +/doc/ @coq/doc-maintainers /man/ @silene # Secondary maintainer @maximedenes diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c2ca6ebaa4..46f8572b94 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -212,6 +212,9 @@ windows32: <<: *windows-template variables: ARCH: "32" + except: + - /^pr-.*$/ + pkg:nix: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9bd3d0b7c7..cd4a246bb4 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -56,9 +56,19 @@ Whitespace discipline (do not indent using tabs, no trailing spaces, text files Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. -- [needs: rebase](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22) indicates the PR should be rebased on top of the latest `master` branch. See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`. -- [needs: fixing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22) indicates the PR needs a fix, as discussed in the comments. -- [needs: benchmarking](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22) and [needs: testing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22) indicate the PR needs testing beyond what the test suite can handle. For example, performance benchmarking is currently performed with a different infrastructure. Unless some followup is specifically requested you aren't expected to do this additional testing. +- [needs: rebase][rebase-label] indicates the PR should be rebased on top of + the latest base branch (usually `master`). See the + [GitHub documentation](https://help.github.com/articles/about-git-rebase/) + for a brief introduction to using `git rebase`. + This label will be automatically added if you open or synchronize your PR and + it is not up-to-date with the base branch. So please, do not forget to rebase + your branch every time you update it. +- [needs: fixing][fixing-label] indicates the PR needs a fix, as discussed in the comments. +- [needs: benchmarking][benchmarking-label] and [needs: testing][testing-label] + indicate the PR needs testing beyond what the test suite can handle. + For example, performance benchmarking is currently performed with a different + infrastructure ([documented in the wiki][jenkins-doc]). Unless some followup + is specifically requested you aren't expected to do this additional testing. To learn more about the merging process, you can read the [merging documentation for Coq maintainers](dev/doc/MERGING.md). @@ -98,3 +108,10 @@ External plugins / libraries contribute to create a successful ecosystem around Ask and answer questions on [Stack Exchange](https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites) which has a helpful community of Coq users. Hang out on the Coq IRC channel, `irc://irc.freenode.net/#coq`, and help answer questions. + +[rebase-label]: https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22 +[fixing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22 +[benchmarking-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22 +[testing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22 + +[jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) diff --git a/dev/ci/README.md b/dev/ci/README.md index 43d680af61..a814e4914e 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -138,14 +138,11 @@ persists to and is used by the next jobs. Artifacts can also be downloaded from the GitLab repository. Currently, available artifacts are: -- the Coq executables and stdlib, in three copies varying in +- the Coq executables and stdlib, in four copies varying in architecture and OCaml version used to build Coq. -- the Coq documentation, built only in the `build:base` job. When submitting +- the Coq documentation, built in the `documentation` job. When submitting a documentation PR, this can help reviewers checking the rendered result. -As an exception to the above, jobs testing that compilation triggers -no OCaml warnings build Coq in parallel with other tests. - ### GitLab and Windows If your repository has access to runners tagged `windows`, setting the diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 9cfcd7ae64..c74d8f540c 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -252,7 +252,7 @@ s}, booktitle = {TYPES}, year = 2002, crossref = {DBLP:conf/types/2002}, - url = {draft at \url{http://www.irif.fr/~letouzey/download/extraction2002.pdf}} + url = {http://www.irif.fr/~letouzey/download/extraction2002.pdf} } @InProceedings{Luttik97specificationof, diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 6e0c1e1b61..a63400103f 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -747,7 +747,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is is: .. math:: - \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} + \ind{0}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} {\left[\begin{array}{rcl} \node &:& \forest → \tree\\ \emptyf &:& \forest\\ @@ -769,7 +769,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is The declaration for a mutual inductive definition of even and odd is: .. math:: - \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ + \ind{0}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ @@ -966,7 +966,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k]`, .. inference:: W-Ind \WFE{Γ_P} - (E[Γ_P ] ⊢ A_j : s_j' )_{j=1… k} + (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k} (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ \WF{E;\ind{p}{Γ_I}{Γ_C}}{Γ} @@ -1025,7 +1025,7 @@ Template polymorphism +++++++++++++++++++++ Inductive types declared in :math:`\Type` are polymorphic over their arguments -in :math:`\Type`. If :math:`A` is an arity of some sort and math:`s` is a sort, we write :math:`A_{/s}` +in :math:`\Type`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local context, then :math:`A_{/s}` is typable by typability of all products in the diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index dc355fa013..6fbb2fac6d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -144,10 +144,11 @@ mode but it can also be used in toplevel definitions as shown below. : | `integer` (< | <= | > | >=) `integer` selector : [`ident`] : | `integer` - : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : | (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) toplevel_selector : `selector` - : | `all` - : | `par` + : | all + : | par + : | ! .. productionlist:: coq top : [Local] Ltac `ltac_def` with ... with `ltac_def` @@ -177,7 +178,7 @@ Sequence A sequence is an expression of the following form: -.. tacn:: @expr ; @expr +.. tacn:: @expr__1 ; @expr__2 :name: ltac-seq The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be @@ -207,11 +208,11 @@ following form: were given. For instance, ``[> | auto]`` is a shortcut for ``[> idtac | auto ]``. - .. tacv:: [> {*| @expr} | @expr .. | {*| @expr}] + .. tacv:: [> {*| @expr__i} | @expr .. | {*| @expr__j}] - In this variant, token:`expr` is used for each goal coming after those - covered by the first list of :n:`@expr` but before those coevered by the - last list of :n:`@expr`. + In this variant, :n:`@expr` is used for each goal coming after those + covered by the list of :n:`@expr__i` but before those covered by the + list of :n:`@expr__j`. .. tacv:: [> {*| @expr} | .. | {*| @expr}] @@ -225,11 +226,11 @@ following form: tactic is not run at all. A tactic which expects multiple goals, such as ``swap``, would act as if a single goal is focused. - .. tacv:: expr ; [{*| @expr}] + .. tacv:: @expr__0 ; [{*| @expr__i}] This variant of local tactic application is paired with a sequence. In this - variant, there must be as many :n:`@expr` in the list as goals generated - by the application of the first :n:`@expr` to each of the individual goals + variant, there must be as many :n:`@expr__i` as goals generated + by the application of :n:`@expr__0` to each of the individual goals independently. All the above variants work in this form too. Formally, :n:`@expr ; [ ... ]` is equivalent to :n:`[> @expr ; [> ... ] .. ]`. @@ -247,20 +248,20 @@ focused goals with: We can also use selectors as a tactical, which allows to use them nested in a tactic expression, by using the keyword ``only``: - .. tacv:: only selector : expr + .. tacv:: only @selector : @expr :name: only ... : ... - When selecting several goals, the tactic expr is applied globally to all + When selecting several goals, the tactic :token:`expr` is applied globally to all selected goals. .. tacv:: [@ident] : @expr - In this variant, :n:`@expr` is applied locally to a goal previously named + In this variant, :token:`expr` is applied locally to a goal previously named by the user (see :ref:`existential-variables`). .. tacv:: @num : @expr - In this variant, :n:`@expr` is applied locally to the :token:`num`-th goal. + In this variant, :token:`expr` is applied locally to the :token:`num`-th goal. .. tacv:: {+, @num-@num} : @expr @@ -271,13 +272,13 @@ focused goals with: .. tacv:: all: @expr :name: all: ... - In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only + In this variant, :token:`expr` is applied to all focused goals. ``all:`` can only be used at the toplevel of a tactic expression. .. tacv:: !: @expr - In this variant, if exactly one goal is focused :n:`expr` is - applied to it. Otherwise the tactical fails. ``!:`` can only be + In this variant, if exactly one goal is focused, :token:`expr` is + applied to it. Otherwise the tactic fails. ``!:`` can only be used at the toplevel of a tactic expression. .. tacv:: par: @expr diff --git a/test-suite/bugs/closed/4202.v b/test-suite/bugs/closed/4202.v new file mode 100644 index 0000000000..522a3604a3 --- /dev/null +++ b/test-suite/bugs/closed/4202.v @@ -0,0 +1,10 @@ +Parameter g : nat -> Prop. +Axiom a : forall n, g (S n). +Lemma foo (H : True) : exists n, g n /\ g n. +eexists. +clear H. +split. +simple apply a. +(* goal is "g (S ?Goal0@ {H:=H})" while H has long ceased to exist *) +simpl. +Abort. diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 3c9b6b428b..dcaea894eb 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -15,7 +15,7 @@ It follows the implementation from Ocaml's standard library, All operations given here expect and produce well-balanced trees - (in the ocaml sense: heigths of subtrees shouldn't differ by more + (in the ocaml sense: heights of subtrees shouldn't differ by more than 2), and hence has low complexities (e.g. add is logarithmic in the size of the set). But proving these balancing preservations is in fact not necessary for ensuring correct operational behavior diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 9d2a73ed0f..95868861fa 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -13,7 +13,7 @@ This module factorizes common parts in implementations of finite sets as AVL trees and as Red-Black trees. The nodes of the trees defined here include an generic information - parameter, that will be the heigth in AVL trees and the color + parameter, that will be the height in AVL trees and the color in Red-Black trees. Without more details here about these information parameters, trees here are not known to be well-balanced, but simply binary-search-trees. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 900964609d..113ba3684c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -425,7 +425,7 @@ let parse_args arglist : coq_cmdopts * string list = |"-worker-id" -> set_worker_id opt (next ()); oval |"-compat" -> - let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in + let v = G_vernac.parse_compat_version (next ()) in Flags.compat_version := v; add_compat_require oval v diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index b959f2afa9..74516e320c 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -59,7 +59,7 @@ let make_bullet s = | '*' -> Star n | _ -> assert false -let parse_compat_version ?(allow_old = true) = let open Flags in function +let parse_compat_version = let open Flags in function | "8.8" -> Current | "8.7" -> V8_7 | "8.6" -> V8_6 |