Gaëtan Gilbert (Jan 29 2021 at 09:06): 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)
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.
Gaëtan Gilbert (Jan 29 2021 at 09:50):that change isn't supposed to have an effect though
Gaëtan Gilbert (Jan 29 2021 at 09:57):https://github.com/AbsInt/CompCert/commit/aba0e740f25ffa5c338dfa76cab71144802cebc2 also possible cause
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.
Gaëtan Gilbert (Jan 29 2021 at 10:22):Changes in other files
the "replace omega" commit changes it, not just others
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.
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
Gaëtan Gilbert (Jan 29 2021 at 10:27):(3 weeks ago)
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?
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
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.
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.
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"
Gaëtan Gilbert (Jan 29 2021 at 10:46):Hint Rewrite also warns on master (but not 8.13)
Guillaume Melquiond (Jan 29 2021 at 10:47):Ah, right.
Gaëtan Gilbert (Jan 29 2021 at 10:47):https://gitlab.com/coq/coq/-/jobs/932639501/ from before "replace omega" succeeded
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.
Guillaume Melquiond (Jan 29 2021 at 11:17):(So, omega was a red herring.)
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)
Enrico Tassi (Jan 29 2021 at 12:55):to point to the right branch (and not #master)
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
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.
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.
Gaëtan Gilbert (May 10 2022 at 11:47):# 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
Gaëtan Gilbert (May 18 2022 at 10:38):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: Apr 20 2024 at 10:02 UTC