| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
We also workaround problem #11405 , however, this should be reverted
once the problem is fixed in OCaml upstream.
|
|
As suggested by Pierre-Marie Pédrot, this is a more conservative
version of #8771 .
In this commit, we replace Coq's custom backtrace type with OCaml
`Printexc.raw_backtrace`; this seems to already give some improvements
in terms of backtraces [see below] and removes quite a bit of code.
Main difference in terms of API is that backtraces become now
first-class in `Exninfo`, and we seek to consolidate thus the
exception-related APIs in that module.
We also fix a bug in `vernac.ml` where the backtrace captured was the
one of `edit_at`.
Closes #6446
Example with backtrace from https://github.com/coq/coq/issues/11366
Old:
```
raise @ file "stdlib.ml", line 33, characters 17-33
frame @ file "pretyping/coercion.ml", line 406, characters 24-68
frame @ file "list.ml", line 117, characters 24-34
frame @ file "pretyping/coercion.ml", line 393, characters 4-1004
frame @ file "pretyping/coercion.ml", line 450, characters 12-40
raise @ unknown
frame @ file "pretyping/coercion.ml", line 464, characters 6-46
raise @ unknown
frame @ file "pretyping/pretyping.ml", line 839, characters 33-95
frame @ file "pretyping/pretyping.ml", line 875, characters 50-94
frame @ file "pretyping/pretyping.ml", line 1280, characters 2-81
frame @ file "pretyping/pretyping.ml", line 1342, characters 20-71
frame @ file "vernac/vernacentries.ml", line 1579, characters 17-48
frame @ file "vernac/vernacentries.ml", line 2215, characters 8-49
frame @ file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
New:
```
Raised at file "stdlib.ml", line 33, characters 17-33
Called from file "pretyping/coercion.ml", line 406, characters 24-68
Called from file "list.ml", line 117, characters 24-34
Called from file "pretyping/coercion.ml", line 393, characters 4-1004
Called from file "pretyping/coercion.ml", line 450, characters 12-40
Called from file "pretyping/coercion.ml", line 464, characters 6-46
Called from file "pretyping/pretyping.ml", line 839, characters 33-95
Called from file "pretyping/pretyping.ml", line 875, characters 50-94
Called from file "pretyping/pretyping.ml" (inlined), line 1280, characters 2-81
Called from file "pretyping/pretyping.ml", line 1294, characters 21-94
Called from file "pretyping/pretyping.ml", line 1342, characters 20-71
Called from file "vernac/vernacentries.ml", line 1579, characters 17-48
Called from file "vernac/vernacentries.ml", line 2215, characters 8-49
Called from file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
|
|
Reviewed-by: maximedenes
|
|
|
|
Integrate merging doc in the main contributing document.
|
|
INSTALL.md
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: jfehrle
|
|
|
|
For now we don't enable it in any source file, neither on dune files.
`lint-repository` has been updated so it will check `dune build @fmt`
returns 0.
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
It is useful for the release process, and there is no reason for somebody
to lose time reimplementing it again.
|
|
|
|
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.
A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.
Also fixes #10504.
|
|
(by the checker refactor AFAICT)
+ fix commit for the coqtop side fix (it got rebased at some point)
Close #10705
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
Opening up a lambda should always lift the substitution attached to it.
|
|
|
|
Explain into the release process how to prepare the release notes.
|
|
Ack-by: ejgallego
Reviewed-by: vbgl
|
|
|
|
|
|
We use the `(coq.pp ...)` dune directive which will produce correct
error messages for `.mlg` files.
Unfortunately we cannot yet use the automatic opam generation features
of Dune 1.10, as this does require a fully native Dune build.
Dune 1.6-1.10 has quite a few other improvements that could be used by
Coq, for example for promote modes.
I have fixed a couple of documentation issues. `Drop` and `ocamldebug`
have been tested in this version.
|
|
|
|
And also clean INSTALL file of useless reminder of the procedure to
install using a package manager.
|
|
|
|
The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.
This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.
Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.
As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.
We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.
|
|
Formerly, knowing if a declaration was to be discharged, to be global
but invisible at import, or to be global but visible at import was
obtained by combining the parser-level information (i.e. use of
Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use
of Local vs Global) with the result of testing whether there were open
sections.
We change the meaning of the Discharge flag: it does not tell anymore
that it was syntactically a Variable/Hypothesis/Let, but tells the
expected semantics of the declaration (issuing a warning in the
parser-to-interpreter step if the semantics is not the one suggested
by the syntax). In particular, the interpretation/command engine
becomes independent of the parser.
The new "semantic" type is:
type import_status = ImportDefaultBehavior | ImportNeedQualified
type locality = Discharge | Global of import_status
In the process, we found a couple of inconsistencies in the treatment
of the locality status. See bug #8722 and test file LocalDefinition.v.
|
|
|
|
|
|
- use coqc instead of coqtop (since -compile doesn't work anymore this
is better)
- pass through extra arguments to dune-dbg
- auto detect the need to pass -emacs to ocamldebug
- instructions for emacs users
The dune-dbg dependencies are still broken ;_;
|
|
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: vbgl
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
|
|
Move existing entries.
|
|
Reviewed-by: maximedenes
|
|
Ack-by: Zimmi48
Reviewed-by: maximedenes
Ack-by: proux01
Reviewed-by: vbgl
|
|
|
|
The amount of dangerous warnings in plugins is out of hand, including
some very serious ones.
As Coq developers are maintaining plugins these days it makes sense to
require the contributions to follow the same coding discipline as in
the main tree, thus we require the set of warnings fatal warnings to
be the same in Coq and in plugins.
We don't mark deprecation as fatal as to allow time for migration.
Fixes #6974
|
|
|
