| Age | Commit message (Collapse) | Author |
|---|
|
|
|
VernacDefinition
|
|
|
|
|
|
We allow to provide a Coq load path at document creation time. This is
natural as the document naming process is sensible to a particular
load path, thus clarifying this API point.
The changes are minimal, as #6663 did most of the work here. The only
point of interest is that we have split the initial load path into two
components:
- a ML-only load path that is used to locate "plugable" toplevels.
- the normal loadpath that includes `theories` and `user-contrib`,
command line options, etc...
|
|
Refinement of the toplevel codepath requires to be more careful about
the conditions for coqtop to be interactive.
Fixes #6691. We also tweak the vio auxiliary function.
|
|
This definitely qualifies as a micro-optimization, but it would not be
performed by Flambda. Indeed, it is unsound in general w.r.t. OCaml
semantics, as it involves a fixpoint and changes potential non-termination.
In our case it doesn't matter semantically, but it is indeed observable
on computation intensive developments like UniMath.
|
|
We can do this after the parent commit (Reductionops.nf_* don't use
empty env)
|
|
|
|
This just shares the unfold_projection between Closure and Reduction.
|
|
|
|
- use Redflags.red_projection
- share unfold_projection between CClosure and Reduction
|
|
This heuristic is justified by the fact that during a conversion check
between a flexible and a rigid term, the flexible one is eventually going
to be fully weak-head normalized. So in this case instead of performing
many small reduction steps on the flexible term, we perform full weak-head
reduction, including delta.
It is slightly more efficient in actual developments, and it fixes a corner
case encountered by Jason Gross.
Fixes #6667: Kernel conversion is much, much slower than `Eval lazy`.
|
|
|
|
error msg
|
|
|
|
|
|
|
|
|
|
|
|
The type discipline of the tactic monad does not distinguish between
mono-goal and multi-goal tactics. Unfortunately enter_one "asserts
false" if called on 0 or > 1 goals. The __LOC__:string argument can
be used to make the error message more helpful (since the backtrace is
pointless inside the monad).
The intended usage is "Goal.enter_one ~__LOC__ (fun gl -> ..".
The __LOC__ variable is filled in by the OCaml compiler with the current
file name and line number.
|
|
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.
|
|
|
|
|
|
|
|
|
|
The old semantics of `with/without_option` allowed the called function
to modify the value of the option. This is an issue mainly with the
`silently/verbose` combinators, as `Set Silent` can be executed under
one of them and thus the modification will be lost in the updated code
introduced in a554519874c15d0a790082e5f15f3dc2419c6c38
IMHO these kind of semantics are quite messy but we have to preserve
them in order for the `Silent` system to work. In fact, note that in
the previous code, `with_options` was not consistent with
`with_option` [maybe that got me confused?]
Ideally we could restore the saner semantics once we clean up the
`Silent` system [that is, we remove the flag altogether], but that'll
have to wait.
Fixes #6645.
|
|
There is no way today to distinguish primitive projections from
compatibility constants, at least in the case of a record without
parameters.
We remedy to this by always using the r.(p) syntax when printing
primitive projections, even with Set Printing All.
The input syntax r.(p) is still elaborated to GApp, so that we can preserve
the compatibility layer. Hopefully we can make up a plan to get rid of that
layer, but it will require fixing a few problems.
|
|
|
|
|
|
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.
|
|
|
|
Fixes BZ#5726.
|
|
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"
|
|
|
|
|
|
|
