| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The amount of dangerous warnings in plugins is out of hand, including
some very serious ones.
As Coq developers are maintaining plugins these days it makes sense to
require the contributions to follow the same coding discipline as in
the main tree, thus we require the set of warnings fatal warnings to
be the same in Coq and in plugins.
We don't mark deprecation as fatal as to allow time for migration.
Fixes #6974
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
This was suggested by the author. See
https://github.com/bmsherman/topology/issues/23
|
|
|
|
|
|
pidetop relies on some rather low level API from STM, which we'd like to
change. It does not seem maintained much anymore, and still hasn't moved
to github.
|
|
This is convenient as to have better automation.
|
|
|
|
|
|
|
|
And fix a typo that was previously there.
|
|
This was kept as a fallback for some time, not worth keeping it
anymore as our GitLab setup seems mature and reliable enough.
|
|
This closes #7618.
|
|
|
|
There is the new pipeline, and the old pipeline. Most of what they
share in common is the (very large) library of lemmas about `Z`.
As per the discussion in
https://github.com/coq/coq/pull/8064#issuecomment-413474176 through
https://github.com/coq/coq/pull/8064#issuecomment-413793143
|
|
|
|
|
|
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't
miss anything.
|
|
So we avoid problems like the one in #7438.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
When invoking through Makefile we always rebuild dependencies. To skip
dependencies, invoke ci-wrapper directly. We make Circle CI do this.
In order to properly support invoking ci-wrapper directly we replace
"make" in ci-common by a bash function which adds -j to the make
invocation outside submakes. We also set TIMED in the ci-wrapper.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This makes it so that when a ci target fails, we don't get red herring
error messages about .ok files not existing.
Since this requires bash, we make a helper script that invokes bash, so
as to not depend on bash in general.
|
|
As per https://github.com/coq/coq/pull/968#discussion_r133238157 and
https://github.com/coq/coq/pull/969#discussion_r133241472
|
|
This puts the boilerplate all in one place
|
|
|
|
Solution found by reading the question [Is it possible to “pass-through”
GNU make jobserver environment to a submake served via a 3rd-party
(non-make)](https://stackoverflow.com/q/29910944/377022).
This, I hope, will fix errors such as
```
make[2]: *** write jobserver: Bad file descriptor. Stop.
make[2]: *** Waiting for unfinished jobs....
make[2]: *** write jobserver: Bad file descriptor. Stop.
make[1]: *** [coqprime] Error 2
make[1]: INTERNAL: Exiting with 1 jobserver tokens available; should be 2!
make[1]: Leaving directory `/home/travis/build/JasonGross/coq/_build_ci/fiat-c
```
which result from having a top-level `make` which sets up the jobserver
(via `-jN`), which invokes a non-makefile script *without passing on the
file descriptors for the jobserver*, which either invokes a makefile
script without `-jN` or invokes a makefile script with `-jN` which itself
invokes a submake without `-jN`. This was the case, for example, in
fiat-crypto.
|
|
Bedrock relies on the 8.4 compat flag that we are removing, and we heard
from MIT that they did not plan to port bedrock to more recent versions
of Coq.
|
|
|
|
|
|
|
|
This development of @bmsherman tests universe polymorphism and setoid
rewriting in type, and should build with v8.6 and trunk.
|
|
|
|
|
