aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ci
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* ci: add elpiGravatar Enrico Tassi2018-02-19
|
* Fix ci-all targetGravatar Gaëtan Gilbert2018-01-10
|
* Fix CI with parallel make (messed up dependencies)Gravatar Gaëtan Gilbert2017-12-21
| | | | | | | | | 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.
* Put bignums, math-classes and corn dependencies in MakefileGravatar Gaëtan Gilbert2017-12-13
|
* Add Equations to CIGravatar Matthieu Sozeau2017-11-20
|
* [ci] Add Ltac2Gravatar Jason Gross2017-11-04
|
* rename ci-iris-coq -> ci-iris-lambda-rustGravatar Ralf Jung2017-10-19
|
* Merge PR #968: Better error messages on the CIGravatar Maxime Dénès2017-09-07
|\
| * Move the rest of the ci target to a bash fileGravatar Jason Gross2017-08-15
| |
| * Better error messages on the CIGravatar Jason Gross2017-08-15
| | | | | | | | | | | | | | | | 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.
* | Fix a typoGravatar Jason Gross2017-08-15
|/ | | | | As per https://github.com/coq/coq/pull/968#discussion_r133238157 and https://github.com/coq/coq/pull/969#discussion_r133241472
* Alternate way of doing timing on ciGravatar Jason Gross2017-07-21
| | | | This puts the boilerplate all in one place
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
| * Pass GNU Make jobserver on to the ci jobsGravatar Jason Gross2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Remove bedrock from test suite.Gravatar Maxime Dénès2017-06-15
| | | | | | | | | | | | 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.
* | [travis] extra test ci-bignums (+factorize other scripts)Gravatar Pierre Letouzey2017-06-13
| |
* | Add coq-dpdgraph CIGravatar Jason Gross2017-06-02
| |
* | Reformat Makefile.ciGravatar Jason Gross2017-05-31
|/
* Add bmsherman/topology to the ciGravatar Jason Gross2017-05-01
| | | | | This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk.
* Add bedrock targets src and facadeGravatar Jason Gross2017-04-20
|
* [travis] Backport from trunk: VSTGravatar Emilio Jesus Gallego Arias2017-03-24
|
* [travis] [8.6.only] Backport latest changes from trunk.Gravatar Emilio Jesus Gallego Arias2017-03-22
|
* [travis] Backport trunk's travis support.Gravatar Emilio Jesus Gallego Arias2017-03-02