| Commit message (Collapse) | Author | Age |
... | |
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | |
|
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
since it affects scheduling (actually the error the option lets one
silence)
|
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
It is not clear yet that support for nested proofs will actually get removed in a future version.
|
| |_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | |
|
| |_|/ / / / / / / / / /
|/| | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
As pointed out by @MSoegtropIMC
[here](https://github.com/coq/coq/pull/7522#issuecomment-389478963)
there are not needed to build the packages, so not building them will
save a couple of minutes.
|
| | | | | | | | | | | | | | | |
|
| |_|_|_|_|/ / / / / / / / /
|/| | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
are on Gitlab.
|
| | | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
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
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|