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?
How differently? Like it doesn't accept or generate the same goals?
Yes, the "Prelude.f_equal" tactic behaves differently and made different goals, so in one machine compilation succeeds while in the other it fails.
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).
coqc --version and
opam list gives the same result.
And you test compilation with which command or in which IDE?
I use a Makefile generated from coq_makefile, which uses coqc.
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)?
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.
which coqc and
coqc -where and it gives me the same result. I also ran
eval $(opam env).
I have tried it in other machines (with clean build) too and only one machine (ASUS amd laptop with ubuntu installed) shows different behavior.
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 01 2023 at 18:01 UTC