search

mit-plv / rewriter

Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Other
22 stars 20 forks source link

speedup wf{3,4}_of_wf by factorizing raw matches to definitions #157

Closed SkySkimmer closed 2 months ago

SkySkimmer commented 2 months ago

This greatly reduces term size (tree size 1988106 -> 1121651 for wf3_of_wf).

Timings before: (Time Succeed Qed includes some time which isn't in Time Qed, see also https://github.com/coq/coq/pull/19426)

wf3 tactics 2.2s qed 1.09s succeed qed 1.25s

wf4 tactics 14.5s qed 7.4s succeed qed 8.5s

After:

wf3 tactics 1.4s qed 0.6s succeed qed 0.65s

wf4 tactics 8s qed 3.6s succeed qed 4s

SkySkimmer commented 2 months ago

CI looks bugged, it's complaining about python versions AFAICT

JasonGross commented 2 months ago

Indeed, I'm guessing the docker image or the apt repositories were recently updated, let's see if https://github.com/mit-plv/rewriter/pull/158 fixes it