| Age | Commit message (Collapse) | Author |
|---|
|
cc: #12350
|
|
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
|
|
Fixes #11936.
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
|
|
|
|
- use a different mirror for main cygwin archive
- (always) publish build log as artifact
- fix call to dune makefiles
- we do just build Coq for now, as:
+ dune is rebuilding Coq to run the test-suite, this needs move
investigation.
+ the test suite seems to take long and it times-out on Win.
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam
|
|
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
|
|
|
