| Age | Commit message (Collapse) | Author |
|---|
|
Fix #13354
This change is very specific to array, but should not be a significant
obstacle to generalization of the feature to eg axioms if we want to later.
|
|
BTW it was incorrect (array needs an instance)
|
|
not only on subidentifiers of an identifier
Reviewed-by: Zimmi48
|
|
There was not any difference between those after the cleanup patches that
come before.
|
|
It was a hidden invariant of the code.
|
|
|
|
Polymorphic side-effects generated in monomorphic mode would be counted towards
trusted subcomponents. This would allow to make ill-typed terms pass as
legitimate by mimicking the shape of the inlining of monomorphic side-effects in
such a proof.
|
|
|
|
Instead we store that data in the native code that was generated in adapt
the compilation scheme accordingly. Less indirections and less imperative
tinkering makes the code safer.
The global symbol table was originally introduced in #10359 as a way not to
depend on the Global module in the generated code. By storing all the
native-related information in the cmxs file itself, this PR also makes other
changes easier, such as e.g. #13287.
|
|
are in custom output path
Reviewed-by: maximedenes
Reviewed-by: herbelin
|
|
|
|
No need to zip the stack if the machine has made no progress.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
By no means a float is a neutral value. When put inside a Zprimitive context
it can trigger computation.
|
|
A partially applied primitive was considered CClosure.Norm, i.e. neutral. But
this is not true, because substituting this term as the head of an application
may trigger further reduction. In this respect, primitive functions behave like
fixpoints.
|
|
Not sure if we can get a bug from this omission.
|
|
|
|
|
|
|
|
We introduce a module type not to have to redeclare CanOrd, UserOrd and
SyntacticOrd all over the place.
|
|
|
|
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
|
|
|
|
|
|
This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
|
|
For now it does not do anything but eventually it should be used to replace
the reliance on canonical names for dual kerpairs such as e.g. constants and
inductive types.
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: SkySkimmer
|
|
output path
In #11581 we introduced the `-native-output-dir` option to allow the
build system to redirect the output of the native compiler.
Unfortunately that patch also modified the default loadpath, which is
now buggy if a library with native is installed.
We thus revert the change to the loadpath handling, so for now
additional native build paths have to be passed with `-nI`.
Note that unfortunately in `link_library` we don't know if the
required library is coming from the build dir or from an installed
dir, as this information is generated from `Require` statements in
`Library.get_used_load_paths`. We thus check and give priority to
files in the build location.
As to make the patch backportable I introduced an extra `stat` system
call which should not be problematic as the cache will be hot for the
second call.
An alternative would be actually to modify loadpath compilation in
`call_compiler` so both include paths would be added if `output_dir`
is not the default, however that seems pretty noisy given the large
path set returned by `!get_load_paths`.
|
|
Reviewed-by: erikmd
Reviewed-by: silene
|
|
parameters in safe_env
Reviewed-by: herbelin
|
|
Reviewed-by: mattam82
Ack-by: Janno
Ack-by: gares
|
|
|
|
|
|
We know statically that the first thing the conversion algorithm is going to
do is to get it from the provided function, so we simply explicitly pass it
around.
|
|
Reviewed-by: ejgallego
Reviewed-by: silene
|
|
This fixes #12623 (bidirectionality breaks impredicativity).
|
|
Reviewed-by: ppedrot
|
|
The safe environment features two different sets of delta resolvers, one for
module parameters and one for the actual body of the module being built. The
purpose of this separations seems to have been to reduce the number of name
equations being added to the environment, since the one from the parameters
would already be present at instanciation time.
Semantically, required modules behave like parameters in this respect, i.e.
delta resolvers that come from modules dependend upon are guaranteed to be added
when that module is actually required. As such, there is no need to store the
quotient coming from the dependencies inside the vo file of a given library.
Yet, the previous code would precisely do that, leading to a potential quadratic
blowup in vo file size, similarly to the issue with vio files storing the whole
chain of dependency. This patch fixes the issue simply by segregating those
redundant constraints in the dedicated field, thus dropping them from the vo.
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
|
|
Semi-persistent arrays are supposed to have amortized O(1) complexity.
This commit ensures it, without forcing the user to litter its functions
with explicit calls to reroot.
This commit also makes rerootk faster by carrying the array along the
dependency chain rather than recomputing it at every step.
|
|
C functions were used for floating-point arithmetic operations, by
fear of double rounding that could happen on old x87 on 32 bits
architecture. This commit uses OCaml floating-point operations on 64
bits architectures.
The following snippet is made 17% faster by this commit.
From Coq Require Import Int63 BinPos PrimFloat.
Definition foo n :=
let eps := sub (next_up one) one in
Pos.iter (fun x => add x eps) two n.
Time Eval native_compute in foo 1000000000.
|
|
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
|
|
Fix #13086.
|
|
The first field of accumulators points out of the OCaml heap, so using
closures instead of tag-0 objects is better for the GC.
Accumulators are distinguished from closures because their code pointer
necessarily is the "accumulate" address, which points to an ACCUMULATE
instruction.
|
|
That way, accumulators again can be used directly as execution
environments by the bytecode interpreter. This fixes the issue of the
first argument of accumulators being dropped when strongly normalizing.
|
|
The second field of a closure can no longer be the value of the first free
variable (or another closure of a mutually recursive block) but must be an
offset to the first free variable.
This commit makes the bytecode compiler and interpreter agnostic to the
actual representation of closures. To do so, the execution environment
(variable coq_env) no longer points to the currently executed closure but
to the last one. This has the following consequences:
- OFFSETCLOSURE(n) now always loads the n-th closure of a recursive block
(counted from last to first);
- ENVACC(n) now always loads the value of the n-th free variable.
These two changes make the bytecode compiler simpler, since it no
longer has to track the relative position of closures and free variables.
The last change makes the interpreter a bit slower, since it has to adjust
coq_env when executing GRABREC. Hopefully, cache locality will make the
overhead negligible.
|
|
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
