checker · coq · Tangled

forked from coq/coq

coq checker

28 files

Gaëtan Gilbert · Stop using resolver for nothing in checker axiom collection · 2w ago

rocqchk: accept the "big" marshal header for segments over 4 GiB

Use standard float an integer datatypes in Votour representation.

rocqchk accumulate axioms without "opacify" logic

rocqchk accumulate axioms without "opacify" logic

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.

Do not trust the serialized VM bytecode in rocqchk

checkInductive.ml

Extrude universe abstraction of inductive types out of the kernel.

checkInductive.mli

Correctly check retroknowledge in the checker.

checkLibrary.ml

Drop useless env argument of collect_module_axioms

checkLibrary.mli

rocqchk accumulate axioms without "opacify" logic

rocqchk accumulate axioms without "opacify" logic

coqchk_main.mli

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

Rename some coqchk files

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

Remove compat coq-core libraries (not executables)

Treat set predicativity and sprop-allowed more like normal typing flags

mod_checking.ml

Stop using resolver for nothing in checker axiom collection

mod_checking.mli

Drop useless env argument of collect_module_axioms

Add `rocqchk` command and `rocq check` subcommand, move coqchk back to coq-core

Add `rocqchk` command and `rocq check` subcommand, move coqchk back to coq-core

safe_checking.ml

Do not trust the serialized VM bytecode in rocqchk

safe_checking.mli

rocqchk accumulate axioms without "opacify" logic

Correctly validate block tags in rocqchk demarshaller.

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

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 Values.equal instead of pointer equality in validate cache

Print the segment hash in votour toplevel output.

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