3

I recently switched from Windows to Mac and now CoqIde is not behaving as I'm used to. I'm using Coq 8.9.1 and I don't remember the version I used to use, but it was last updated fall 2018.

On my old machine, I could compile a file (e.g. file1.v to get file1.vo and file1.glob) and then import or export it in another file in the same directory (e.g. writing Require Export file1.) without changing the load path. Now I have to explicitly add the current directory to the load path or I get "Unable to locate library ..." error.

Is this the expected behaviour? I've been away from Coq for a while, but I'm pretty certain I didn't used to have to do this. Adding the current directory to the load path isn't in any of my old work. Is there a way to always have the current directory in the load path?

I read this question and the answers, but the suggestions there look like they all boil down to adding any directory I'm working in to the load path (either in the file I'm working on or somewhere else).

Update:

I was able to get the solution of opening from Terminal at the location of the file to work (resulting in the current file's path being in the LoadPath), but it was more of a headache than I'm used to with Windows.

I had to write a small Bash script in ~/bin/coqide that simply calls /Applications/CoqIDE_8.8.0/Contents/MacOS/coqide. Adding a symbolic link in my home user's binaries directory couldn't find files it expects to be relative to where the symbolic link was called.

I was not able to get the second solution using a _CoqProject file to work in CoqIde and ended up seeing some odd behaviour. Compiling from terminal using coqc worked.

I have added this to the Coq GitHub issue tracker (see here and here).

lady.corvus
  • 95
  • 6
  • 1
    Are you loading CoqIDE from the command line or from a desktop link? One possible explanation is that the "current directory" is not the one you think (in the latter case). – Zimm i48 May 24 '19 at 20:31
  • @Zimmi48 I open from the dock or by clicking a .v file in Finder. In the latter case, CoqIde opens with only the scratch tab and doesn't load the file. When I print the working directory I get "/". Is there a way to get the absolute path of the working directory to check what it is? – lady.corvus May 24 '19 at 23:03
  • 1
    Isn't `/` an absolute path already? In any case, I'd recommend that you open CoqIDE from the console, after having navigated to the directory where your file is. – Zimm i48 May 24 '19 at 23:24

1 Answers1

4

When you open a file with CoqIDE, it won't find the other files you depend on relative to the location of the file you opened but relative to the location where you opened CoqIDE (see also https://github.com/coq/coq/issues/5124).

So one possible solution is the one I mentioned in my comment above (open CoqIDE from the console from where your files are). But fortunately there is another solution that I'd recommend as soon as you are working on a project with several files and which has the advantage of allowing you to open CoqIDE however you want: it is to use a _CoqProject file.

So just create a _CoqProject file wherever your Coq files are with just this line:

-R . MyProjectNamespace

and then all should work magically (provided that you recompile all the files).

Zimm i48
  • 2,901
  • 17
  • 26
  • I tried opening CoqIDE from the directory where I have my .v files, but it's still not able to find the library compiled there. They also don't load when I open from Finder, but the program opens. Is this a bug I should report? Can you please elaborate on the recommendation here? What should MyProjectNamespace be? I've tried making a _CoqProject file with the line you provided but changing MyProjectNamespace to the names of the files or the folder, but I get an error for each of these. Is there some more detailed documentation you can point me to so that I understand what you're suggesting? – lady.corvus May 25 '19 at 23:37
  • 1
    @lady.corvus The namespace is an arbitrary name, and it need not be a file or folder's name. e.g. If the `_CoqProject` file has `-R . Foo`, and there's a file called `Tactics.vo` in the project folder (you should run `coqc Tactics.v` beforehand), then you can import that file using `From Foo Require Import Tactics.` – Bubbler May 26 '19 at 23:46
  • @Zimmi48 thanks for your help! I've marked this answer as accepted, though there are some challenges in getting the first solution to work on macOS. The second solution has some bugs and does not currently work on macOS. – lady.corvus May 27 '19 at 23:16