| Commit message (Collapse) | Author | Age |
|\ |
|
| | |
|
|\ \
| | |
| | |
| | | |
with apt.
|
| |/
|/| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This should help towards ensuring that the system only has the
packages we specify in the Dockerfile.
We were missing:
- `git`: used in the CI system itself!
- `rsync`: used in the test-suite
- `python3-setuptools`, `python3-wheel`: necessary to use pip3
properly to install the missing python package.
- `autoconf`, `automake`: a few CI contribs depend on them.
|
|/ |
|
|\
| |
| |
| | |
points of Camlp5
|
| | |
|
|/
|
|
| |
This allows to append /archive at the end.
|
|\
| |
| |
| | |
constr in Constr
|
| | |
|
|/ |
|
|\ |
|
|\ \
| | |
| | |
| | | |
constants
|
| | | |
|
| | | |
|
| | | |
|
| |/
|/| |
|
|\ \ |
|
| |/
| |
| |
| | |
This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
|
|/
|
|
| |
See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
|
|\ |
|
| | |
|
|/ |
|
|\ |
|
|\ \
| | |
| | |
| | | |
to anomaly)
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We had mostly used absolute links in the past.
I just discovered that GitHub recommends using relative links instead:
https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links
and indeed my Emacs Markdown mode can handle relative links but doesn't
interpret absolute links relatively to the root of the git repository.
[ci skip]
|
| |/
|/|
| |
| | |
To be removed in 8.10.
|
| | |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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 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]
|