Stream: Coq devs & plugin devs

Topic: compcert failing in bench?


view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 09:06):

seems to fail on https://github.com/AbsInt/CompCert/blob/25483cf1acce8695a438f4f2164b09fb1ecd9d2e/lib/IEEE754_extra.v#L305 with "no applicable tactic"
see https://gitlab.com/coq/coq/-/jobs/993262537
(the lambda-rust failure is spurious because of a printing change in that PR, the perf test and sf failures are already known)

view this post on Zulip Guillaume Melquiond (Jan 29 2021 at 09:37):

Xavier has been busy silencing the 8.13 warnings by rewriting Hint into Global Hint. I am surprised this had such an effect.

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 09:50):

that change isn't supposed to have an effect though

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 09:57):

https://github.com/AbsInt/CompCert/commit/aba0e740f25ffa5c338dfa76cab71144802cebc2 also possible cause

view this post on Zulip Guillaume Melquiond (Jan 29 2021 at 10:19):

None of that makes sense, the failing file is standalone. (The only dependency is Flocq, and the bench is now using the external Flocq rather than the one of CompCert.) Changes in other files should not affect it. Also, needless to say, the file compiles fine on 8.13.

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 10:22):

Changes in other files

the "replace omega" commit changes it, not just others

view this post on Zulip Guillaume Melquiond (Jan 29 2021 at 10:24):

Sure, but that commit was pushed one month ago, we should have seen it fail before. In fact, the ci-compcert job goes through just fine. So the issue is specific to the bench job.

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 10:27):

nobody notices bench failures
here's a compcert failure from the 7th https://gitlab.com/coq/coq/-/jobs/949773128

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 10:27):

(3 weeks ago)

view this post on Zulip Guillaume Melquiond (Jan 29 2021 at 10:33):

by the way, how did you find that it is this line of IEEE754_extra.v which fails?

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 10:36):

the bench jobs have the logs in the artifact
so for instance from https://gitlab.com/coq/coq/-/jobs/949773128 you can click "browse" on the right and continue to _bench/logs finally getting to https://gitlab.com/coq/coq/-/jobs/949773128/artifacts/file/_bench/logs/coq-compcert.NEW.opam_install.deps_only.stderr.log
which makes me notice the 3 weeks old error was in menhir btw, I guess it got solved at some point

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 10:37):

but the recent log at https://gitlab.com/coq/coq/-/jobs/993262537/artifacts/file/_bench/logs/coq-compcert.NEW.opam_install.1.stderr.log says

# File "./lib/IEEE754_extra.v", line 305, characters 2-5:
# Error: No applicable tactic.

view this post on Zulip Guillaume Melquiond (Jan 29 2021 at 10:43):

Something else is going wrong. If you look a few lines before, there are warnings about Hint. Yet, as I said, Xavier did remove all of them. So, I am a bit confused as to which CompCert's commit is being compiled.

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 10:43):

this one https://gitlab.com/coq/coq/-/jobs/957716419/ says "no applicable tactic" from 2 weeks ago, ie after "replace omega"

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 10:46):

Hint Rewrite also warns on master (but not 8.13)

view this post on Zulip Guillaume Melquiond (Jan 29 2021 at 10:47):

Ah, right.

view this post on Zulip Gaëtan Gilbert (Jan 29 2021 at 10:47):

https://gitlab.com/coq/coq/-/jobs/932639501/ from before "replace omega" succeeded

view this post on Zulip Guillaume Melquiond (Jan 29 2021 at 11:10):

So, it succeeds with embedded Flocq and with released Flocq. But it fails with the dev version of Flocq. The master branch of Flocq is known to be incompatible with CompCert, so it is not that surprising, in hindsight.

view this post on Zulip Guillaume Melquiond (Jan 29 2021 at 11:17):

(So, omega was a red herring.)

view this post on Zulip Enrico Tassi (Jan 29 2021 at 12:54):

I guess the fix is to this line https://github.com/coq/opam-coq-archive/blob/3507879a38f6381ad960823ed146d68d04d3ffd8/extra-dev/packages/coq-compcert/coq-compcert.dev/opam#L35 , use ... | 3.dev (and provide that package)

view this post on Zulip Enrico Tassi (Jan 29 2021 at 12:55):

to point to the right branch (and not #master)

view this post on Zulip Enrico Tassi (Jan 29 2021 at 12:57):

Now I understand: the platform CI did work, but it has a local overlay for compcert and the 3.dev package https://github.com/coq/platform/tree/master/opam/packages/coq-flocq/coq-flocq.3.dev

view this post on Zulip Enrico Tassi (Jan 29 2021 at 12:57):

the overlay should just be pushed upstream, I guess @Michael Soegtrop did not have the time to do it.

view this post on Zulip Michael Soegtrop (Jan 30 2021 at 11:00):

the overlay should just be pushed upstream, I guess @Michael Soegtrop did not have the time to do it.

Yes, I am a bit behind with pushing the Coq Platform local patches upstream - the fix for gappa dev on macOS homebrew took me a while (it requires a slightly controversial opam hack - symlinking system stuff into the opam switch bin folder).

I will first try to get the 8.13 CI running again (some strange issues with mathcomp and then this funny effect with a git tar file changing its hash) and then look into CompCert dev. Please feel free to create an upstream PR from the patch in Coq platform.


Last updated: Oct 21 2021 at 22:02 UTC