| Age | Commit message (Collapse) | Author |
|---|
|
|
|
symlink from repo
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Currently, `configure.ml` does copy/link some files from `kernel` to
`checker` in an ad-hoc way. Instead, it is preferable to add a copy
rule to make and let it handle the dependencies properly.
This also fixes a dependency bug in Windows, as files wouldn't be
properly refreshed if `configure` was not run each time.
|
|
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't
miss anything.
|
|
|
|
|
|
and indentation.
|
|
requested compiler.
|
|
|
|
OpenBSD mktemp fails with an error otherwise.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
