| Age | Commit message (Collapse) | Author |
|---|
|
`CoqProject_file` uses the feedback system, however this is not very
convenient in some scenarios such as `coqdep` that has to be run very
early in the build process [and thus in "boot" mode].
We thus make the warning function a paramater.
Should fix #8913.
|
|
|
|
|
|
This PR fixes an issues that was bugging me for some time, namely that
`Vernacinterp` really means `Vernacextend`.
We thus rename the file and move the associated functions there, which
were incorrectly placed in `Vernacentries`.
Note the beneficial effects on reducing the `.mli` API.
|
|
|
|
Avoid downloading Coq.
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
This is the first release that contains the type-safe grammar API.
|
|
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We update the docs for the removal of `Sigma` and the deprecation of
`enter_nf`.
|
|
an environment
|
|
|
|
|
|
|
|
This is a step towards limiting calls to the global environment.
Incidentally unify naming evd -> sigma in Termops.
|
|
merged commit."
|
|
|
|
|
|
This reverts commit df69c44af03f2587b3f1706a805d0e2728c1f1dc.
Should be merged before any PR with plugin tutorial overlays, or we
can just merge the vendor PR instead.
|
|
|
|
|
|
|
|
We need to update in Docker:
- dune to 1.4.0: as it honors `-p` on test stanzas
- dune-release to 1.1.0: support for OPAM 2.0 + fixes
This makes `dune-release distrib` / `dune-release opam pkg` work.
TODO: we need to figure out what is going on with the
versioning. Should we do `dune subst` on `pinned`?
|
|
As noted by Gäetan, we didn't compile these. We also provide a recipe
to run `ocamldebug`. Try (after a build):
```
dune exec dev/dune-dbg
(ocd) source dune_db
```
or
```
dune exec dev/dune-dbg checker
(ocd) source checker_dune_db
```
for the checker.
|
|
We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.
Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.
We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.
|
|
This includes many changes, please have a look at the newly generated
docs.
|
|
|
|
This fixes the CI until this commit is merged into master.
|
|
We had a brief leftovers of the ocamlbuild experiment that are not
relevant anymore as it was removed from the tree a few years ago.
p.s: The amount of cruft we have in the `dev/build/windows` folder is
staggering, see for example what `git grep ocamlbuild` returns.
|
