| Age | Commit message (Collapse) | Author |
|---|
|
This ensures that the log will contain the commit hash that we tested.
This reuses the method from the Windows build script (we have a number
of common functions, it would be interesting to start a bash shared
library file).
|
|
Reviewed-by: SkySkimmer
|
|
Since a long time the compiler switch is not very useful as it is not
used to test any CI.
The `edge+flambda` version seems stable enough to carry out the `edge`
testing by itself, thus we remove the `egde` switch saving valuable
Docker image size and Gitlab runners.
We also tweak the `pkg:opam` job as to correctly set the version of
the pinned local package.
|
|
I think the usage looks cleaner this way.
|
|
In order to do so we place the polymorphic status and name in the
read-only part of the monad.
Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.
Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.
Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.
|
|
Reviewed-by: maximedenes
|
|
passed
https://gitlab.com/coq/coq/-/jobs/158737429
|
|
COQMF_ARGS is a bedrock2-specific name to pass extra arguments to coq_makefile,
and we use VERBOSE=1 for better debuggability
|
|
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
Coq and the Coq libraries can now be excluded
(by setting the NOCOQ environment variable).
|
|
|
|
|
|
|
|
suite again
|
|
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
We're recently reorganized fiat-crypto. This should fix the OOM CI
issues.
Fixes #9338
|
|
Move plugin tutorial to Coq repo
|
|
Once https://github.com/mit-plv/fiat-crypto/pull/477 is merged, the
master branch will no longer contain the files nor the targets for
fiat-crypto legacy. (We should perhaps consider moving fiat-crypto
legacy to coq-community as a source of vm and printing tests.)
|
|
|
|
|
|
|
|
This was suggested by the author. See
https://github.com/bmsherman/topology/issues/23
|
|
|
|
|
|
This changes the semantics a bit since we don't have
TRAVIS_COMMIT_RANGE anymore, instead we do per-commit linting for the
commits since the last merge commit.
|
|
Try to mimick MSoegtropIMC
(https://github.com/coq/coq/pull/9243#issuecomment-448968353 )
|
|
|
|
|
|
|
|
|
|
workers
|
|
|
|
|
|
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`]
CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit`
cannot be currently installed, thus we have to add a switch to the
test suite to disable `unit-tests`.
Many deprecation warnings happened in 4.08 so we use the `release`
profile to make them not fatal. Using a 4.08 build profile would be an
option too.
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
|
|
This is a reduced version of #8503 as to provide a way to build the
reference manual with Dune.
Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.
This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in #8503.
Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.
|
