| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
|
| |
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't
miss anything.
|
| |
|
|
| |
So we avoid problems like the one in #7438.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
When invoking through Makefile we always rebuild dependencies. To skip
dependencies, invoke ci-wrapper directly. We make Circle CI do this.
In order to properly support invoking ci-wrapper directly we replace
"make" in ci-common by a bash function which adds -j to the make
invocation outside submakes. We also set TIMED in the ci-wrapper.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
This makes it so that when a ci target fails, we don't get red herring
error messages about .ok files not existing.
Since this requires bash, we make a helper script that invokes bash, so
as to not depend on bash in general.
|
| |/
|
|
|
| |
As per https://github.com/coq/coq/pull/968#discussion_r133238157 and
https://github.com/coq/coq/pull/969#discussion_r133241472
|
| |
|
|
| |
This puts the boilerplate all in one place
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| | |
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 development of @bmsherman tests universe polymorphism and setoid
rewriting in type, and should build with v8.6 and trunk.
|
| | |
|
| | |
|
| | |
|
| |
|
Andres Erbsen
Leonidas Lampropoulos
Jason Gross
Emilio Jesus Gallego Arias
Enrico Tassi
Beta Ziliani
Anton Trunov
Théo Zimmermann
Gaëtan Gilbert
Matthieu Sozeau
Ralf Jung
Maxime Dénès
Pierre-Marie Pédrot
Pierre Letouzey