Hi, if you have some time could you do dune exec -- coqc test-suite/complexity/pretyping.v
, I'm interested in seeing what kind of values people get.
Here is me running it 10 times:
for i in {1..10}; do _build/install/default/bin/coqc test-suite/complexity/pretyping.v; done
Finished transaction in 1.259 secs (1.25u,0.008s) (successful)
Finished transaction in 1.198 secs (1.178u,0.019s) (successful)
Finished transaction in 1.265 secs (1.207u,0.03s) (successful)
Finished transaction in 1.231 secs (1.211u,0.019s) (successful)
Finished transaction in 1.252 secs (1.218u,0.018s) (successful)
Finished transaction in 1.222 secs (1.209u,0.012s) (successful)
Finished transaction in 1.26 secs (1.226u,0.027s) (successful)
Finished transaction in 1.935 secs (1.619u,0.315s) (successful)
Finished transaction in 1.203 secs (1.182u,0.02s) (successful)
Finished transaction in 1.194 secs (1.174u,0.019s) (successful)
As you can see there is a jump to 1.9 seconds randomly towards the end
I'm starting to form the opinion that the complexity tests are garbage and that we should move them to the bench in a dedicated package.
Last updated: May 28 2023 at 16:30 UTC