| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
|\ \ \ |
|
| | | | |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | |/ / |
|
| | | | | | | |
|
| | | |_|/ /
| | |/| | | |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | |
|
| | | | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Primitive projections were not correctly unfolded, leading to failure of
conversion checks in some cases. The kernel was strangely not affected by
this bug, and it was probably a remnant of some vestigial code.
|
| |_|_|_|_|_|_|_|/ /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
The constant_value function was actually not behaving the same as
constant_value_in w.r.t. projections. The former was not used, and
the only place that used the latter was in Tacred and was statically
insensitive to the use of projections.
|
| | | | | | | | | | |
|
| |_|_|_|_|/ / / /
|/| | | | | | | | |
|