| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
We gather (almost) all the STM options in a record, now set at
document creation time.
This is refactoring is convenient for some other ongoing
functionalization work.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
menhir.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
records for cbv and native_compute
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Fixes #5286 (last remaining part).
|
| | |_|_|_|/ / / / / /
|/| | | | | | | | | |
|
| | |_|_|_|_|_|/ / /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
We refactor top-level load path handling. This is in preparation to
make load paths become local to a particular document.
To this effect, we introduce a new data type `coq_path` that includes
the full specification of a load path:
```
type add_ml = AddNoML | AddTopML | AddRecML
type vo_path_spec = {
unix_path : string; (* Filesystem path contaning vo/ml files *)
coq_path : Names.DirPath.t; (* Coq prefix for the path *)
implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *)
has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *)
}
type coq_path_spec =
| VoPath of vo_path_spec
| MlPath of string
type coq_path = {
path_spec: coq_path_spec;
recursive: bool;
}
```
Then, initialization of load paths is split into building a list of
load paths and actually making them effective. A future commit will
make thus the list of load paths a parameter for document creation.
This API is necessarily internal [for now] thus I don't think a
changes entry is needed.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
We separate functions dealing with VM values (vmvalues.ml) and
interfaces of the bytecode interpreter (vm.ml). Only the former relies
on untyped constructions.
This also makes the VM architecture closer to the one of native_compute,
another patch could probably try to share more code between the two for
conversion and reification (not trivial, though).
This is also preliminary work for integers and arrays.
|
| | | | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Fixes #5747: "make validate" fails with "bad recursive trees"
|
| | | | | | | | | | |
|
| | |_|_|_|_|/ / /
|/| | | | | | | |
|
| | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \
| |_|_|_|/ / / / / /
|/| | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|/ /
|/| | | | | | | | | |
|
| | |_|_|/ / / / / /
|/| | | | | | | | |
|
| | |_|/ / / / / /
|/| | | | | | | |
|
| | |_|_|_|/ / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The implementation of the subterm relation for primitive projections was
a bit wrong. I found the problem independently of this bug, and tried to
see if a proof of False could be derived, but I don't think so, due to
another check (check_is_subterm) that saves the kernel at the last
minute.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
sudo apt-get install will fail on gcc-multilib if apt-get update cannot
fetch launchpad, so instead we delay installing these packages.
|
| | |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Script modified from
https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status
I stuck the code in "install" rather than "before_install" so that the
lint target didn't need to be changed. I also haven't touched the
targets that add more packages; I'll leave that to someone who knows
more about the "&" and "*" syntax being used in the configuration.
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | | |
These tests are already done by CircleCI.
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
for primitive projections
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
pr_lname
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
When asking for a hint about bullets, we check
that there is an ongoing proof.
|
| | | | | | |/ / / |
|
| | | | | | | | | |
|
| | | | |_|/ / /
| | |/| | | | |
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | | |
|
| | |_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | |
|
| | | | | | | | | | | | | |
|
Emilio Jesus Gallego Arias
Maxime Dénès
Gaëtan Gilbert
Pierre-Marie Pédrot
Jason Gross
Ralf Jung
Théo Zimmermann
Cyprien Mangin
Vincent Laporte