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?
Hm, that's weird. The first one should succeed. The second one often fails with master, so...
The second one often fails with master
isn't it in CI?
I think the CI uses script trickery to make it compile. The bench uses the opam package instead.
bench log for sf-plf says
# make: *** No rule to make target 'install'. Stop.
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.
cc @Jason Gross
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?
Last updated: Jun 08 2023 at 04:01 UTC