| 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.
|
|
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.
|
|
I'd like to add this convention as it is very convenient for the
development of dev tools. Example, I can do `setup-coq-devs ltac
equations` and then get a fully composed tree. Similarly for preparing
overlays.
|
|
|
|
Those optional arguments did not really make sense. It was pretty clear from
our code base, as all instances where triplicating the same type for TYPED,
RAW_TYPED and GLOB_TYPED.
|
|
|
|
Fixes #8337
|
|
Not a big point on running the checker on Appveyor I think, this will
save a bunch of time and improve reliability.
|
|
"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.
We thus remove the polymorphism with the hope to be able to reify the
control later on.
|
|
|
|
|
