Ali Caglayan (May 16 2022 at 18:57): Ali Caglayan (May 16 2022 at 18:57):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.
Ali Caglayan (May 16 2022 at 19:02):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
Ali Caglayan (May 16 2022 at 19:07):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