| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
|
|
Reviewed-by: MSoegtropIMC
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
We move from the previous complex CI download setup to a much more
straightforward public mirror repository.
Thanks to Yishuai Li and Benjamin Pierce for the very quick response.
Closes #12290
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: gares
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
After #12023 broke the bug minimizer, I'd like to add
[coq-tools](https://github.com/JasonGross/coq-tools/) to the CI. It's
relatively light-weight (under 5 minutes, I believe), and I'd like to
know when it's going to break on master before it's broken, rather than
after. It tests a relatively under-tested part of Coq, mostly (the
display output of error message, by and large), and I'm happy to take
responsibility for fixing it when some PR is going to break it (mainly I
just want a sort-of early warning system, and I want PRs to not
accidentally break it by changing things that they don't realize they're
changing).
|
|
|
|
Indeed, it would be intuitive that `Require Import Ltac` is an
equivalent for Ltac of `Require Import Ltac2.Ltac2`.
Also declaring the classic proof mode.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Specifically https://github.com/PrincetonUniversity/VST/commit/86d7ac6eaf9c580d5705c4257814f64560d24257
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
No diff to sources (luckily), see release notes at
https://discuss.ocaml.org/t/ann-ocamlformat-0-14-0/5435 for more
information.
|
|
|
|
It is unfortunate that we cannot install coqide and Dune 2.5.0 in < 4.07.0
|
|
|
|
autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124
|
|
Auto-generated files like the Makefile have recently been removed from
the sources (cf. coq-community/corn#88). Calling ./configure.sh is
now required.
|
|
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.
|
