aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci
Commit message (Collapse)AuthorAge
...
* | | | | | [ci] Temporal workaround for checker non-backwards compatible change.Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | |
| | | * | | [ci] Download ci-sf archives into the proper CI build dir.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | Currently, `make ci-sf` downloads and builds the files in the main root directory. we fix that.
| | * | | Fix a copy-paste error in ci-ltac2.Gravatar Théo Zimmermann2017-12-08
| | | | |
* | | | | Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\ \ \ \ \
| | * | | | [ci] CoLoR has moved to githubGravatar Emilio Jesus Gallego Arias2017-12-07
| |/ / / / |/| | | | | | | | | | | | | | Closes #6194 .
| | | * | Overlay for Equations.Gravatar Gaëtan Gilbert2017-12-06
| |_|/ / |/| | |
* | | | [ci] Test coqchk on the CompCert target.Gravatar Théo Zimmermann2017-11-30
| | | |
* | | | [ci] [vst] Shorten compilation time to avoid Travis timeouts.Gravatar Emilio Jesus Gallego Arias2017-11-28
| |_|/ |/| | | | | | | | | | | | | | | | | | | | 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.
| * | Adding overlay for ltac2.Gravatar Hugo Herbelin2017-11-27
| |/
* / Overlay for stronger restrict_universe_context.Gravatar Gaëtan Gilbert2017-11-25
|/
* Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionGravatar Maxime Dénès2017-11-24
|\
| * Adding ad hoc overlay for sf/vfa.Gravatar Hugo Herbelin2017-11-23
| |
* | [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
|/ | | | | | | | | | 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.
* Add Equations to CIGravatar Matthieu Sozeau2017-11-20
|
* Merge PR #6126: Fix ci-bignums.sh "missing ]" error.Gravatar Maxime Dénès2017-11-13
|\
* \ Merge PR #6071: [ci] Add Ltac2Gravatar Maxime Dénès2017-11-13
|\ \
| | * Fix ci-bignums.sh "missing ]" error.Gravatar Gaëtan Gilbert2017-11-09
| |/ |/| | | | | | | 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.
| * [ci] Add Ltac2Gravatar Jason Gross2017-11-04
| |
* | [ci] Switch VST back to upstream.Gravatar Théo Zimmermann2017-10-30
|/ | | | This finally closes #5994.
* [ci] Switch back to upstream version of Math-Classes and Corn.Gravatar Théo Zimmermann2017-10-27
|
* Merge PR #6003: Point HoTT back at master, which now supports Coq masterGravatar Maxime Dénès2017-10-25
|\
| * Point HoTT back at master, which now supports Coq masterGravatar Jason Gross2017-10-23
| |
* | Switch testing branch back to CompCert upstream.Gravatar Théo Zimmermann2017-10-20
| | | | | | | | This follows the merge of AbsInt/CompCert#191.
* | rename ci-iris-coq -> ci-iris-lambda-rustGravatar Ralf Jung2017-10-19
| |
* | CI: build lambdaRust (which depends on Iris) rather than just IrisGravatar Ralf Jung2017-10-19
|/
* Merge PR #1067: Iris CI: use opam to install dependenciesGravatar Maxime Dénès2017-10-10
|\
* \ Merge PR #1117: [ci] Remove temporary bignums overlay.Gravatar Maxime Dénès2017-10-09
|\ \
| * | [ci] Remove temporary bignums overlay.Gravatar Théo Zimmermann2017-10-04
| | |
* | | Fix GeoCoq build by using a shared CI configure.Gravatar Théo Zimmermann2017-10-03
|/ / | | | | | | See also GeoCoq/GeoCoq#7.
* | Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileGravatar Maxime Dénès2017-10-03
|\ \
| | * start counting at 0...Gravatar Ralf Jung2017-09-29
| | |
| | * Iris CI: use opam to determine std++ git commitGravatar Ralf Jung2017-09-29
| |/ |/|
* | In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gravatar Gaëtan Gilbert2017-09-20
| |
* | Merge PR #979: Fix install-doc target and other gitlab failuresGravatar Maxime Dénès2017-09-15
|\ \
| * | Fix GitLab CIGravatar Gaëtan Gilbert2017-09-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | - 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.
* | | Move README.ci and link to it from CONTRIBUTING.Gravatar Théo Zimmermann2017-09-08
| | |
* | | Merge PR #968: Better error messages on the CIGravatar Maxime Dénès2017-09-07
|\ \ \
* \ \ \ Merge PR #914: Making the detyper lazyGravatar Maxime Dénès2017-09-07
|\ \ \ \
| | | | * Trying to properly propagate errors in Windows CI script.Gravatar Maxime Dénès2017-09-07
| |_|_|/ |/| | |
* | | | Make AppVeyor generate Windows package.Gravatar Maxime Dénès2017-09-05
| | | |
* | | | Fix Software Foundations build.Gravatar Maxime Dénès2017-09-05
| |_|/ |/| | | | | | | | The Software Foundations archive has been replaced by three volumes.
| * | Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Don't strip the newline, don't use \rGravatar Jason Gross2017-08-24
| | | | | | | | | | Not sure entirely what it was supposed to do, but stripping the newline erased the following line
| * Swap order of "aggregating..." message and travis_foldGravatar Jason Gross2017-08-24
| | | | | | | | | | Now the folded line starts with "Aggregating..." and not with "---------"
| * Only display travis_fold: on travisGravatar Jason Gross2017-08-24
| |
| * 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.
* | Have coq-dpdgraph ci test print the differencesGravatar Jason Gross2017-08-01
|/ | | | This allows better debugging when it fails.
* Merge PR #746: Timing on ci via coq_makefile for various projectsGravatar Maxime Dénès2017-07-31
|\
* \ Merge PR #782: Update API for fiatGravatar Maxime Dénès2017-07-28
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 01:05:56 +0000