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