| Age | Commit message (Collapse) | Author |
|---|
|
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
|
|
|
|
- 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
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
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: Zimmi48
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
|
|
|
|
|
|
|
|
Also fix an installation issue
|
|
|
|
The old script was still working but downloading an old version,
probably there is a git ref called trunk somewhere
|
|
|
|
|
|
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).
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
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
|
|
This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.
There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:
- moved leminv to `ltac_plugin`; this is unused in the core codebase
and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
later, for now I've introduced a `declareUctx` module to avoid being
invasive there.
In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.
This partially supersedes #10951 for now and helps with #11492 .
|
|
|
|
|
