kernel · coq · Tangled

forked from coq/coq

coq kernel

1 folder · 142 files

Sami Jawhar · Fix proof of False when VM conversion eta-expands a mutual fixpoint · 2w ago

Merge PR #22447: Add support for native_compute on ARM64 processors.

Lift big closures to reduce memory consumption

Add higher-order substitution to CClosure so that rewrite rules don't call term_of_fconstr

constant_typing.ml

Merge PR #22589: Nicer error for incorrect Proof using

constant_typing.mli

Fix kernel APIs to take Univ.ContextSet rather than the PConstraints one.

Remove compare_head_gen_with from the Constr API.

Remove compare_head_gen_with from the Constr API.

Move CompactedDecl to ppconstr

Move CompactedDecl to ppconstr

Deprecate the canord-based maps and sets of constants.

conv_oracle.mli

Add Kernel Conversion Dep Heuristic flag for smarter constant unfolding.

Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.

VM/native support inductive cumulativity

Use the now correct set and maps Names APIs.

Use the now correct set and maps Names APIs.

Add support for parsing elimination constraints

cPrimitives.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

declarations.mli

Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.

Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.

Extrude universe abstraction of general definitions out of the kernel.

Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Remove compat coq-core libraries (not executables)

Extrude universe abstraction of general definitions out of the kernel.

Enforce consistency of env typing flags with ugraph type-in-type flag

Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.

kernel/esubst.ml: fix a BUG in the UNUSED function [weakening_to_lift].

kernel/esubst.mli: fix incorrect comment.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Rename all C functions and macros from the VM according to the Great Rocqification.

Update the OCaml headers to reflect the fact Coq is now Rocq.

float64_common.ml

Rename all C functions and macros from the VM according to the Great Rocqification.

float64_common.mli

Rename Coq -> Rocq in various comments and doc

Rename Coq -> Rocq in various comments and doc

Merge PR #21677: Improved handling of disabled VM

Remove dead API from Genlambda.

genOpcodeFiles.ml

Rename all C functions and macros from the VM according to the Great Rocqification.

genOpcodeFiles.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Remove KerPair.SyntacticOrd

Hashconsing try to avoid recomputing hashes

Stop relying on CanOrd in Inductive.

When a record cannot be declared with primitive projections, explain why

Extrude universe abstraction of inductive types out of the kernel.

Track inductives that depend on indices not mattering

Fix recursive-call errors in fixpoint binder types

Stop relying on CanOrd in Inductive.

inferCumulativity.ml

inferCumulativity treat letins in indices and constructor types as invariant positions

inferCumulativity.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

mod_declarations.ml

Correctly substitute module implementation δ-resolvers.

mod_declarations.mli

Invert the aliasing declaration for inclusions of non-path modules.

Use the now correct set and maps Names APIs.

Keep aliasing and inlining data separate in δ-resolvers.

Minor assertion in module inclusion.

Factorize the code of module inclusion.

Enforce more conditions in subtyping of inductive types.

Enforce more conditions in subtyping of inductive types.

Name sets and maps now use the user naming for key indexing.

Deprecate the _env modules for sets and maps from Names.

Use the now correct set and maps Names APIs.

Pass Nativecode symbols by reference.

Stop relying on canonical names in Native conversion.

Update the OCaml headers to reflect the fact Coq is now Rocq.

nativelambda.ml

Wrap Lambda nodes in a dummy indirection.

nativelambda.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Stop using global lazy for temp dir in nativelib

Pass Nativecode symbols by reference.

nativelibrary.ml

Pass Nativecode symbols by reference.

nativelibrary.mli

Move the module-related definitions from Declarations to a new module.

nativevalues.ml

Expose the Nativevalues internals as OCaml externals.

nativevalues.mli

Expose the Nativevalues internals as OCaml externals.

Fix kernel APIs to take Univ.ContextSet rather than the PConstraints one.

opaqueproof.mli

Fix kernel APIs to take Univ.ContextSet rather than the PConstraints one.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

partial_subst.ml

Extrude NoDupArray into its own clib file, rename it to WriteOnceArray

partial_subst.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

pConstraints.ml

QGlobal is not QVar

pConstraints.mli

QGlobal is not QVar

Check for coherence of primitive constants using user names.

Statically enforce primitive string size invariant.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Allow setting a root in AcyclicGraph.

Validate Proof: detect missing constraints, error if any issues found

Implement [RedFlags] with bitfields.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

relevanceops.ml

feat: Allow primitive projections with postponed eta

relevanceops.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

retroknowledge.ml

Update the OCaml headers to reflect the fact Coq is now Rocq.

retroknowledge.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Store inductive automata next to their regular tree in Declarations.

Store inductive automata next to their regular tree in Declarations.

Merge PR #22528: Add constant unfolding heuristic based on definitional heights.

safe_typing.mli

Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.

Use the now correct set and maps Names APIs.

QGlobal is not QVar

Merge PR #21957: Avoid conflict between global sorts defined in separate modules

Merge PR #21957: Avoid conflict between global sorts defined in separate modules

Enforce more conditions in subtyping of inductive types.

Fix subtyping with elim constraints

More specific anomalies in contract_case

More specific anomalies in contract_case

transparentState.ml

Update the OCaml headers to reflect the fact Coq is now Rocq.

transparentState.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Fix recursive-call errors in fixpoint binder types

type_errors.mli

Fix recursive-call errors in fixpoint binder types

Move check_hyps_inclusion out of the kernel

Move check_hyps_inclusion out of the kernel

Remove the unused AcyclicGraph.choose primitive.

Remove the unused AcyclicGraph.choose primitive.

Fix primitive int asr implem (fixes #22462)

Fix primitive int asr implem (fixes #22462)

Update the OCaml headers to reflect the fact Coq is now Rocq.

changed |= to | when displaying universes constraints

Reintroduce Univ.ContextSet.

changed |= to | when displaying universes constraints

QGlobal is not QVar

Update the OCaml headers to reflect the fact Coq is now Rocq.

QGlobal is not QVar

QGlobal is not QVar

Stop relying on CanOrd in VM conversion.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Fix proof of False when VM conversion eta-expands a mutual fixpoint

Update the OCaml headers to reflect the fact Coq is now Rocq.

QGlobal is not QVar

vmbytecodes.mli

Rename all C functions and macros from the VM according to the Great Rocqification.

Be more defensive against nullary functions (cf #21136).

VM error when encountering non compiled constant (from disabled VM)

Treat opaque Var nodes as structured constants in the VM.

vmemitcodes.mli

VM error when encountering non compiled constant (from disabled VM)

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Wrap Lambda nodes in a dummy indirection.

Use CDebug for Dump Bytecode and Dump Lambda

Names: move set/map modules `KNset` -> `KerName.Set` etc

Update the OCaml headers to reflect the fact Coq is now Rocq.

Treat opaque Var nodes as structured constants in the VM.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Fix proof of False when VM conversion eta-expands a mutual fixpoint

Fix proof of False when VM conversion eta-expands a mutual fixpoint