aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2017-08-01Have coq-dpdgraph ci test print the differencesJason Gross
This allows better debugging when it fails.
2017-07-31Merge PR #746: Timing on ci via coq_makefile for various projectsMaxime Dénès
2017-07-28Merge PR #782: Update API for fiatMaxime Dénès
2017-07-21Alternate way of doing timing on ciJason Gross
This puts the boilerplate all in one place
2017-07-21Separate make from python script for HoTTJason Gross
HoTT still needs to use the submodule, but this will allow us to more easily see where the build fails, if it does
2017-07-21Display timing data travis for various projectsJason Gross
HoTT, which builds it's own makefile, and supports timing data, makes use of its own timing script. Everything else goes through the coq-bundled timing scripts.
2017-07-18[ci] VST is now built with IGNORECOQVERSION=true.Théo Zimmermann
2017-07-11Merge PR #858: [travis] Remove CompCert version check hack.Maxime Dénès
2017-07-05[travis] Remove CompCert version check hack.Emilio Jesus Gallego Arias
We now pass `-ignore-coq-version` to CompCert's configure (cf AbsInt/CompCert#188) , thanks to @xavierleroy .
2017-07-04Revert fiat-crypto overlayJason Gross
Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6.
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-20Merge PR#779: Each user overlay goes into its own file.Maxime Dénès
2017-06-16Remove -j ${NJOBS} from make invocations in the ciJason Gross
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 ```
2017-06-16Fix ci-fiat-crypto to have a proper lite targetJason Gross
The lite target depends on having the submodule cloned to generate the list of files to not build.
2017-06-16Each user overlay goes into its own file.Théo Zimmermann
This will avoid stupid merge conflicts in the future.
2017-06-15Merge PR#778: Revert "[travis] temporary UniMath overlay"Maxime Dénès
2017-06-15Update fiat-parsers overlayJason Gross
2017-06-15Remove bedrock from test suite.Maxime Dénès
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.
2017-06-14Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58Maxime Dénès
2017-06-14Temporary overlays because fewer plugins are loaded at startup.Maxime Dénès
2017-06-14[travis] overlay for fiat-crypto (a Require Import FunInd)Pierre Letouzey
2017-06-14[travis] overlays for CompCert and VST (an extra Require Export FunInd)Pierre Letouzey
2017-06-14[travis] fix Software Foundation (one added Require Extraction)Pierre Letouzey
2017-06-14[travis] fix CoLoR by inserting some Require Import FunIndPierre Letouzey
2017-06-14Temporary overlays for bignums.Maxime Dénès
2017-06-13Revert "[travis] temporary UniMath overlay"Théo Zimmermann
This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43. Not necessary anymore since UniMath/UniMath#715 has been merged.
2017-06-13[travis] overlay for cornPierre Letouzey
2017-06-13[travis] extra test ci-bignums (+factorize other scripts)Pierre Letouzey
2017-06-13[travis] overlay + extra deps for math-classes (and formal-topology)Pierre Letouzey
2017-06-13[travis] adapt CoLoR compilation to depend on the bignum packagePierre Letouzey
2017-06-13Merge PR#764: Point ci-hott at a newer version of HoTTMaxime Dénès
2017-06-12Merge PR#715: Add coq-dpdgraph ciMaxime Dénès
2017-06-12[travis overlay] Partially Revert 013c0232953f1f58Jason Gross
I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed
2017-06-12Temporary overlay, waiting for upstream PR merges.Maxime Dénès
2017-06-12add overlaysMatej Košík
2017-06-11Point ci-hott at a newer version of HoTTJason Gross
2017-06-08Mirror dpdgraph's travis test more accuratelyJason Gross
2017-06-08Remove coq-dpdgraph overlayJason Gross
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Remove overlay.Maxime Dénès
2017-06-07add overlaysMatej Košík
2017-06-06Overlay.Maxime Dénès
2017-06-06Remove some overlays.Maxime Dénès
2017-06-06Overlays.Maxime Dénès
2017-06-06Merge PR#723: [travis] [fiat] Test also fiat-core.Maxime Dénès
2017-06-02Add an overlay for coq-dpdgraph for 8.7Jason Gross
2017-06-02Add coq-dpdgraph CIJason Gross
2017-06-02[travis] [fiat] Test also fiat-core.Emilio Jesus Gallego Arias
I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
2017-05-31Adding overlay for math-comp.Hugo Herbelin
2017-05-29Merge PR#687: Gitlab CIMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 22:29:14 +0000