| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
bypassing dependencies
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
symlink from repo
|
|
And marginal improvements in the last section of the Gallina chapter.
|
|
|
|
|
|
|
|
|
|
|
|
Following the migration to Gitlab (#6919) we reduce Circle load, see
also discussion in #7436 and #7482.
|
|
This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
|
|
|
|
Fixes #7065
|
|
only-printing declarations.
|
|
|
|
|
|
It's redundant as a dependency of formal-topology.
|
|
|
|
|
|
Not only are most of "forall"s in the manual in Coq notation, but the
math notation leads to have a specially long space after the comma.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
They are now done on Gitlab CI. The test suite on Windows stays on
Appveyor.
|
|
We use a specific runner on Inria CloudStack. This allows us to have the
same build infrastructure setup for signed and unsigned binary packages.
The main Coq repository on Gitlab will produce unsigned binaries, using
a runner without secret. On my repository, a one-click operation will
sign the packages, making this part of the release process smoother.
|
|
|
|
|
|
|
|
|
|
|
|
|
