proliferation of Local in files with program logic proofs about bedrock2 HOT 3 OPEN

Q: Why not Import instead of Load such a file?
A: There are settings (such as eg Printing Width, reserved notations) which follow Require (as opposed to other settings which follow Require Import), and in order to make them not follow anything, you can prefix them with Local, but then these settings can't be put into a shared file and pulled into the program logic proof files via Import, so we'll have to use Load, which "inlines" the loaded file.

from bedrock2.

Turns out Load isn't that easy either because paths

130 andres-erbsen@andres-erbsen-sifive /tmp % find b                                                                                                                                                              :(
b
b/a.glob
b/.a.aux
b/a.v
b/b.v
andres-erbsen@andres-erbsen-sifive /tmp % coqc b/a.v
File "./b/a.v", line 1, characters 0-11:
Error: Can't find file b.v on loadpath

could we somehow make things so that for each file, emacs and makefile call coq from the same working directory?

coq/coq#8649 coq/coq#8649 coq/coq#4953

from bedrock2.

emacs changes the working directory to the directory of the file of the current buffer before invoking coqtop, and while we might be able to change that behavior using some emacs hacks, I'd rather not have a solution which depends on the current working directory.

Coq's Load command calls find_file_in_path in lib/system.ml, which distinguishes between "implicit paths" and "non implicit paths" (according to what Filename.is_implicit returns).
If you put a "non implicit path" (i.e. one which starts with ., .., or the root /) after the Load, Coq will use the file system's behavior to look for the file, and this depends on the current working directory of the coq process, which we want to avoid.
On the other hand, if you put an "implicit path" after the Load, Coq will loop through all paths in the loadpath, append that implicit path to each of them, and pick the first file which exists, emitting a warning if several exist.

So the following works both for compliation from the command line, and within emacs:

[sam@samsdell tmp]$ find src
src
src/b.v
src/a.vo
src/mysubdir
src/mysubdir/c.v
src/a.glob
src/a.v~
src/a.v
src/.a.aux
[sam@samsdell tmp]$ cat src/b.v 
Definition foo: nat := 5.
[sam@samsdell tmp]$ cat src/mysubdir/c.v 
Definition bar: nat := 6.
[sam@samsdell tmp]$ cat src/b.v 
Definition foo: nat := 5.
[sam@samsdell tmp]$ cat src/a.v
Load "b.v".
Load "mysubdir/c.v".
Print foo.
Print bar.
[sam@samsdell tmp]$ coqc -Q ./src b ./src/a.v 
foo = 5
     : nat
bar = 6
     : nat
[sam@samsdell tmp]$ cat _CoqProject 
-Q ./src b
[sam@samsdell tmp]$ emacs ./src/a.v

from bedrock2.