| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | rename ci-iris-coq -> ci-iris-lambda-rust |  Ralf Jung | 2017-10-19 |
| | | |||
| * | GitLab CI: make all_stdlib.v in build job |  Gaëtan Gilbert | 2017-10-05 |
| | | |||
| * | Fix GitLab CI |  Gaëtan Gilbert | 2017-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. | ||
| * | [ci] [gitlab] coq-dpdgraph: Remove allow-failure |  Jason Gross | 2017-08-24 |
| | | |||
| * | Add [opam update] and online repository to gitlab CI script. | Gaëtan Gilbert | 2017-07-21 |
| | | | | | | | | This allows it to find out about new packages / compilers without having to invalidate cache somehow. Additionally the latest camlp5 (7.01) is not in the local repository for some reason. | ||
| * | Merge PR #877: Travis+4.05.0 |  Maxime Dénès | 2017-07-20 |
| |\ | |||
| | * | [travis] Update testing to 4.05.0 + Camlp5 7.01 |  Emilio Jesus Gallego Arias | 2017-07-13 |
| | | | |||
| * | | Add timing scripts | Jason Gross | 2017-07-11 |
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds timing scripts from https://github.com/JasonGross/coq-scripts/tree/master/timing into the tools folder, and integrates them into coq_makefile and Coq's makefile. The main added makefile targets are: - the `TIMING` variable - when non-empty, this creates for each built `.v` file a `.v.timing` variable (or `.v.before-timing` or `.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively) - `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of sorted timings at the end, saving it to `time-of-build-pretty.log` - `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file `time-of-build-before.log` or `time-of-build-after.log`, respectively - `print-pretty-timed-diff` - prints a table with the difference between the logs recorded by `make-pretty-timed-before` and `make-pretty-timed-after`, saving the table to `time-of-build-both.log` - `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a table with the differences between two `.v.timing` files, and saves the output to `time-of-build-pretty.log` - `*.v.timing.diff` - this saves the result of `print-pretty-single-time-diff` for each target to the `.v.timing.diff` file - `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's own Makefile) - makes all `*.v.timing.diff` targets N.B. We need to make `make pretty-timed` fail if `make` fails. To do this, we need to get around the fact that pipes swallow exit codes. There are a few solutions in https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make; we choose the temporary file rather than requiring the shell of the makefile to be bash. | ||
| * | Merge PR#784: API additions for coq-dpdgraph | Maxime Dénès | 2017-06-19 |
| |\ | |||
| | * | Add coq-dpdgraph to gitlab CI | Gaëtan Gilbert | 2017-06-16 |
| | | | |||
| * | | Remove bedrock from test suite. | Maxime Dénès | 2017-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) |  Pierre Letouzey | 2017-06-13 |
| | | |||
| * | [travis] print failing test suite logs on failure | Gaëtan Gilbert | 2017-05-31 |
| | | |||
| * | [gitlab] Artifact test suite logs on failure. | Gaëtan Gilbert | 2017-05-30 |
| | | |||
| * | Gitlab CI | Gaëtan Gilbert | 2017-05-28 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |
path: root/.gitlab-ci.yml