| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
native_compute is called.
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
caml_something_to_do.
Reviewed-by: gasche
Ack-by: ppedrot
Reviewed-by: xavierleroy
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
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.
|
|
|
|
|
|
|
|
This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents
arities being mistakenly set to zero.
|
|
Since the compiler initializes the arities to zero, coq_tcode_of_code
wrongly believes that the word following a primitive operation contains
an opcode, while it is the global index of the primitive operation. So,
the function will try to translate it and thus corrupt it. But as long as
the evaluated term fully reduces (which is always the case for
CoqInterval), the corrupted word will never be read.
At this point, it all depends on the arity of the global index (seen as
an opcode). If it is zero, then coq_tcode_of_code will recover and
correctly translate the following opcodes. If it is nonzero, then the
function starts translating random words, possibly corrupting the memory
past the end of the translation buffer. Independently of this memory
corruption, coq_interprete will execute random code once it gets to the
opcode following the primitive operation, since it has not been
translated.
The reason CoqInterval is not always crashing due to this bug is just
plain luck. Indeed, the arity of the pseudo opcode only depends on the
global index of the primitive operations. So, as long as this arity is
zero, the memory corruption is fully contained. This happens in the vast
majority of cases, since coq_tcode_of_code translates any unrecognized
opcode to STOP, which has arity zero.
This bug is exploitable.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Also works for simpl.
|
|
MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is
never encountered in the fast path, this optimization is not worth the
extra complexity.
|
|
The generated bytecode almost never needs to modify the field of an OCaml
object. The only exception is the laziness mechanism of coinductive types.
But it modifies field 2, and thus uses the generic opcode SETFIELD anyway.
|
|
The PUSHFIELDS opcode is a costly one, yet lots of constructors have at
most one usable argument (e.g., option, nat, positive, Z, Acc). For those
constructors, PUSHFIELDS(1) is replaced by GETFIELD(0);PUSH, assuming
the accu register is no longer used afterwards.
Replacing one single opcode by two opcodes might seem like a
pessimization, but it is not. Indeed, pattern-matching branches usually
start by filling the accu register with a constructor argument or the
value of a free variable or a constant. All of those offer peephole
optimizations for PUSH, which means that the number of opcodes actually
stay constant.
Note that, for the same reason, the assumption above holds in practice:
the accu register is no longer used after PUSHFIELDS.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.
|
|
Instead we export a representation function that gives a high-level view
of the data structure in terms of constraints.
|
|
|
|
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.
|
|
We need this file for the upcoming kernel representation change there.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
When using OCaml >= 4.10, function caml_process_pending_actions_exn is
called whenever the bytecode interpreter tries to apply a term. This
function exits immediately when caml_something_to_do is not set. But since
term application happens every few opcodes, even exiting immediately still
accounts between 5% and 10% of the whole interpreter. So, this commit
makes sure the function is not called unless caml_something_to_do is
already set (i.e., when the user presses Ctrl+C). This means that this
conditional branch is perfectly predicted by the processor.
On the following benchmark, this commit makes the VM 13% faster.
Time Eval vm_compute in Pos.iter (fun x => x) tt 100000000.
Note that, before OCaml 4.10, the VM code was checking the value of
caml_signals_are_pending before calling caml_process_pending_signals. So,
this commit actually fixes a regression.
|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
notations.
Reviewed-by: jfehrle
Reviewed-by: proux01
Ack-by: Zimmi48
Ack-by: SkySkimmer
|
|
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
|
|
|
|
|
|
|
|
We use a variant of skewed lists enriched over a monoid, whose purpose is
to count the number of lifts added to the substitution. This makes addition
O(1) and lookup O(log n).
|
|
|
|
- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API)
- the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors
- Grants #13484: String notations for primitive arrays
- Fixes #13517: String notation printing fails with primitive integers inside lists
|
|
They are not used there, and removing the redundance of the the case
representation requires access to the environment, so we push their use
further up.
|
|
This is presumably not usable from the surface language. But an ML module
could easily create a proof of false by passing a negative number to
Const.mkInt.
|
|
|
|
Before this commit, function mask63 was called implicitly at each step.
|
|
|
|
|
|
of cases.
|
|
cumulative inductive types
Reviewed-by: SkySkimmer
|
|
types
|
|
|
|
|
|
This is just an experiment, but makes the uses of the API easier as we
don't mess with the global state anymore.
|
