| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
|
|
|
|
Reviewed-by: mattam82
Ack-by: Zimmi48
|
|
|
|
As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.
It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.
We thus remove all bitrotten dead code.
|
|
|
|
|
|
to check for conversion
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
|
|
Instead of taking a type and checking that the inferred type for the expression
is correct, we simply pick an optional constraint and return the type directly
in the callback. This prevents having to compute type conversion twice in the
special case of Ltac2 variable quotations.
This should be 1:1 equivalent to the previous code, we are just moving code
around.
|
|
The table of coercion classes (`class_tab`) has been extended with information
about reachability. The conversion checking of a pair of multiple inheritance
paths (of coercions) will be skipped if these paths can be reduced to smaller
adjoining pairs of multiple inheritance paths, and this reduction will be
determined based on that reachability information.
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego
|
|
`coe_source` and `coe_target` fields of type `cl_typ` have been added to
`coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a
coercion. The `coercion` record has also been replaced with `coe_info_typ`.
|
|
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: gares
Ack-by: LasseBlaauwbroek
Ack-by: silene
Ack-by: vbgl
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
raised.
Reviewed-by: jfehrle
|
|
|
|
native_compute is called.
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
called (fix #13849).
The libraries are eventually linked in native_norm and native_conv_gen,
just before mk_norm_code and mk_conv_code are called.
This commit also renames call_linker as execute_library to better reflect
its role. It also makes link_library independent from it, since their
error handling are completely opposite.
|
|
|
|
|
|
Otherwise, the interpreter sees already unified evars as accumulators
rather than actual constants, thus preventing the computations from
progressing.
This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed
evar normalization. The effect went unnoticed because the computed term is
still convertible to the reduced term, except that it is the lazy
machinery that ends up reducing it, rather than the bytecode one.
So, performances became abysmal, seemingly at random.
|
|
Reviewed-by: ppedrot
|
|
Towards #5154 (but insufficient)
|
|
Reviewed-by: ppedrot
|
|
|
|
Instead of storing the bare fixpoint and its unfolded body in the term,
incurring a cost for their lifts under contexts, we simply store them
in the side map used to track the relation between a fresh problem evar
and its minimal arity. We also replace the hacky evarmap used to track
instantiation with a mere set.
|
|
|
|
|
|
Reviewed-by: mattam82
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
|
|
We know statically that whd_betaiota is a local reduction function, so it
does not need to access the rel_context of its environment argument.
|
|
|
|
This also allows to move the strong variant of cbn to the Cbn module.
|
|
Also works for simpl.
|
|
|
|
|
|
|
|
It is equivalent but makes the code more similar to the PCase vs. Case case (aha).
|
|
|
|
This partially fixes #13732 and matches what we do in detype_sort
|
|
The infamous whd_betaiota_deltazeta_for_iota_state function is critical for
unification, and it seems that eagerly reducing let-bindings appearing in
case branches was a bad idea for efficiency. Instead, when try to preserve
the old behaviour where a dummy beta-let cut was introduced.
|
|
Since we have eta-expansion guaranteed by the term representation, we do
not have any more to do a little dance to try to recognize eta-expanded
branches and return predicate.
Still not able to compile the elpi test, but a good step towards it.
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
