| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \
| | |
| | |
| | | |
[travis] Add math-comp overlays, update CompCert to official version, add UniMath
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
We make math-comp overlays easier, we also start structuring the
scripts a bit more.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We extend `Stm.vernac_interp` so it can handle the commands it should
by level. This reenables `Show Script` handling, and this
interpretation function should handle more commands in the future such
as Load.
However note that we must first refactor the parsing state handling a
bit and remove the legacy `Stm.interp` before that.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| | |
Fix the ordering of the results in the output of Search to correspond
to the "priority" ordering.
|
| |\ \ |
|
| |/ / |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263.
String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
- A few tweaks of string are now done via the Bytes module
- lots of String.capitalize_ascii and co
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
No more pp_alias_spec et pp_alias_decl.
Instead, we use "include" and "module type of".
The extracted code might hence need OCaml 3.12 (quite rarely)
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Not_found)
This clarifies the execution flow
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
A double call to pp_module_type inside Ocaml.pp_specif was
causing an complexity blowup when pretty-printing heavily modular
extracted code.
I wasn't able to figure out why this double call is there. It could
be the leftover of some intermediate work in 2007 before commit 350398eae
(which introduced global printing phases Pre/Impl/Intf).
Anyway I'm reasonably sure that today these two pp_module_type calls produce
the exact same pretty-printed signature (even if there's a large bunch of
imperative states around). Moreover, this duplicated signature is actually
slightly wrong: when we alias a module M with a unambiguous name like Coq__123,
the type of Coq__123 should not be an exact copy of the type of M, but rather
a "strengthened" version of it (with equality between inductive types).
So the best solution is now to use this funny feature of OCaml introduced in 3.12 :
module Coq__123 : module type of struct include M end
This "module type of struct include" is slightly awkward, but short, correct,
and trivial to produce :-). And I doubt anybody will object to the (rare) use
of some 3.12 features in extracted code of 2017...
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15
minutes which is too much for Travis. Pity, because it was a nice use case.
|
| |\ \ \ \ \ |
|
| |/ / / / / |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Types were a bit difficult to read as they were mostly based on
anonymous products, this commit replaces them by named records and
refactors out some imperative code.
There is still quite a bit of room for improvement, but at least the
records provide a basis for more fine-grained understanding and
documentation.
|
| |\| | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
iris-coq math-classes sf
- [TLC] [metacoq] not ready for 8.6 yet
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Add README.ci
Suggestions and comments welcome.
- Use the system compiler to get some boot speedup.
- Build log folding.
- Set NJOBS=2 (very moderate speedup)
- Set language to a defined value.
OPAM itself recommends C, so we follow suit.
- Remove spurious `.opam`test
No harm in testing we are in the right opam setting even if the
cache did exist.
Anyways, it seems that the previous was spurious, as it was testing
if ~/coq/.opam did exists. I think the correct command would have
been:
```shell
[ -e ${HOME}/.opam ] || opam init ...
```
See the log at https://travis-ci.org/coq/coq/builds/198948812 for an
example.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Improve the setup to support external contribs.
We use a more minimalistic Coq build, gaining a few extra minutes.
- [math-comp] workaround `make -j` bug to enable parallel building.
|
| |/ / /
| | |
| | |
| | | |
We also optimize `travis_wait` use.
|
| |\ \ \ |
|
| | | | | |
|
| |/ / / |
|
| |\ \ \
| | | |
| | | |
| | | | |
Commits were squashed.
|
| |/ / / |
|
| |\ \ \ |
|
| | |\ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This was introduced in 8.5 while reorganizing the structure of
intro-patterns.
|
Maxime Dénès
Emilio Jesus Gallego Arias
Enrico Tassi
Arnaud Spiwack
Pierre Letouzey
Pierre-Yves Strub
Pierre-Marie Pédrot
Hugo Herbelin