Stream: Coq devs & plugin devs

Topic: bench failing packages


view this post on Zulip Gaëtan Gilbert (Jan 12 2021 at 15:03):

failed to install coq-performance-tests-lite coq-sf-plf
(eg https://gitlab.com/coq/coq/-/jobs/907722827)
what can we do about this?

view this post on Zulip Gaëtan Gilbert (Jan 12 2021 at 15:03):

cc @Jason Gross

view this post on Zulip Jason Gross (Jan 12 2021 at 16:25):

Where did coq-performance-tests-lite fail? What's the error message/file/log?

view this post on Zulip Gaëtan Gilbert (Jan 12 2021 at 16:30):

logs are in the artifacts

view this post on Zulip Gaëtan Gilbert (Jan 12 2021 at 16:31):

>

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:

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.

/home/gitlab-runner/builds/6WQk5HVP/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-performance-tests-lite.dev/PerformanceExperiments/Makefile.generated-files:23: recipe for target 'rewrite_lift_lets_map/_4_SuperFast.log' failed

view this post on Zulip Jason Gross (Jan 15 2021 at 18:38):

@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

A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross] - coq-community/coq-performance-tests

view this post on Zulip Jason Gross (Jan 15 2021 at 18:39):

(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...)

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:31):

enabling native-compiler lead to such instability to get very active pushback @Jason Gross

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:33):

because of OCaml (performance) bugs, or Coq using OCaml in ways that are not supported, performance-wise

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:34):

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_computehad to recompile dependencies, so it was slow and seldom useful

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:35):

because ondemand didn't have enough caching to save the compiled result across files (basically)

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:36):

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!

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:37):

(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)

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:40):

also, enabling it reveals it works less well than people hoped. So it's been made opt-in for CI.

view this post on Zulip Jason Gross (Jan 16 2021 at 01:16):

This isn't the CI, though, this is the bench

view this post on Zulip Paolo Giarrusso (Jan 16 2021 at 01:24):

I realize, and I don't know the default there

view this post on Zulip Paolo Giarrusso (Jan 16 2021 at 01:25):

and sure, seems opting-in to native benchs should be allowed

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2021 at 17:12):

As of today, vst and compcert are still failing on the bench due to what looks like broken opam packages.

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2021 at 17:12):

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).

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2021 at 17:12):

I don't remember discussing the VST failure though.

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2021 at 17:13):

What should be done? It's a bit annoying since these are two flagship Coq devs.

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2021 at 17:13):

VST in particular proved to be useful in the change of case representation, since it's super sensitive to unification heuristics for case nodes (!).

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2021 at 17:14):

Maybe we've been wreaking havoc since then, because we have no way to really check.

view this post on Zulip Gaëtan Gilbert (Aug 08 2021 at 17:24):

vst depends on compcert

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2021 at 17:54):

ok, but why is compcert still failing in the first place?

view this post on Zulip Gaëtan Gilbert (Aug 08 2021 at 17:59):

because it depends on flocq3 but flocq.dev is flocq4 iirc

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2021 at 18:00):

that's still the same reason as in January, and this looks like a serious bug to me.

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2021 at 18:01):

this means a big schism in the set of libraries, depending on whether you're flocq3 or flocq4


Last updated: Oct 16 2021 at 10:02 UTC