Pierre-Marie Pédrot

Switch the default locality of hint-like commands to #[export].

31

This is a sister draft PR of #16004, whose only goal is to check that the changes in CI devs are compatible with the switch of semantics. Eventually this should...

# Release checklist # ## When the release managers for version `X.X` get nominated ## - [x] Create a new issue to track the release process where you can copy-paste...

Test equations playground

1

cc @mattam82 @SkySkimmer

Allow Ltac2 notations from within Ltac1

12

This is preliminary work to check that the design aligns with the requirements of the people who asked for this feature. This PR adds a new Ltac2 vernacular command of...

Clean the API of the congruence plugin

2

We remove from the API stuff that is exported but clearly internal details, and enforce a few invariants by typing.

Store VM relocations that do not need substitution on disk.

4

This prevents loading in memory potentially useless data, especially the so-called "structured values" which are (potentially big) blobs. As per the bench, the size of vo files is basically unchanged.

Remove the Lforce node from the generic lambda AST.

6

We move the code responsible from the generation of the forcing of lazy constants in the native compiler to the second compilation phase. This also has the nice side-effect of...

[Experiment] Hack a global fixpoint expansion in conversion.

18

Quick and dirty experiment following the Coq call. Rather than implementing a full-blown refolding of fixpoint everywhere, we experiment with refolding when converting only.

Incorrect compilation of lazy native definitions in presence of variables

1

This is a byproduct of #18692. Native compilation wraps some definitions in a lazy node, but generates garbage code if this code happens to refer to free variables. ```coq Section...