| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ejgallego
|
|
Ack-by: Matafou
Reviewed-by: SkySkimmer
|
|
|
|
- problem with metacoq overlay ; it expects to send a non-ground
constant to the kernel, now it fails at prepare.
Record Sigma (A : Type) (B : A -> Type) : Type :=
{ fst : A ; snd : B fst }.
Arguments fst {A B}.
Arguments snd {A B}.
Quote Recursively Definition foo := (fst, snd).
There is a hack on the overlay, we need to discuss it a bit more.
|
|
|
|
I believe a recent commit to master broke it, and now that it's no
longer tested as part of fiat-crypto-legacy, I think it's time to add
it.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
We include the `version=0.13.0` field that should help users not to
use the wrong version. `disable=true` still seems a noop with `dune`.
There are some minor changes in the way comments are formatted; I'm
unsure if this is due to the `wrap-comments` option; as always; tweaks
to the config are most welcome.
|
|
There is a lot of check overhead in the code, we will try to provide a
more convenient API for manipulation of remaining obligations.
|
|
|
|
|
|
That release includes non trivial changes related C compilers, in
particular due to `-fno-common` support.
|
|
|
|
|
|
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
|
|
|
|
New versions did remove the autogen.sh script in favor of plain
`autoreconf`
Note that the Coquelicot build documentation seems incorrect.
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: mattam82
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
No reason to have them in the same .sh
|
|
|
|
|
|
Motivations:
- We should have only maintained developments in our CI
- `make ci-fiat-crypto-legacy` takes about 15 mins before the first call
to `coqc`, making it unusable to work on overlays
- The coding style of this development is so fragile that adapting to
any change of behavior requires diffing gigabytes of Ltac traces.
@mattam82 and I have been blocked for 6 months this way, when working on
unifall.
I understand this development was meant to stress-test some components
like printing, but I think the trade-off is bad. We should rather come
up with specialized test suites for these components.
|
|
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes
|
|
|
|
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
|
|
|
|
Fiat-Crypto does not guarantee compatibility with the tip of bedrock2,
only with the pinned version, and bedrock2 is still relatively unstable.
So we make the CI not have Fiat-Crypto depend on bedrock2, and instead
use the pinned submodule, by using `EXTERNAL_REWRITER=1
EXTERNAL_COQPRIME=1` rather than `EXTERNAL_DEPENDENCIES=1`.
|
|
It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.
Fixes #9390: What is the purpose of the function "kind_of_type"?
|
|
Co-Authored-By: Jason Gross <jasongross9@gmail.com>
|
|
The computation of which files to build is now mostly cached rather than
computed, eliminting basically all of the wait-time from `make` to the
first invocation of `coqc`.
Note that we no longer need to invoke
`./etc/ci/remove_autogenerated.sh`, but it does not hurt, and it speeds
up `coqdep` somewhat significantly.
Fixes #9298
|
|
Contributors are *not* required to prepare all the patches by
themselves. They can request help from project authors, who should be
ready to take part in this.
Also, finish replacing "development" by the more appropriate word
"project".
|
