| Age | Commit message (Collapse) | Author |
|---|
|
Now that the checker is using the regular kernel files it can also use
the normal printers.
|
|
|
|
|
|
This reverts commit c4880effb91fab55c250a799cbceac9b04681db0, reversing
changes made to 65927c22bcad62e1bc9a28a57377d82eba215a2d.
|
|
|
|
for pretyping"
|
|
|
|
|
|
|
|
|
|
This is the first release that contains the type-safe grammar API.
|
|
This reverts commit 8d8200d4bff3ffc44efc51ad44dccee9eb14ec6a.
Fix #7936
# Conflicts:
# proofs/clenvtac.ml
|
|
|
|
|
|
|
|
section of CHANGES.md.
|
|
[ci skip]
|
|
|
|
|
|
|
|
In #8900 a quicker build target is requested, this PR does provide
targets towards that goal.
- `check`, introduced in Dune 1.5.0, will build all ml files in a fast way,
- `quick{byte,opt}`, does build a set of relevant hand-picked targets.
Further improvements could come from having `coq_dune` use
`coqtop.byte` when appropriate, taking advantage from
https://github.com/ocaml/dune/issues/1073, and not generating rules
for `.vo` files.
|
|
Following discussion in #7042, we write down an advice to give time
for last comments before merging potentially controversial PRs.
We document a practice that is becoming standard in order to improve
PR merging time: some other maintainer can self-assign if the main
maintainer is not responding.
Encourage component maintainers to announce when they won't be available.
We document the practice of code owner teams.
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
Also update CAMLP5_VER_EDGE: 7.06 → 7.06.10-g84ce6cc4
This is to avoid an OCaml bug that occurs when compiling the OCaml code
extracted from part of a patched version of CompCert.
~~~
File "extraction/Parser.ml", line 12375, characters 19-29:
Error: Constraints are not satisfied in this type.
Type initstate' should be an instance of initstate'
~~~
This compiler issue only appears with OCaml 4.07.0 (neither with 4.06
nor with 4.07.1); hence this update.
|
|
"${foo+}" is always the empty string
"${foo-}" is "$foo" when foo is set and empty string when it's unset.
|
|
|
|
At the same time, we made the safe_env threading explicit.
|
|
|
|
|
|
|
|
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
It was full with utility functions and wrappers that are unused in the Coq
codebase.
|
|
|
|
|
|
terms
This is necessary for programs like Equations that call add_definition
and want to later update in their hook some separate datastructures
which refer to the obligations that are defined by Program. We give back
a map from obligation name to a constr defined in the program's universe
state which the hook returns as well. (Obligation names also correspond
to undefined evars in the original terms through
Obligations.eterm_obligations).
Using this, I can avoid ucontext_of_aucontext in Equations, allowing PR
#8601 to go through.
|
|
This mostly fixes text that was italicized instead of teletyped. When
possible, tactic names have been made to point to their documentation.
Also, the date of the 8.9 release has been proactively changed to
November.
|
|
|
|
This is a bit more portable.
|
|
|
|
This constructor only makes sense in the backtracking mode, that has
been removed from our vendored version of camlp5.
|
|
It is just a wrapper around Sopt. I do not really understand why it is
hardwired in the entry AST.
|
|
Used by rule factorisation in theory, but appears to be unused in Coq.
|
|
It is only used in strict mode, which makes no sense for Coq grammar.
|
|
This constructor was only used by meta-level macros that are not used and
serve no purpose in the grammar engine.
|
|
When `-coqlib $PATH` is absent, Coq will try to locate coqlib using a
heuristic based on the name of the executable.
The code in `envars.ml` basically does:
```ocaml
Filename.(dirname CUnix.(canonical_path_name (dirname Sys.executable_name)))
```
which doesn't seem to work very well on Windows and OSX when `coqtop`
is a symlink.
Instead, we now pass the right `-coqlib` to coqtop from `coq_dune`.
Maybe fixes #8862.
|
