| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
We now pass `-ignore-coq-version` to CompCert's configure (cf
AbsInt/CompCert#188) , thanks to @xavierleroy .
|
|
Not a useful overlay. Fiat-crypto has since been updated to pass
-compat 8.6.
|
|
|
|
|
|
According to
https://www.gnu.org/software/make/manual/html_node/Options_002fRecursion.html#Options_002fRecursion
it's not necessary, because we pass `-j ${NJOBS}` to the top-level `make`
invocation in `.travis.yml`. Additionally, explicitly passing `-j` in,
e.g., fiat-crypto, results in error messages such as
```
make[2]: *** write jobserver: Bad file descriptor. Stop.
make[2]: *** Waiting for unfinished jobs....
make[2]: *** write jobserver: Bad file descriptor. Stop.
make[1]: *** [coqprime] Error 2
make[1]: INTERNAL: Exiting with 1 jobserver tokens available; should be 2!
make[1]: Leaving directory `/home/travis/build/JasonGross/coq/_build_ci/fiat-c
```
because the `-j` on the `make` in the `ci-fiat-crypto.sh` script
disables jobserver mode, and the submake in fiat-crypto to make coqprime
does not explicitly pass `-j`, and so reenables jobserver mode, and then
`make` gets very confused.
Commit made with
```bash
cd dev/ci
git grep --name-only -- 'make -j ${NJOBS}' | xargs sed s'/make -j \${NJOBS}/make/g' -i
git grep --name-only -- 'make -f Makefile.coq -j ${NJOBS}' | xargs sed s'/make -f Makefile.coq -j \${NJOBS}/make -f Makefile.coq/g' -i
```
|
|
The lite target depends on having the submodule cloned to generate the
list of files to not build.
|
|
This will avoid stupid merge conflicts in the future.
|
|
|
|
|
|
Bedrock relies on the 8.4 compat flag that we are removing, and we heard
from MIT that they did not plan to port bedrock to more recent versions
of Coq.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43.
Not necessary anymore since UniMath/UniMath#715 has been merged.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
|
|
|
|
|
|
|
|
We move Coqlib to library in preparation for the late binding of
Gallina-level references. Placing `Coqlib` in `library/` is convenient
as some components such as pretyping need to depend on it.
By moving we lose the ability to locate references by syntactic
abbreviations, but IMHO it makes to require ML code to refer to
a true constant instead of an abbreviation/notation.
Unfortunately this change means that we break the `Coqlib`
API (providing a compatibility function is not possible), however we
do so for a good reason.
The main changes are:
- move `Coqlib` to `library/`.
- remove reference -> term from `Coqlib`. In particular, clients will
have different needs with regards to universes/evar_maps, so we
force them to call the (not very safe) `Universes.constr_of_global`
explicitly so the users are marked.
- move late binding of impossible case from `Termops` to
`pretying/Evarconv`. Remove hook.
- `Coqlib.find_reference` doesn't support syntactic abbreviations
anymore.
- remove duplication of `Coqlib` code in `Program`.
- remove duplication of `Coqlib` code in `Ltac.Rewrite`.
- A special note about bug 5066 and commit 6e87877 . This case
illustrates the danger of duplication in the code base; the solution
chosen there was to transform the not-found anomaly into an error
message, however the general policy was far from clear. The long
term solution is indeed make `find_reference` emit `Not_found` and
let the client handle the error maybe non-fatally. (so they can test
for constants.
|
|
We are waiting for an upstream merge of a fix related to coq_makefile2.
|
|
|
|
|
