I have successfully installed Coq with opam. From the terminal, after typing eval $(opam env) and coqtop, I am able to launch Coq and write Coq code. However, I don’t know how to save the code. I still would like to know how to open the specific .v. So, is there any tutorial illustrating these basic commands for coq from the terminal? Thank you very much!
To get started with Coq, it might be easier to try CoqIDE — documented here:
https://coq.inria.fr/refman/practical-tools/coqide.html.
Alternatives include VSCoq (a plugin for Visual Studio Code).
For users who are comfortable with Emacs, there is also Proof General, but nowadays you do not need to learn Emacs to use Coq.
Yes, I have been using CoqIDE. However, when I tried to learn Verifiable C to verify C code, the book “Verifiable C” asked me to install VST 2.8. The version of the VST installed in CoqIDE is not the same as that demanded by the book. So, I think it is more convenient to use opam to install Coq and the right version VST. That’s the reason why I asked this question. Thank you.
Hi,
coqide does not install libraries. opam does, so if the version of vst seen by coqide is not the good version you probably need to upgrade your package.
Today:
$ opam list coq-vst
# Packages matching: (installed | available) & name-match(coq-vst)
# Package # Installed # Synopsis
coq-vst.2.2 -- Verified Software Toolchain
coq-vst.2.6 -- Verified Software Toolchain
coq-vst.2.7 -- Verified Software Toolchain
coq-vst.2.7.1 -- Verified Software Toolchain
coq-vst.2.8 -- Verified Software Toolchain
So you probably need this:
opam update
opam install coq coq-vst.2.8 coqide
then
coqide file.v
and start using coq from an editor instead of from the terminal.
Hope this heps.
1 Like
Okay, but coqtop is not very useful and does not have a way to save files. 
on opam install coq coq-vst.2.8 coqide.
I wonder how that happened — either you had an old package as @Matafou says, or a CoqIDE package bundled with a separate Coq install. In the latter case, might be simplest to uninstall that in favor of the opam package.
Please give the error displayed by coq when you try to load the library.
I insist: coqide is NOT a package manager. It CANNOT install anything and it does NOT come with vst. You must have install vst by yourself.
The current opam package for vst (called coq-vst) is 2.8 so with the opam command I gave it should work. Did you try it? Don’t forget to uninstall any other version of coq/coqide/coqtop/vst you had installed before.
Last but not least: coqide IS the alternative to coqtop you are asking for.
It seems that this installation command does not change the configuration of coqide. Now, I am using coqtop to run program, because I can use opam to install the vst of right version. So, that’s why I am using CoqIDE (check, save the code, etc.) and coqtop at the same time.
When I tried to run Preface.v in CoqIDE, it said
Tactic failure: The wrong version of VST is installed.
You have VST version "2.7" but this version of 'Software Foundations Volume 5: Verifiable C'
demands version "2.8"
So, CoqIDE indeed includes VST 2.7.
When I list the installed vst by using opam list, it shows
To conclude, I may say CoqIDE includes VST2.7 instead of VST2.8. Thus, we have to use opam to download coq and vst of the right version, and run it in the terminal.
I cannot run the compiled .v file in CoqIDE, because the versions of OCaml are not compatible.
The file /Users/liu/vc/stack.vo was compiled with OCaml 4.10.2 while this instance of Coq was compiled with OCaml 4.07.1. Coq object files need to be compiled with the same OCaml toolchain to be compatible.
Thus, can I say it is impossible to run Preface.v in CoqIDE ?
Thank you.
You are quite right! We can CHANGE NOTHING in CoqIDE. So, we have to use the terminal to run the program. It works. Thank you very much!
By the way, when I change the version needed to VST.2.7, I am not able to compile stack.v. This is the error information: Cannot find module Clightdefs.ClightNotations. I am not sure whether it relates to the version of VST or not.
Nope, coqide does not include any library (I mean really). It can only look for libraries installed in you system. So you have installed vst 2.7 a way or another.
- What is your os?
- How do you launch coqide? Are you sure the one from opam is launched?
That said you can launch coqide with -I <path_to_vst_2.8> and it should work.
I am using Mac M1. I use application Coq_Platform_2021.02.1.
When I use opam search coq, it shows the following information about coq-vst.
coq-vst 2.8 Verified Software Toolchain
coq-vst-32 -- Verified Software Toolchain
coq-vst-64 -- Verified Software Toolchain
What is the way to check all the vst installed in my OS? How can I get the path of vst.2.8 ? I have to install coqide by using opam install coqide then use command coqide ... to launch the system instead of clicking on the application directly ?
OK but how do you launch coqide? From the terminal? If yes, try which coqide.
I just downloaded the dmg file and installed it. And I just click on the coq_platform icon to open it. That’s all.
So you have two different and incompatible Coq installations:
- the Coq platform, with VST 2.7 and one version of CoqIDE, reachable from the icon
- the one installed via opam, with VST 2.8 and a different CoqIDE version, that you can probably launch from the terminal as follows:
eval $(opam env)
coqide &
Those two installations are independent, and opam will not affect the first one.
Different Coq installations often produce incompatible .vo files. That explains this error:
The simplest way to avoid confusion between the two installation is to uninstall the Coq Platform and only use opam.
It’s done. I tried brew install coqide to install coqide, because it asked me to install several packages when I used opam install coqide. I’ve found the installed coqide didn’t work. Then I installed all the packages needed, so I was able to install coqide by opam install coqide. Finally, I tried to compile the file Preface.v. No error exists at this time.
So, in order to practise the Verifable C, we have to use opam to install VST.2.8 and coqide. Right ? The CoqIDE_Platform of dmg version does not meet the configuration requirements for using Verifiable C.
The CoqIDE_Platform of dmg version does not meet the configuration requirements for using Verifiable C.
It seems indeed, as you can see there: GitHub - coq/platform: Multi platform setup for Coq, Coq libraries and tools. But as they explain in this page coq_platform uses opam itself so once you have installed coq_platform you can update the packages by hand with regular opam commands. This is what you actually did.
Not quite: that doesn’t work on Mac packages, both the old ones and the new ones — as confirmed by the platform docs, and consistent with all messages above: