coqcoqide

Coq: Issue with Require Export

my issue seems to be a common one, but none of the found answers could solve it. I am following the software foundations course on Coq, and so I come to the command:

> From LF Require Export Basics.

Whatever I try, I get always the following answer:

"Cannot find a physical path bound to logical path matching suffix <> and prefix LF."

I compiled Basics.v from coqIde, and the Basics.vo file is created correctly. I also compiled it from the coqc command line, as suggested somewhere My _CoqProject file exists, in the same folder as Basics.v, and states: -Q . LF the _CoqProject parameter is set to "appended to arguments".

when I load Basics.v I see on the bottom of CoqIde "Reading Options from ..._CoqProject" I put the lf folder into a folder which is in the LoadPath of coq.

What else could I check?

My system is Windows 10. I run CoqIde 8.9.1

Thank you!

Solution

  • I usually work under a Linux machine, but here something I did using a virtual machine.

    1. I downloaded the windows installer from https://github.com/coq/coq/releases/tag/V8.9.1
    2. I downladed the lf.tgz file from https://softwarefoundations.cis.upenn.edu/lf-current/index.html
    3. I ran the windows installer for Coq. It placed the coq system in C:\coq
    4. I used cygwin tools to expand the file lf.tgz so that I had a directory C:\Users\user\foundations\lf containing Basics.v, _CoqProject etc.

    Then I used the search command to find coqide as an installed app. I then proceeded with the following steps:

    1. start coqide
    2. open the file Basics.v
    3. use the option Compile->Compile buffer

    I could then observe that the directory C:\Users\user\foundations\lf contained a file named Basics.vo

    1. Then I opened a new buffer, and wrote From LF Require Export Basics. and did not try to execute this line
    2. I saved this buffer in a file in directory C:\Users\user\foundations\lf. Let's assume this file is named toto.v
    3. I closed the toto.v buffer.
    4. I re-opened the toto.v using the option File->Open
    5. I executed the file contents.

    This process is the result of trial-and-error. What I know is that Require Export ... only works if there are ...vo files on you disk, but coqide needs to know where to look for these files. For this it maintains a "load path". When opening a file from a given directory, coqide looks in this directory (and ancestors) to find a _CoqProject file, and the latter may contain directives to modify the load path. It is the case here "-Q . LF" indicates that all .vo files in the current directory should be considered, and that their symbolic name should start with the prefix "LF."

    The problem is that when you start from an empty buffer, no _CoqProject file gets read and coqide does not where to look for your data. This is why I did the steps 5-6-7: when reading the file toto.v, I provoked the reading of the _CoqProject file.

    Takeaway lesson: Make sure the Basics.vo file exists, and then make sure the buffer you are working on was obtained through a reading operation from the same directory. If needed, save, close, and re-open to make sure this is the case.