| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Fix suggested by Hugo.
|
|
|
|
|
|
|
|
|
|
The status of a warning can now be set before the warning is declared
(typically by a plugin). However, I had to remove the "unknown warning"
warning.
|
|
|
|
|
|
|
|
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
```
|
|
Solution found by reading the question [Is it possible to “pass-through”
GNU make jobserver environment to a submake served via a 3rd-party
(non-make)](https://stackoverflow.com/q/29910944/377022).
This, I hope, will fix errors 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
```
which result from having a top-level `make` which sets up the jobserver
(via `-jN`), which invokes a non-makefile script *without passing on the
file descriptors for the jobserver*, which either invokes a makefile
script without `-jN` or invokes a makefile script with `-jN` which itself
invokes a submake without `-jN`. This was the case, for example, in
fiat-crypto.
|
|
The lite target depends on having the submodule cloned to generate the
list of files to not build.
|
|
|
|
This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Use an explicit label ~algebraic for make_flexible_variable as well.
|
|
Indeed, 8.6 is announced to be compilable with 4.01.0 and it is
convenient not seeing warnings about which nothing can be done.
Remove deprecation warnings new from ocaml 4.03, as well as warning 52.
This is a partial cherry-pick of a77734ad6.
|
|
|
|
The shell script configure was assuming the existence of option
-camldir which was removed in 333d41a9.
|
|
|
|
|
|
|
|
This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019),
"[zify] loops on dependent types"; before, we would see a `Z.of_nat (S
?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a
hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a
hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on
this.
This may not be the "right" fix (there may be cases where `zify` should
succeed where it still fails with this change), but this is a pure
bugfix in the sense that the only places where it changes the behavior
of `zify` are the places where, previously, `zify` looped forever.
|
|
|
|
|
|
(EDIT: for mutual fixpoints)
|
|
section variables.
|
|
|
|
|
|
|
|
|
|
Two issues in one:
- some focused_simpl were called on the wrong locations
- some focused_simpl were done on whole equations
In the two cases, this could be bad if "simpl" goes too far
with respect to what omega expects: later calls to "occurrence"
might fail. This may happen for instance if an atom isn't a variable,
but a let-in (b:=5:Z in the example).
|
|
|
|
|
|
Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug.
|
|
This fixes Théo's bug on eset.
|
