| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Like circle CI we install every opam package in opam-boot jobs (one
per switch).
This should be more reliable with less issues from outdated cache.
Also avoid messing with symlinks through OPAMROOT (we can't
cache/artifact files outside the coq directory).
Avoid using "system" compiler (no risk of getting an upgrade through
the base image).
|
| |
|
|
|
|
|
|
|
|
| |
When `build` was made to build the doc it dropped `-coqide opt` and
dropped the environment variables for building coqide.
The combination means that when the cache had lablgtk in
opam (installed by some other job) configure would pick it up but the
system package wouldn't be there causing a failure. When lablgtk isn't
in the cache everything was fine.
|
| | |
|
| |
|
|
|
| |
Previously it was installed for the compilation jobs causing random
failures when the other jobs got a cache without it.
|
| | |
|
| |
|
|
| |
The config/Makefile is carried over by artefacts.
|
| |
|
|
| |
Closes #6194 .
|
| |
|
|
|
|
| |
This avoids mixing native and byte compilation as the debug printers
are always byte compiled and the tools have no .byte rule, only the
OCAMLBEST rule.
|
| |
|
|
|
| |
Hopefully this will stop the intermittent
test-suite/coq-makefile/findlib-package failures.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.
We also refactor travis to test more lablgtk versions.
We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.
Fixes #6140.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
- 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.
|
| | |
|
| |
|
|
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| |
|
Beta Ziliani
Anton Trunov
Gaëtan Gilbert
Maxime Dénès
Enrico Tassi
Emilio Jesus Gallego Arias
Matthieu Sozeau
Jason Gross
Ralf Jung
Gaëtan Gilbert
Pierre Letouzey