Stream: Coq devs & plugin devs

Topic: What do you get for test-suite/complexity/pretyping.v


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Dec 01 2023 at 07:01 UTC