Stream: Coq devs & plugin devs

Topic: bench failures


view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 11:14):

The bench always says

INFO: failed to install coq-performance-tests-lite
coq-sf-plf

Is it a bug?
Should we remove them from the package list?

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 11:16):

Hm, that's weird. The first one should succeed. The second one often fails with master, so...

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 11:21):

The second one often fails with master

isn't it in CI?

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 11:21):

I think the CI uses script trickery to make it compile. The bench uses the opam package instead.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 11:22):

bench log for sf-plf says # make: *** No rule to make target 'install'. Stop.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 11:23):

perf tests says

# File "./rewrite_lift_lets_map/_4_SuperFast.v", line 3, characters 11-26:
# Warning: native_compute disabled at configure time; falling back to vm_compute. [native-compute-disabled,native-compiler]
# File "./rewrite_lift_lets_map/_4_SuperFast.v", line 3, characters 11-26:
# Error: Stack overflow.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 11:26):

cc @Jason Gross

view this post on Zulip Jason Gross (Dec 03 2020 at 11:49):

Um, that's weird. I recently added a file to coq-performance-tests, and there was briefly a time when that file wasn't compiling, but it wasn't that file and I haven't touched that file lately. Can you give me an Ltac backtrace for where the stack overflow occurs?

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 11:54):

I can't


Last updated: Oct 21 2021 at 22:02 UTC