# Ask For Basic Commands For COQ

**URL:** <https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418>\
**Category:** Miscellaneous\
**Created:** [August 27, 2021, 11:36am UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418 "2021-08-27T11:36:57Z")\
**Posts on this page:** 16\
**Page:** 1

<div class="post-metadata">

**Author:** ![lyl](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyl/32/575_2.png) [@lyl](https://discourse.rocq-prover.org/u/lyl)\
**Post date:** [August 27, 2021, 11:36am UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/1 "2021-08-27T11:36:57Z")

</div>

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!

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [August 28, 2021, 7:46am UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/2 "2021-08-28T07:46:29Z")

</div>

To get started with Coq, it might be easier to try CoqIDE — documented here:  
[https://coq.inria.fr/refman/practical-tools/coqide.html](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.

---

<div class="post-metadata">

**Author:** ![lyl](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyl/32/575_2.png) [@lyl](https://discourse.rocq-prover.org/u/lyl)\
**Post date:** [August 28, 2021, 9:28am UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/3 "2021-08-28T09:28:47Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [August 28, 2021, 12:29pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/4 "2021-08-28T12:29:50Z")

</div>

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:

```auto
$ 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:

```auto
opam update
opam install coq coq-vst.2.8 coqide

```

then

```auto
coqide file.v

```

and start using coq from an editor instead of from the terminal.  
Hope this heps.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [August 28, 2021, 1:40pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/5 "2021-08-28T13:40:53Z")

</div>

> [@lyl](#):
>
> So, I think it is more convenient to use `opam` to install Coq and the right version VST.

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`.

> [@lyl](#):
>
> The version of the VST installed in CoqIDE is not the same as that demanded by the book.

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.

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [August 29, 2021, 5:23pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/6 "2021-08-29T17:23:35Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![lyl](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyl/32/575_2.png) [@lyl](https://discourse.rocq-prover.org/u/lyl)\
**Post date:** [August 31, 2021, 2:47pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/7 "2021-08-31T14:47:13Z")

</div>

> [@Blaisorblade](#):
>
> 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` .

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.

> [@Blaisorblade](#):
>
> 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.

When I tried to run `Preface.v` in CoqIDE, it said

```auto
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

 ![Sans titre 2](https://us1.discourse-cdn.com/flex001/uploads/coq/original/1X/59518893833e3a21607af95128ee350ef3804969.jpeg). So, I have installed VST 2.8 as needed.

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.

---

<div class="post-metadata">

**Author:** ![lyl](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyl/32/575_2.png) [@lyl](https://discourse.rocq-prover.org/u/lyl)\
**Post date:** [August 31, 2021, 2:51pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/8 "2021-08-31T14:51:05Z")

</div>

> [@Matafou](#):
>
> 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.

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.

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [August 31, 2021, 4:28pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/9 "2021-08-31T16:28:35Z")

</div>

> [@lyl](#):
>
> When I tried to run `Preface.v` in CoqIDE, it said
> 
> ```auto
> 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.

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.

1. What is your os?
2. 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.

---

<div class="post-metadata">

**Author:** ![lyl](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyl/32/575_2.png) [@lyl](https://discourse.rocq-prover.org/u/lyl)\
**Post date:** [August 31, 2021, 5:01pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/10 "2021-08-31T17:01:43Z")

</div>

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.

```auto
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 ?

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [August 31, 2021, 5:17pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/11 "2021-08-31T17:17:05Z")

</div>

OK but how do you launch coqide? From the terminal? If yes, try `which coqide`.

---

<div class="post-metadata">

**Author:** ![lyl](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyl/32/575_2.png) [@lyl](https://discourse.rocq-prover.org/u/lyl)\
**Post date:** [August 31, 2021, 8:53pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/12 "2021-08-31T20:53:26Z")

</div>

I just downloaded the dmg file and installed it. And I just click on the coq\_platform icon to open it. That’s all.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [September 1, 2021, 7:53am UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/13 "2021-09-01T07:53:28Z")

</div>

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:

```auto
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:

> [@lyl](#):
>
> 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.`

The simplest way to avoid confusion between the two installation is to uninstall the Coq Platform and only use opam.

---

<div class="post-metadata">

**Author:** ![lyl](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyl/32/575_2.png) [@lyl](https://discourse.rocq-prover.org/u/lyl)\
**Post date:** [September 1, 2021, 12:15pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/14 "2021-09-01T12:15:12Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [September 5, 2021, 4:16pm UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/15 "2021-09-05T16:16:20Z")

</div>

> 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](https://github.com/coq/platform). 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.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [September 8, 2021, 2:20am UTC](https://discourse.rocq-prover.org/t/ask-for-basic-commands-for-coq/1418/16 "2021-09-08T02:20:56Z")

</div>

> [@Matafou](#):
>
> 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:

> <https://github.com/coq/platform/blob/2021.02/README_macOS.md>