Accumulators as functions and optionnal accumulators by IBBXEF · Pull Request #22347 · rocq-prover/rocq

IBBXEF · 2026-08-14T14:59:24Z

This one has both changes (optionnal accumulators and new representation)

coqbot-app · 2026-08-14T14:59:28Z

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

ppedrot · 2026-08-16T11:14:40Z

@coqbot run full ci

ppedrot · 2026-08-16T11:15:35Z

@coqbot bench

SkySkimmer · 2026-08-16T11:31:04Z

bench will crash since neither #22351 or #22350 are merged

coqbot-app · 2026-08-16T11:46:29Z

🏁 Bench results:

┌──────────────┬───────────────────────┬─────────────────────────────────────┬───────────────────────┐
│              │     user time [s]     │          CPU instructions           │ max resident mem [KB] │
│              │                       │                                     │                       │
│ package_name │  NEW     OLD    PDIFF │      NEW            OLD       PDIFF │  NEW     OLD    PDIFF │
├──────────────┼───────────────────────┼─────────────────────────────────────┼───────────────────────┤
│    rocq-core │  15.74   16.72  -5.86 │  100062004099   108935017371  -8.15 │ 496736  495972   0.15 │
│     coq-hott │ 169.41  169.73  -0.19 │ 1053463032343  1053438199966   0.00 │ 467648  467792  -0.03 │
│    rocq-elpi │  20.26   20.27  -0.05 │  132019558698   132671841164  -0.49 │ 491460  491432   0.01 │
│ rocq-runtime │  76.05   76.06  -0.01 │  555183372221   554784125909   0.07 │ 542520  542284   0.04 │
│     coq-core │   2.85    2.79   2.15 │   19297222765    19293687095   0.02 │ 114024  114004   0.02 │
└──────────────┴───────────────────────┴─────────────────────────────────────┴───────────────────────┘

INFO: failed to install
rocq-stdlib (in NEW)
rocq-mathcomp-boot (dependency install failed in NEW)

rocq-bignums (dependency rocq-stdlib failed)
coq-performance-tests-lite (dependency rocq-stdlib failed)
coq-engine-bench-lite (dependency rocq-stdlib failed)
rocq-mathcomp-order (dependency rocq-mathcomp-boot failed)
rocq-mathcomp-ssreflect (dependency rocq-mathcomp-boot failed)
rocq-mathcomp-finite-group (dependency rocq-mathcomp-boot failed)
rocq-mathcomp-algebra (dependency rocq-mathcomp-boot failed)
rocq-mathcomp-solvable (dependency rocq-mathcomp-boot failed)
rocq-mathcomp-field (dependency rocq-mathcomp-boot failed)
rocq-mathcomp-group-representation (dependency rocq-mathcomp-boot failed)
coq-mathcomp-odd-order (dependency rocq-mathcomp-boot failed)
coq-mathcomp-analysis (dependency rocq-mathcomp-boot failed)
coq-math-classes (dependency rocq-stdlib failed)
coq-corn (dependency rocq-stdlib failed)
coq-compcert (dependency rocq-stdlib failed)
rocq-equations (dependency rocq-stdlib failed)
rocq-metarocq-utils (dependency rocq-stdlib failed)
rocq-metarocq-common (dependency rocq-stdlib failed)
rocq-metarocq-template (dependency rocq-stdlib failed)
rocq-metarocq-pcuic (dependency rocq-stdlib failed)
rocq-metarocq-safechecker (dependency rocq-stdlib failed)
rocq-metarocq-erasure (dependency rocq-stdlib failed)
rocq-metarocq-translations (dependency rocq-stdlib failed)
coq-color (dependency rocq-stdlib failed)
coq-coqprime (dependency rocq-stdlib failed)
coq-coqutil (dependency rocq-stdlib failed)
coq-bedrock2 (dependency rocq-stdlib failed)
coq-rewriter (dependency rocq-stdlib failed)
coq-fiat-core (dependency rocq-stdlib failed)
coq-fiat-parsers (dependency rocq-stdlib failed)
coq-fiat-crypto-with-bedrock (dependency rocq-stdlib failed)
coq-unimath (dependency rocq-stdlib failed)
coq-coquelicot (dependency rocq-mathcomp-boot failed)
coq-iris-examples (dependency rocq-stdlib failed)
coq-fourcolor (dependency rocq-mathcomp-boot failed)
coq-rewriter-perf-SuperFast (dependency rocq-stdlib failed)
coq-vst (dependency rocq-stdlib failed)
coq-category-theory (dependency rocq-stdlib failed)
coq-neural-net-interp-computed-lite (dependency rocq-stdlib failed)

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                          TOP 25 SLOW DOWNS                                           │
│                                                                                                      │
│   OLD     NEW     DIFF    %DIFF    Ln              FILE                                              │
├──────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   0.345   0.373  0.0276    8.00%   296  coq-hott/theories/HIT/V.v.html                               │
│   0.136   0.149  0.0125    9.16%    69  coq-hott/theories/Colimits/Colimit_Pushout_Flattening.v.html │
│   0.206   0.218  0.0119    5.78%   670  coq-hott/theories/Pointed/Core.v.html                        │
│   0.556   0.568  0.0119    2.14%   156  coq-hott/theories/Categories/Adjoint/Pointwise.v.html        │
│  0.0715  0.0829  0.0114   16.01%    84  coq-hott/theories/Classes/orders/integers.v.html             │
│   0.227   0.236  0.0096    4.24%    70  coq-hott/theories/Categories/Pseudofunctor/Identity.v.html   │
│   0.204   0.213  0.0092    4.50%    62  coq-hott/theories/Homotopy/PiSpheres.v.html                  │
│ 0.00390  0.0122  0.0083  212.65%   145  coq-hott/theories/Cubical/DPathCube.v.html                   │
│   0.118   0.126  0.0078    6.55%   105  coq-hott/theories/Spaces/Torus/TorusEquivCircles.v.html      │
│  0.0378  0.0451  0.0073   19.25%   856  coq-hott/theories/Homotopy/Join/TriJoin.v.html               │
│  0.0664  0.0735  0.0071   10.65%   668  coq-hott/theories/Algebra/Groups/FreeProduct.v.html          │
│   0.375   0.382  0.0068    1.80%   268  coq-hott/theories/Homotopy/CayleyDickson.v.html              │
│  0.0342  0.0408  0.0066   19.36%   321  coq-hott/theories/Colimits/GraphQuotient.v.html              │
│  0.0322  0.0389  0.0066   20.59%   660  coq-hott/theories/Colimits/Coeq.v.html                       │
│  0.0564  0.0626  0.0062   11.06%   949  coq-hott/theories/WildCat/Products.v.html                    │
│   0.431   0.437  0.0062    1.43%   170  coq-hott/theories/Pointed/pFiber.v.html                      │
│   0.106   0.112  0.0060    5.70%    54  coq-hott/theories/Categories/ExponentialLaws/Law4/Law.v.html │
│   0.656   0.662  0.0058    0.89%   703  coq-hott/theories/Pointed/Core.v.html                        │
│  0.0596  0.0652  0.0056    9.40%   688  coq-hott/theories/Pointed/Core.v.html                        │
│   0.655   0.661  0.0056    0.85%    37  coq-hott/theories/Homotopy/PiSpheres.v.html                  │
│   0.159   0.165  0.0055    3.48%   447  coq-hott/theories/Pointed/Core.v.html                        │
│   0.198   0.203  0.0054    2.72%  1013  coq-hott/theories/Homotopy/Syllepsis.v.html                  │
│   0.683   0.688  0.0052    0.75%   435  coq-hott/theories/Homotopy/HomotopyGroup.v.html              │
│  0.0156  0.0209  0.0052   33.47%    25  coq-hott/theories/Categories/Grothendieck/ToCat.v.html       │
│  0.0706  0.0756  0.0050    7.06%   137  coq-hott/theories/Algebra/AbGroups/AbPushout.v.html          │
└──────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                             TOP 25 SPEED UPS                                             │
│                                                                                                          │
│  OLD     NEW     DIFF     %DIFF   Ln               FILE                                                  │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  0.535   0.508  -0.0274   -5.12%   22  coq-hott/theories/Categories/GroupoidCategory/Morphisms.v.html    │
│  0.798   0.784  -0.0135   -1.70%   45  coq-hott/theories/Categories/ExponentialLaws/Law2/Law.v.html      │
│  0.236   0.225  -0.0112   -4.75%  211  coq-hott/theories/Colimits/Colimit_Flattening.v.html              │
│  0.280   0.269  -0.0108   -3.87%  103  coq-hott/theories/Cubical/PathCube.v.html                         │
│  0.299   0.288  -0.0104   -3.47%  102  coq-hott/theories/Cubical/PathCube.v.html                         │
│  0.379   0.369  -0.0100   -2.64%   48  coq-hott/theories/Categories/ExponentialLaws/Law4/Law.v.html      │
│ 0.0599  0.0511  -0.0088  -14.77%  130  coq-hott/theories/Algebra/AbSES/SixTerm.v.html                    │
│  0.296   0.288  -0.0079   -2.67%  101  coq-hott/theories/Cubical/PathCube.v.html                         │
│  0.111   0.104  -0.0076   -6.82%  312  coq-hott/theories/Algebra/Groups/QuotientGroup.v.html             │
│  0.285   0.277  -0.0074   -2.61%  196  coq-hott/theories/Categories/LaxComma/CoreLaws.v.html             │
│  0.361   0.354  -0.0071   -1.97%  113  coq-hott/theories/Categories/Adjoint/Functorial/Laws.v.html       │
│  0.764   0.757  -0.0069   -0.91%   32  coq-hott/theories/Categories/ExponentialLaws/Law3/Law.v.html      │
│  0.410   0.403  -0.0069   -1.68%   81  coq-hott/theories/Algebra/Rings/QuotientRing.v.html               │
│ 0.0577  0.0519  -0.0058  -10.07%  450  coq-hott/theories/Colimits/Sequential.v.html                      │
│ 0.0710  0.0653  -0.0057   -8.08%  241  coq-hott/theories/Colimits/Sequential.v.html                      │
│ 0.0320  0.0264  -0.0056  -17.46%  206  coq-hott/theories/Algebra/AbSES/Pushout.v.html                    │
│  0.237   0.231  -0.0055   -2.32%  455  coq-hott/theories/Classes/implementations/natpair_integers.v.html │
│  0.139   0.134  -0.0051   -3.67%  295  coq-hott/theories/Categories/Category/Sigma/Univalent.v.html      │
│  0.243   0.238  -0.0051   -2.11%  735  coq-hott/theories/Algebra/AbSES/Core.v.html                       │
│  0.157   0.152  -0.0047   -2.99%  438  coq-hott/theories/Spaces/BAut/Bool.v.html                         │
│ 0.0956  0.0909  -0.0047   -4.94%  208  coq-hott/theories/Algebra/ooGroup.v.html                          │
│ 0.0181  0.0139  -0.0043  -23.61%   79  coq-hott/theories/Algebra/AbGroups/TensorProduct.v.html           │
│  0.165   0.161  -0.0043   -2.61%   85  coq-hott/theories/Pointed/Loops.v.html                            │
│ 0.0226  0.0187  -0.0039  -17.22%  598  coq-hott/theories/Homotopy/BlakersMassey.v.html                   │
│ 0.0250  0.0212  -0.0038  -15.13%  414  coq-hott/theories/Colimits/Sequential.v.html                      │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

Is now able to compile strings, floats and sequences of mllambda to malfunction

…atements

…the same file

…ld have two dolla sign in front of them

…ted as $() instead of 0

…unctions

…accumulators

…his information is used when compiling

…it instead of crashing

… info is used to avoid unecessary accumulator use.

…ed using ocaml-print-intf.

…ger needed, and removed the useless import of Constructs

…ther library that uses them (recompiles it instead).

…between supporting accumulators and generating them

…uld reuse the previous file when switching to an accumulator representation late

…use recompilation with accumulators if inside an inductive type

…lator is needed to interpret the return value

…from closures

…assembly

…ns that would break our accumulator detection

coqbot-app · 2026-08-19T10:52:01Z

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 14, 2026

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 16, 2026

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 16, 2026

IBBXEF added 22 commits August 19, 2026 12:45

enabling native-compiler

050b513

Created placeholder functions for compiling to mlf

bb6c614

Is now able to compile strings, floats and sequences of mllambda to malfunction

Now compiles lambda functions

238477b

Now compiles primitives

24371ff

the mlf compiler is now called by the general compile function

21cdcaa

fixed two naming errors

50fcc05

Now compiles local and global variable names, applications and let st…

c501fcf

…atements

Now compiles if and letrec statements, and fixed a bug with global names

741d512

Now compiles (at least define) let cases

01393e9

Now compiles global table fix types (whatever that is)

1d8d2c4

Now compiles global table norm and fixed a few bugs

1ed11de

Fixed a capitalization error and a few inconsistencies

53890e2

Now compiles arrays and reference assignment

0a3be3f

Fixed an arror where global names where wrongly assumed to come from …

2fe67ee

…the same file

Fixed a bug introduced by the last fix where some global variable wou…

e6fd9ed

…ld have two dolla sign in front of them

refactored some of the code and fixed a bug where () would be transla…

5a62b24

…ted as $() instead of 0

rt1 and rt2 are now correctly marked as coming from the Nativelib module

5962c78

refactored pp_gname_plf

fd8852f

Fixed an error whith double dollar signs before variables

8d28a82

Now compiles match statements

3b6b7d3

Now compiles primitives Mk_fix and Mk_var

a9153b4

Fixed a double dollar bug and some values being wrongly compiled as f…

6ef0751

…unctions

IBBXEF added 26 commits August 19, 2026 12:50

fixed some comments that are no longer accurate

b900ce0

accumulator removal now takes into account libraries that could need …

649408c

…accumulators

fixed has_accus_native_file wrongly always returning true

516a3a3

Libraries mli interfaces now indicate if they use accumulators, and t…

f5a9513

…his information is used when compiling

made a temporary fix to mli files being in the wrong location

2c08084

When a library does not support accumulators but we do, we recompile …

df20cb1

…it instead of crashing

Libraries now indicate if they do not generate accumulators, and this…

60e294c

… info is used to avoid unecessary accumulator use.

custom flags are now stored in the compiled interface and are retriev…

1c40dbc

…ed using ocaml-print-intf.

fixed library file being wrong when registering native libraries

5f46da5

removed global type declaration as they are no longer needed

7294f15

Removed prefix and inductive name from MLconstruct as they are no lon…

f5ab538

…ger needed, and removed the useless import of Constructs

Now longer forces accumulators by needing an inductive defined in ano…

aa91e6f

…ther library that uses them (recompiles it instead).

fixed a comment

ae8a008

fixed most TODOs, and non-library files now also have a dinstinction …

0d7ccdd

…between supporting accumulators and generating them

Fixed an old bug made visible by the last commit : native_conv_gen wo…

ef77ee3

…uld reuse the previous file when switching to an accumulator representation late

fixed an important bug where functions (and productions) would not ca…

1839a60

…use recompilation with accumulators if inside an inductive type

Now make simple checks to avoid recompiling everything when an accumu…

155d3b0

…lator is needed to interpret the return value

updated gitlab ci

8945ff0

changed the representation of accumulators to be a closure

e7ec5e5

Fixed closures and accumulators being undistinguishable

9dbd0e2

removed the main hack in the handling of accumulators

81ffacb

cleaned code and simplified the hack used to differentiate functions …

7ae5882

…from closures

removed magic numbers

8cd6c05

changed accumulator contruction and check to not use Obj.with_tag

28362fc

removed architectures checks as native_compute no longer uses inline …

79b43fc

…assembly

added more guardrails to the build_accu function to avoid optimisatio…

390c586

…ns that would break our accumulator detection

IBBXEF force-pushed the accumulators_as_functions branch from d82431e to 390c586 Compare August 19, 2026 10:51

coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Aug 19, 2026

Navigation Menu

Uh oh!

Accumulators as functions and optionnal accumulators - #22347

Accumulators as functions and optionnal accumulators#22347
IBBXEF wants to merge 110 commits into
rocq-prover:masterfrom
IBBXEF:accumulators_as_functions

IBBXEF commented Aug 14, 2026

Uh oh!

coqbot-app Bot commented Aug 14, 2026

Uh oh!

ppedrot commented Aug 16, 2026

Uh oh!

ppedrot commented Aug 16, 2026

Uh oh!

SkySkimmer commented Aug 16, 2026

Uh oh!

coqbot-app Bot commented Aug 16, 2026

Uh oh!

coqbot-app Bot commented Aug 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

IBBXEF commented Aug 14, 2026

Uh oh!

coqbot-app Bot commented Aug 14, 2026

Uh oh!

ppedrot commented Aug 16, 2026

Uh oh!

ppedrot commented Aug 16, 2026

Uh oh!

SkySkimmer commented Aug 16, 2026

Uh oh!

coqbot-app Bot commented Aug 16, 2026

Uh oh!

coqbot-app Bot commented Aug 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants