YoungJu Song (Jun 23 2021 at 06:37): 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?
Théo Winterhalter (Jun 23 2021 at 06:42):How differently? Like it doesn't accept or generate the same goals?
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.
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).
YoungJu Song (Jun 23 2021 at 07:53):Yes, coqc --version and opam list gives the same result.
Théo Winterhalter (Jun 23 2021 at 07:56):And you test compilation with which command or in which IDE?
YoungJu Song (Jun 23 2021 at 08:00):I use a Makefile generated from coq_makefile, which uses coqc.
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)?
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).
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.
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: Oct 13 2024 at 01:02 UTC