| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
Bumping to 4.02.3 was decided some time ago in the WG, however a
couple of places escaped updating.
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Packages such as `menhir` or `elpi` are fragile w.r.t. updates, so
allowing a non-deterministic install in the Dockefile seems risky. We
have found trouble with Menhir in the past. We thus specify a concrete
version for all `CI_OPAM` packages.
cc: https://github.com/AbsInt/CompCert/issues/234
We also add remove `hevea` from `apt` dependencies as it hasn't been
needed since #7466 and add `texlive-science` which is needed to build
the `source-doc` target due to the `textgreek` package being used.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| | |
https://github.com/AbsInt/CompCert/issues/234
|
| |\ \ |
|
| |\ \ \
| |_|/
|/| | |
|
| |\ \ \ |
|
| | | | | |
|
| | |_|/
|/| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
This is needed for CI packages that use `META.coq` such as in
https://github.com/coq/coq/pull/7656 .
|
| |/ /
| |
| |
| |
| |
| | |
We bump Windows builds to 4.06.1, IMHO it makes sense to use the
latest OCaml version to build on that platform due to the support
status and number of fixes.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.
This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.
This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.
IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
| |\ \ |
|
| | |/
|/| |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
We now have only two notions of environments in the kernel: env and
safe_env.
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.
IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.
The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.
This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| |\ \ \ \ \ |
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | | |
We address the easy ones, but they should probably be all removed.
|
| | |/ / /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We remove the `fix N / cofix N` forms from the tactic language. This
way, these tactics don't depend anymore on the proof context, in
particular on the proof name, which seems like a fragile practice.
Apart from the concerns wrt maintenability of proof scripts, this also
helps making the "proof state" functional; as we don't have to
propagate the proof name to the tactic layer.
|
| |\ \ \ \ |
|
| | |_|_|/
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
comments.
[ci skip]
|
| | | | |
| | | |
| | | |
| | | | |
[ci skip]
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Clarification prompted by Jim Fehrle.
[ci skip]
|
| |\ \ \ \
| |/ / /
|/| | |
| | | | |
in CArray
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The `ide` folder contains two different binaries, the language server
`coqidetop` and `coqide` itself.
Even if these binaries are in the same folder, the only thing they
have in common is that they link to the protocol files. In the OCaml
world, having "doubly" linked files in the same project is considered
a bit of an ugly practice, and some build tools such as Dune disallow it.q
Thus, to clean up the build, we move the common protocol files to its
own library `ideprotocol`.
This helps towards Dune integration and towards having an IDE
standalone target, such as the one that was implemented here:
https://github.com/ejgallego/coqide-exp
|
| |\ \ \ |
|
| | |/ /
|/| | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This should hopefully alleviate memory problems on gitlab, by first
building the `lite` targets, and then building the remaining
not-that-big targets.
|
| |\ \ \
| |/ /
|/| |
| | | |
lib.cma).
|
| | | | |
|
| |\ \ \
| |/ /
|/| | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
packaging scripts.
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Théo Zimmermann
Matthieu Sozeau
Michael Soegtrop
Pierre-Marie Pédrot
Leonidas Lampropoulos
Maxime Dénès
Enrico Tassi
Hugo Herbelin
Jim Fehrle
Jason Gross