aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2017-11-20Add Equations to CIMatthieu Sozeau
2017-11-13Merge PR #6126: Fix ci-bignums.sh "missing ]" error.Maxime Dénès
2017-11-13Merge PR #6071: [ci] Add Ltac2Maxime Dénès
2017-11-09Fix ci-bignums.sh "missing ]" error.Gaëtan Gilbert
It made the test always fail so ci-common was always sourced. It's not quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure.
2017-11-04[ci] Add Ltac2Jason Gross
2017-10-30[ci] Switch VST back to upstream.Théo Zimmermann
This finally closes #5994.
2017-10-27[ci] Switch back to upstream version of Math-Classes and Corn.Théo Zimmermann
2017-10-25Merge PR #6003: Point HoTT back at master, which now supports Coq masterMaxime Dénès
2017-10-23Point HoTT back at master, which now supports Coq masterJason Gross
2017-10-20Switch testing branch back to CompCert upstream.Théo Zimmermann
This follows the merge of AbsInt/CompCert#191.
2017-10-19rename ci-iris-coq -> ci-iris-lambda-rustRalf Jung
2017-10-19CI: build lambdaRust (which depends on Iris) rather than just IrisRalf Jung
2017-10-10Merge PR #1067: Iris CI: use opam to install dependenciesMaxime Dénès
2017-10-09Merge PR #1117: [ci] Remove temporary bignums overlay.Maxime Dénès
2017-10-04[ci] Remove temporary bignums overlay.Théo Zimmermann
2017-10-03Fix GeoCoq build by using a shared CI configure.Théo Zimmermann
See also GeoCoq/GeoCoq#7.
2017-10-03Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileMaxime Dénès
2017-09-29start counting at 0...Ralf Jung
2017-09-29Iris CI: use opam to determine std++ git commitRalf Jung
2017-09-20In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gaëtan Gilbert
2017-09-15Merge PR #979: Fix install-doc target and other gitlab failuresMaxime Dénès
2017-09-13Fix GitLab CIGaëtan Gilbert
- timing needs time and python - check for compiled files without source looks in the install directory (except for make -f Makefile.ci which doesn't check), as such the install directory has been renamed to _install_ci and isn't searched.
2017-09-08Move README.ci and link to it from CONTRIBUTING.Théo Zimmermann
2017-09-07Merge PR #968: Better error messages on the CIMaxime Dénès
2017-09-07Merge PR #914: Making the detyper lazyMaxime Dénès
2017-09-07Trying to properly propagate errors in Windows CI script.Maxime Dénès
2017-09-05Make AppVeyor generate Windows package.Maxime Dénès
2017-09-05Fix Software Foundations build.Maxime Dénès
The Software Foundations archive has been replaced by three volumes.
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
2017-08-24Don't strip the newline, don't use \rJason Gross
Not sure entirely what it was supposed to do, but stripping the newline erased the following line
2017-08-24Swap order of "aggregating..." message and travis_foldJason Gross
Now the folded line starts with "Aggregating..." and not with "---------"
2017-08-24Only display travis_fold: on travisJason Gross
2017-08-15Move the rest of the ci target to a bash fileJason Gross
2017-08-15Better error messages on the CIJason Gross
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.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 20:45:46 +0000