Error message `Coq object files need to be compiled with the same OCaml toolchain to be compatible.`

[eleehiga]

Currently I am trying to verify verif_sumarray.v (from https://github.com/PrincetonUniversity/VST/blob/master/progs/verif_sumarray.v) but on the first line Require Import VST.floyd.proofauto. it has an error message that says:

The file /home/test/VST/floyd/proofauto.vo was compiled with OCaml 4.08.1
while this instance of Coq was compiled with OCaml 4.13.1.
Coq object files need to be compiled with the same OCaml toolchain to be compatible.

Can you please assist me to fix this error?

[QinshiWang]

As shown, you are using VST from the source code. You might want to use the OPAM version. If you wish to continue using this version, you need to recompile it, because you updated Coq after compiling VST. After changing Coq version, you have to recompile every Coq project.

[eleehiga]

@QinshiWang How do I get the OPAM version? But I probably agree and want to continue using this version. Therefore by recompiling do you mean to run make again?

[eleehiga]

Actually maybe not running make again as when I ran make that yielded the error message: Makefile:130: *** COMPCERT VERSION MISMATCH: COMPCERT_VERSION=version=3.11 but /snap/coq-prover/30/coq-platform/2022-04-1/lib/coq/user-contrib/compcert/VERSION=version=3.10. Stop. Therefore how would you suggest for me to recompile VST?

[eleehiga]

@QinshiWang Actually I think I have the OPAM version with coq-vst, but how do I use coq-vst?

[QinshiWang]

Could you run the follow script to see what have been installed?

opam list --installed coq-*

[eleehiga]

This is what that command returns:

# Packages matching: installed & name-match(coq-*)
# Name        # Installed # Synopsis
coq-compcert  3.11        The CompCert C compiler (64 bit)
coq-flocq     4.1.0       A formalization of floating-point arithmetic for the Coq system
coq-menhirlib 20211128    A support library for verified Coq parsers produced by Menhir
coq-vst       2.10        Verified Software Toolchain

[QinshiWang]

Then you can include by Require Import VST.floyd.proofauto. See the VST user manual for more information.

[eleehiga]

@QinshiWang The error:

The file /home/test/VST/floyd/proofauto.vo was compiled with OCaml 4.08.1
while this instance of Coq was compiled with OCaml 4.13.1.
Coq object files need to be compiled with the same OCaml toolchain to be compatible.

happens when executing the line Require Import VST.floyd.proofauto.

[eleehiga]

@QinshiWang Is it that I am supposed to call proofauto.vo from coq-vst and not source code? And if so how would you recommend me to do that?

[QinshiWang]

You can make clean in your VST source code. And for particular examples you want to run, you can build AST files (e.g., revarray.v) in CoqIDE and then go to verif_revarray.v.

[eleehiga]

@QinshiWang When I run make clean the error message Makefile:130: *** COMPCERT VERSION MISMATCH: COMPCERT_VERSION=version=3.11 but /snap/coq-prover/30/coq-platform/2022-04-1/lib/coq/user-contrib/compcert/VERSION=version=3.10. Stop. appears. Was wondering how you would recommend me to solve that error? And yes I have the AST and verif_ files in the VST/progs folder, that is good right?

[mansky1]

It seems likely that your problem is you have two different Coq installations, one through OPAM and one through Snap. If you want to use everything through OPAM, you're best off uninstalling the Coq Snap package.

[QinshiWang]

I have no idea what is Snap.

[mansky1]

@QinshiWang It's a package manager for Linux that provides precompiled programs (similar to apt or brew, if you've ever used those).

[mansky1]

Following up on this, if you want to have two versions of Coq on your computer for some other reason (I've done this for development), you can set the COQBIN environment variable before running make (e.g., export COQBIN=~/.opam/.../coq/bin/ depending on where your OPAM installation lives).

[eleehiga]

Ah ok that sounds good and I do want to uninstall the coq snap package.

[eleehiga]

@QinshiWang and @mansky1 I have installed Coq with Opam and uninstalled the Snap Coq but in verif_sumarray.v (from the cloned git VST source in the progs folder) when running the line Require Import VST.progs.sumarray. that yields the error message Cannot find a physical path bound to logical path matching suffix VST.progs. Can you guys please assist me to fix this error? And also just to make sure I am not supposed to run make as an attempt to fix this right?

[mansky1]

For this, you need to do two things:

1. Use the clightgen tool from CompCert to generate sumarray.v from sumarray.c, if it's not already present.
2. Compile sumarray.v with Coq. I think you won't need any special arguments or options.

This is the procedure for processing C programs in VST, whether they're existing examples or ones you wrote. You can find more information in chapter 3 of the manual (https://raw.githubusercontent.com/PrincetonUniversity/VST/master/doc/VC.pdf), and if you intend to use VST in depth, I would also recommend working through some of the Software Foundations volume on VST (https://softwarefoundations.cis.upenn.edu/vc-current/index.html).

[eleehiga]

@mansky1 to compile sumarray.v would I run coqc sumarray.v or something else? This is as when I did coqc sumarray.v there still is the error Cannot find a physical path bound to logical path matching suffix VST.progs.. Also sounds good for if I do want to use clightgen, find more info, and if I would want to use VST in depth.

[eleehiga]

Actually turns out to fix this error I changed the line to Require Import sumarray.. But I was wondering what would the solution to this problem be without changing that line?

[mansky1]

You would make a _CoqProject file that said something like -Q . VST.progs and pass it to coqc. This is the standard way to give your files a namespace in Coq, not something VST-specific.

[eleehiga]

@mansky1 How do I pass _CoqProject to coqc? Is it something like coqc _CoqProject sumarray.v?

[eleehiga]

Also for running the line #[export] Instance CompSpecs : compspecs. there is the error message export attribute not supported here. Was wondering how you would suggest me to fix that error?

[mansky1]

1. Actually, if you only have one option, it might be easier to just pass it directly: coqc -Q . VST.progs sumarray.v. If you're building a bigger project, https://coq.github.io/doc/master/refman/practical-tools/utilities.html has a good overview of how to set it up with a _CoqProject file.
2. The current version of the VST repo is one or two Coq versions ahead of the OPAM version. Fortunately, you should be able to solve this just by removing the #[export], and that won't have any effect on the proofs in this file.

[eleehiga]

@mansky1 I ran coqc -Q . VST.progs sumarray.v but I still get the error Cannot find a physical path bound to logical path matching suffix VST.progs. at the line Require Import VST.progs.sumarray.. Was wondering if there is another solution you would recommend me to try?

[eleehiga]

Also thank you as removing #[export] did work

[mansky1]

@mansky1 I ran coqc -Q . VST.progs sumarray.v but I still get the error Cannot find a physical path bound to logical path matching suffix VST.progs. at the line Require Import VST.progs.sumarray.. Was wondering if there is another solution you would recommend me to try?

Okay, for this to work you should also have a _CoqProject file with -Q . VST.progs in that folder. CoqIde will automatically load that _CoqProject file when you open another file in the folder.

[eleehiga]

Ah ok I made a _CoqProject file with -Q . VST.progs but it still has the same error.

[mansky1]

It worked for me, so let's troubleshoot. First, I was assuming you were using CoqIde when you got this error -- is that true? If so, did you close and reopen it after making the _CoqProject file? And is your _CoqProject in the same folder as sumarray.v and verif_sumarray.v?

[eleehiga]

@mansky1 Closing and reopening the IDE made it work. Thank you and @QinshiWang for taking the time to assist me with all of this.