| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: gares
Ack-by: maximedenes
|
|
We get rid of the future wrappers, as all callers are immediately forcing
the result.
|
|
Safe_typing is now responsible for hashconsing of all accessible structures,
except for opaque terms which are handled by Opaqueproof.
|
|
|
|
This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
|
|
|
|
|
|
We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.
|
|
|
|
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
I think the usage looks cleaner this way.
|
|
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
|
|
|
|
|
|
|
|
Fix #8609
gares said: I believe it was introduced in de20a45 where the
option (part of the summary) is moved to the save env. By setting the
summary, you unshare the safe env. Now we do that only if needed. The
stm uses `==` on the safe env to detect tactics that alter the env, eg
abstract.
|
|
|
|
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
|
|
The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).
We also add a `-bytecode-compiler` flag.
Fixes #4607
|
|
|
|
|
|
Instead of threading the universe state and making it grow, we make clear
in the signature that the differed side-effects generate constraints to be
added.
|
|
This reduces the attack surface of the API, as actually there is only a back
and forth between the two modules, and side-effects validity certificates are
intuitively nothing more than safe environments.
|
|
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
|
Adding a ucontext to the global environment only makes sense
internally when checking a polymorphic constant.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We remove internal functions and types from the API.
|
|
We simply exploit a type isomorphism to remove the use of dedicated algebraic
types in the kernel which are actually not necessary.
|
|
We eta-expand cofixpoints when needed, so that their call-by-need
evaluation is correctly implemented by VM and native_compute.
|
|
We now have only two notions of environments in the kernel: env and
safe_env.
|
|
|
|
We force the upper layers to extrude the universe constraints before sending
it to the kernel. This simplifies the suspicious handling of polymorphic
constraints for section-local definitions.
|
|
This allows to statically ensure well-formedness properties.
|
|
Let definitions have the same behaviour if they are ended with a Qed or a
Defined command, i.e. they are treated as if they were transparent. Indeed,
it doesn't make sense for them to be opaque as they are going to be expanded
away at the end of the section.
For an unknown reason, handling of side-effects in Let definitions considers
them as if they were opaque, i.e. the effects are inlined in the definition.
This discrepancy has bad consequences in the kernel, where one is forced to
juggle with universe constraints generated by polymorphic Let definitions.
As a first phase of cleaning, we simply enforce by typing that Let definitions
should be purified before reaching the kernel.
This has the intended side-effect to make side-effects persistent in Let
definitions, as if they were indeed truly transparent.
|
|
The patch has three parts:
- Introduction of a configure flag `-bytecode-compiler (yes|no)`
(due to static initialization this is a configure-time option)
- Installing the hooks that register the VM with the pretyper and the
kernel conditionally on the flag.
- Replacing the normalization function in `Redexpr` by compute if the
VM is disabled.
We also rename `Coq_config.no_native_compiler` to `native_compiler`
and `Flags.native_compiler` to `output_native_objects` [see #4607].
|
|
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
|
This will allow to merge back `Names` with `API.Names`
|
