Stream: Coq users

Topic: What to do if Coq behaves differently on different machines?


view this post on Zulip YoungJu Song (Jun 23 2021 at 06:37):

Hi all,
I am facing a very strange situation where I have two different machines with exactly same Ocaml, Coq and package versions but coqc behaves differently.
Is there any advice on resolving this situation?

view this post on Zulip Théo Winterhalter (Jun 23 2021 at 06:42):

How differently? Like it doesn't accept or generate the same goals?

view this post on Zulip YoungJu Song (Jun 23 2021 at 07:14):

Yes, the "Prelude.f_equal" tactic behaves differently and made different goals, so in one machine compilation succeeds while in the other it fails.

view this post on Zulip Christian Doczkal (Jun 23 2021 at 07:40):

That appears very odd (unlikely). Are you absolutely certain you are running the same version of Coq on both machines? Sometimes there are multiple versions (i.e., one installed via opam and one via the systems package mananger).

view this post on Zulip YoungJu Song (Jun 23 2021 at 07:53):

Yes, coqc --version and opam list gives the same result.

view this post on Zulip Théo Winterhalter (Jun 23 2021 at 07:56):

And you test compilation with which command or in which IDE?

view this post on Zulip YoungJu Song (Jun 23 2021 at 08:00):

I use a Makefile generated from coq_makefile, which uses coqc.

view this post on Zulip Michael Soegtrop (Jun 23 2021 at 08:20):

It might be that you have environment variables set, which redirect coq's standard library. Also t is worthwhile to double check which coqc and coqc -where. Also did you run eval $(opam env)?

view this post on Zulip YoungJu Song (Jun 25 2021 at 03:28):

I guess if environment variable has redirected the stdlib into another version's one, it should have gave me version mismatch error message (magic number thing), but it does not. Actually, the glitch happens only once in 30K loc of code and the rest compiles well.
I checked which coqc and coqc -where and it gives me the same result. I also ran eval $(opam env).

view this post on Zulip YoungJu Song (Jun 25 2021 at 03:31):

I have tried it in other machines (with clean build) too and only one machine (ASUS amd laptop with ubuntu installed) shows different behavior.

view this post on Zulip Michael Soegtrop (Jun 25 2021 at 07:10):

I would say then you should .tar.gz the complete opam switch folder and upload it somewhere together with your Coq code (or a minimal reproducible example), so that people can reproduce and look into it.


Last updated: Feb 08 2023 at 22:03 UTC