proliferation of Local in files with program logic proofs

[andres-erbsen]

We should probably make a file that we can Load to set up the correct parsing/elaboration environment for source code, specs, and program logic proofs.

[samuelgruetter]

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.

[andres-erbsen-sifive]

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

[samuelgruetter]

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

[SkySkimmer]

There are settings (such as eg Printing Width, reserved notations) which follow Require

Are you sure?
Printing Width should be whatever locality you give it (Local Global or #[export]), reserved notations are import time AFAIK. eg

Module Foo.
Reserved Notation "x --> y" (at level 55).
Fail Check _ --> _. (* unknow interpretation *)
End Foo.
Check _ --> _. (* syntax error happens before Fail can wrap it *)

[andres-erbsen]

This indeed seems better now. The following works too:

Module Foo.
Reserved Notation "x --> y" (at level 55).
Notation "x --> y" := (x+y) (at level 55).
Check _ --> _. (* unknow interpretation *)
End Foo.
Notation "x --> y" := (x, y) (at level 1).
Unset Printing Notations.
Check fun f:_->nat => f 1 --> 1. (* syntax error happens before Fail can wrap it *)

[SkySkimmer]

I don't get a syntax error on that last one. And AFAICT behaviour hasn't changed since 8.4 (as far back as I have installed).