failed to install coq-performance-tests-lite coq-sf-plf
(eg https://gitlab.com/coq/coq/-/jobs/907722827)
what can we do about this?
cc @Jason Gross
Where did coq-performance-tests-lite fail? What's the error message/file/log?
logs are in the artifacts
>
@Gaëtan Gilbert Why is the bench disabling the native compiler? In any case, if you decide that in fact you want to keep disabling the native compiler, then you should update the max size for kind_red native
to match the branch for kind_red vm
in https://github.com/coq-community/coq-performance-tests/blob/aedb0bab5042af75c65a425d8c9584fd01f8c64e/PerformanceExperiments/rewrite_lift_lets_map.v#L186-L189
(It seems to me like it's a mis-feature for the bench to disable the native compiler, since then native compiler changes can never get benched...)
enabling native-compiler lead to such instability to get very active pushback @Jason Gross
because of OCaml (performance) bugs, or Coq using OCaml in ways that are not supported, performance-wise
basically, since a while ago until the recent CEP, Coq defaulted to native_compiler=ondemand
: then it only slowed down Coq very little, but native_compute
had to recompile dependencies, so it was slow and seldom useful
because ondemand
didn't have enough caching to save the compiled result across files (basically)
now Coq tends to have it enabled or disabled, and if we enable it, files are compiled eagerly, so installing packages is slower but native_compute
becomes useful more often!
(and if it's disabled, it's actually disabled — this is the default, and is changed in opam by installing the coq-native
package that acts as an opam flag)
also, enabling it reveals it works less well than people hoped. So it's been made opt-in for CI.
This isn't the CI, though, this is the bench
I realize, and I don't know the default there
and sure, seems opting-in to native benchs should be allowed
As of today, vst and compcert are still failing on the bench due to what looks like broken opam packages.
There was a thread back in January where the compcert failure was blamed upon an interaction with Flocq (it works with the submodule version but not the released one).
I don't remember discussing the VST failure though.
What should be done? It's a bit annoying since these are two flagship Coq devs.
VST in particular proved to be useful in the change of case representation, since it's super sensitive to unification heuristics for case nodes (!).
Maybe we've been wreaking havoc since then, because we have no way to really check.
vst depends on compcert
ok, but why is compcert still failing in the first place?
because it depends on flocq3 but flocq.dev is flocq4 iirc
that's still the same reason as in January, and this looks like a serious bug to me.
this means a big schism in the set of libraries, depending on whether you're flocq3 or flocq4
Last updated: Oct 13 2024 at 01:02 UTC