aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2017-12-11Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.Maxime Dénès
2017-12-11Merge PR #6351: Fix a copy-paste error in ci-ltac2.Maxime Dénès
2017-12-11Merge PR #6346: [ci] CoLoR has moved to githubMaxime Dénès
2017-12-10[ci] Temporal workaround for checker non-backwards compatible change.Emilio Jesus Gallego Arias
2017-12-09[ci] Download ci-sf archives into the proper CI build dir.Emilio Jesus Gallego Arias
Currently, `make ci-sf` downloads and builds the files in the main root directory. we fix that.
2017-12-08Fix a copy-paste error in ci-ltac2.Théo Zimmermann
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-12-07[ci] CoLoR has moved to githubEmilio Jesus Gallego Arias
Closes #6194 .
2017-12-06Overlay for Equations.Gaëtan Gilbert
2017-11-30[ci] Test coqchk on the CompCert target.Théo Zimmermann
2017-11-28[ci] [vst] Shorten compilation time to avoid Travis timeouts.Emilio Jesus Gallego Arias
We remove the progs target [examples] to save time, we still build the full library thou. I guess we can't do better for now unless we get some Travis subscription.
2017-11-27Adding overlay for ltac2.Hugo Herbelin
2017-11-25Overlay for stronger restrict_universe_context.Gaëtan Gilbert
2017-11-24Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionMaxime Dénès
2017-11-23Adding ad hoc overlay for sf/vfa.Hugo Herbelin
2017-11-22[plugin] Remove LocalityFixme über hack.Emilio Jesus Gallego Arias
To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 20:40:27 +0000