Doesn't work in coqide

[benlaurie]

https://github.com/project-oak/silveroak/blob/d7dce7914483e6545dbd8238b7b235b2d67931c7/demos/tutorial.v#L57

Presumably because you have to do something to make it aware of the _CoqProject.

[jadephilipoom]

We should add something to the README install instructions that addresses this (and maybe links to Coq installation instructions and installation instructions for different IDE options).

[satnam6502]

I've used tutorial.v in VS Code and Emacs without issue. I think you have to make sure you build first, because we now generate the _CoqProject file and then run the tool in the right directory e.g. after building I have to do:

$ code .

In the root silveroak directory to get all the Coq paths to work out. I don't use CoqIDE any more but I recall I think a similar situation.

[satnam6502]

Just checked and works out of the box for me with CoqIDE just launched from the toolbar.

[satnam6502]

Ben, what does your root _CoqProject file look like?

[benlaurie]

It is exactly the one in the repo...

[satnam6502]

@blaxill @jadephilipoom can you please help Ben out? Ben, did you do a make to build the system before running CoqIDE? Again, it just seems to work for me so I can't repo what you are experiencing.

[jadephilipoom]

I also installed CoqIDE to check and didn't get any problems running the tutorial. Starting from a fresh clone, I ran:

$ git clone --recursive https://github.com/project-oak/silveroak.git fresh-silveroak
$ cd fresh-silveroak
$ make -j6 cava
$ coqide demo/tutorial.v

Ben, can you replicate that process? I think you'd indeed get the error you're describing if make failed for some reason (the imports would fail because the binaries don't exist).

[jadephilipoom]

Note that we've recently upgraded to Coq 8.13 -- if you have 8.12, check out the commit just before the upgrade:

$ git clone --recursive https://github.com/project-oak/silveroak.git fresh-silveroak
$ cd fresh-silveroak
$ git checkout 3cee9ca81354603d1fc766d189684e09bb9c7baa
$ git submodule update --recursive # check out 8.12 versions of dependencies
$ make -j6 cava
$ coqide demo/tutorial.v

[benlaurie]

I'm on a new laptop, and I installed the Coq Platform - now it works when I load the tutorial, so I guess I got my old machine into a weird state (it did end up with several different versions of Coq installed in different ways).

Now the problem I have is that if I want to start a new Coq file using Cava I have to save it somewhere in the silveroak tree and then close and re-open before I can load Cava. Perhaps there's a better way?

[benlaurie]

Note that if you are reading the tutorial as a web page (presumably common) this is exactly what you will do, so it seems there's a missing step between "install Cava" and Require Import Cava.Cava (I think this is, actually, my original problem).

[jadephilipoom]

@benlaurie , is this resolved by the more detailed build instructions added in #773? (Maybe easier to read on the tutorial page itself: https://project-oak.github.io/silveroak/demo/tutorial#id1)

[benlaurie]

Hmm. Now I have a new problem - when I try to import Cava.Cava after those instructions, I get:

Compiled library Cava.Cava (in file /Users/benl/git-work/silveroak/cava/Cava/Cava.vo) makes inconsistent assumptions over library ExtLib.Structures.MonadCompiled library Cava.Cava (in file /Users/benl/git-work/silveroak/cava/Cava/Cava.vo) makes inconsistent assumptions over library ExtLib.Structures.Monad

[satnam6502]

You often get this when you have some files compiled with different versions of Coq. Does cleaning everything and rebuilding work?

[benlaurie]

This was a fresh checkout, so presumably it won't but I'll try.

[benlaurie]

It doesn't make any difference - also, don't you get a different error if versions don't match (i.e. a version mismatch error).

[benlaurie]

It turns out I had a typo in _CoqProject, so the Extlib directory did not exist. Not a helpful error message!

[jadephilipoom]

From the discussion, it looks like this issue was resolved (assuming we're not going to fix Coq's unhelpful error messages!) so I'm closing.