| Commit message (Collapse) | Author | Age |
... | |
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
In the original Travis CI setup, the per-job time limit was an
issue. However, Gitlab has much improved this problem due to
a) Coq not being built for each contrib,
b) user-configurable time limit.
We thus disable the expensive builds from Travis:
`fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`,
`math-comp`, `unimath`, `vst`
and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`]
in full.
We also update the `math-comp` script as the `odd-order` theorem lives
in a separate repository and it is a key CI case.
|
| |_|_|/ / / / / / / / / / /
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
This is a "test" PR, but could be merged if we like it.
|
| |_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
This makes `coqidetop` behavior consistent with the one of
`coqtop`.
This was likely needed in the past when Coq used to print all kind of
stuff to stdout, including goal display. Now, it is not the case
anymore and this flag mainly controls printing verbosity.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
function
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
Co-Authored-By: @Zimmi48
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
Co-Authored-By: @Zimmi48
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
The readme is auto-generated by combining introductory text with the docstrings
in coqdomain.py.
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
Also get rid of a few unused or redundant constructs: the :ltac: role and the
'tac' directive (unused) and the :gallina: and :notation: roles (redundant).
|
| | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
Simpler
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
Actually there are more general instructions
|
| | | |_|_|_|_|_|_|/ / / / / /
| | |/| | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
bypassing dependencies
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
A docker-boot job is added which builds the docker image and pushes it
to the registry, the other jobs running on the image from the
registry.
The boot job reuses the already pushed image if it exists and matches,
this is important to cut down its runtime.
Making a new image takes 30min for all the switches
https://gitlab.com/SkySkimmer/coq/-/jobs/66650546
For testing I removed all jobs except boot and main build, and after
that run I built only the standard switch.
Building 1 switch takes around 20min
https://gitlab.com/SkySkimmer/coq/-/jobs/66656942
When the registry is up to date it takes 2min
https://gitlab.com/SkySkimmer/coq/-/jobs/66658790
(I don't know about all switches but probably no more than 5min)
Each pipeline pushes the image to $CI_REGISTRY_IMAGE:$CI_PIPELINE_ID
which is eg registry.gitlab.com/skyskimmer/coq:21557176 and is what
the other jobs use to run themselves.
For caching it pulls from and pushes to a constant name, in this test
$CI_REGISTRY_IMAGE:$CACHEKEY. We might also want to pull from the main
coq repo to avoid redoing work.
The question of having 1 image or 1 image/switch remains open.
Using the gitlab registry doesn't really work for circle CI, so the
dockerhub account would have to remain (or circle could return to an
opam-boot job, or be removed from our CI). There are similar concerns
with travis if we want to move it to docker.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | |
symlink from repo
|
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
And marginal improvements in the last section of the Gallina chapter.
|
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | |
We never actually used the -warn-error flag...
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|/ / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | |
Uses internal to Refiner remain.
|
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | | | | | | | | |
|