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)
Xavier has been busy silencing the 8.13 warnings by rewriting Hint
into Global Hint
. I am surprised this had such an effect.
that change isn't supposed to have an effect though
https://github.com/AbsInt/CompCert/commit/aba0e740f25ffa5c338dfa76cab71144802cebc2 also possible cause
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.
Changes in other files
the "replace omega" commit changes it, not just others
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.
nobody notices bench failures
here's a compcert failure from the 7th https://gitlab.com/coq/coq/-/jobs/949773128
(3 weeks ago)
by the way, how did you find that it is this line of IEEE754_extra.v
which fails?
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
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.
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.
this one https://gitlab.com/coq/coq/-/jobs/957716419/ says "no applicable tactic" from 2 weeks ago, ie after "replace omega"
Hint Rewrite also warns on master (but not 8.13)
Ah, right.
https://gitlab.com/coq/coq/-/jobs/932639501/ from before "replace omega" succeeded
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.
(So, omega
was a red herring.)
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)
to point to the right branch (and not #master)
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
the overlay should just be pushed upstream, I guess @Michael Soegtrop did not have the time to do it.
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.
# The following term contains unresolved implicit arguments:
# [...]
# More precisely:
# - ?Hmax: Cannot infer this placeholder of type "prec < emax" in
# environment:
# prec, emax : Z
# prec_gt_0_ : Prec_gt_0 prec
# prec_lt_emax_ : Prec_lt_emax prec emax
# n : Z
#
# make[1]: *** [Makefile:261: lib/IEEE754_extra.vo] Error 1
looks like Flocq stuff
also fiat-crypto-with-bedrock
# File "/home/gitlab-runner/builds/y9yFkek2/0/coq/coq/_bench/opam.NEW/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-fiat-crypto-with-bedrock.dev/rupicola/bedrock2/compiler/src/compiler/FitsStack.v", line 191, characters 12-36:
# Error:
# Found no subterm matching "map.get (map.put ?M4480 ?M4481 ?M4482) ?M4481" in the current goal.
Last updated: May 28 2023 at 16:30 UTC