Stream: Coq devs & plugin devs

Topic: coqchk in test-suite/bugs/

view this post on Zulip Ali Caglayan (Apr 05 2022 at 20:20):

While working on the dune test-suite I noticed that we don't call coqchk for closed bugs. Curious, I tried running coqchk in bugs/ to find that 9 tests fail with exit code 129, presumably with an anomaly. Do we not expect coqchk to pass on these?

Here is an example:

$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_2923.vo) &> _build/default/test-suite/bugs/bug_2923.v.chk.log
Fatal Error: Anomaly "Uncaught exception Modops.ModuleTypingError(_)."
             Please report at http://coq.inria.fr/bugs/.

view this post on Zulip Ali Caglayan (Apr 05 2022 at 20:26):

Here is a full list:

$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_2923.vo) &> _build/default/test-suite/bugs/bug_2923.v.chk.log
$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_2668.vo) &> _build/default/test-suite/bugs/bug_2668.v.chk.log
$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_2141.vo) &> _build/default/test-suite/bugs/bug_2141.v.chk.log
$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_2464.vo) &> _build/default/test-suite/bugs/bug_2464.v.chk.log
$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_1962.vo) &> _build/default/test-suite/bugs/bug_1962.v.chk.log
$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_2467.vo) &> _build/default/test-suite/bugs/bug_2467.v.chk.log
$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_2136.vo) &> _build/default/test-suite/bugs/bug_2136.v.chk.log
$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_2137.vo) &> _build/default/test-suite/bugs/bug_2137.v.chk.log
$(cd _build/default/test-suite/bugs && ../../../install/default/bin/coqchk -silent -o -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -norec bug_2281.vo) &> _build/default/test-suite/bugs/bug_2281.v.chk.log

view this post on Zulip Ali Caglayan (Apr 05 2022 at 20:31):

In fact, all but the first seem to be the same anomaly:

Fatal Error: Anomaly: assert failure
             (file "checker/check.ml", line 98, characters 22-28). Please
             report at http://coq.inria.fr/bugs/.

view this post on Zulip Ali Caglayan (Apr 05 2022 at 20:34):

To run this in your own build, the subshell command should work after make test-suite I believe

view this post on Zulip Gaëtan Gilbert (Apr 05 2022 at 20:36):

the others are probably some funky module issue too looking at the sources

view this post on Zulip Pierre-Marie Pédrot (Apr 05 2022 at 21:03):

this anomaly is probably some issue with abstract

view this post on Zulip Pierre-Marie Pédrot (Apr 05 2022 at 21:20):

ah, no it's actually a pretty innocuous issue

view this post on Zulip Pierre-Marie Pédrot (Apr 05 2022 at 21:21):

it's just that libraries loaded in nonrec mode do not register their opaque table (they don't even load it, for efficiency)

view this post on Zulip Pierre-Marie Pédrot (Apr 05 2022 at 21:23):

the fix is pretty much trivial, I think

view this post on Zulip Ali Caglayan (Apr 05 2022 at 21:31):

Are you talking about the first or the others?

view this post on Zulip Ali Caglayan (Apr 06 2022 at 11:34):

Pierre-Marie Pédrot said:

the fix is pretty much trivial, I think

What's the fix you have in mind?

view this post on Zulip Ali Caglayan (Apr 06 2022 at 18:30):

@Pierre-Marie Pédrot so https://github.com/coq/coq/pull/15911 fixes the second kind of anomaly right? Have you any idea what might be causing the first?

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 20:51):

educated guess: broken module implementation

view this post on Zulip Ali Caglayan (Apr 06 2022 at 20:52):

Btw the others all work with your patch now

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 21:00):

definitely a broken module implementation

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 21:03):

(we have two kernames with the same user name but not the same canonical name, that's an invariant violation)

Last updated: Oct 12 2024 at 13:01 UTC