coqIDE is not properly connecting files in project and is not compiling

Question

I'm new to using coq/coqIDE and I'm not computer savvy either so I don't know whats wrong or what to call the issue. I was trying to go through the Software Foundations book, but coqIDE isn't working right. I'm using the latest windows 10, and coqIDE 8.10.2

The first issue is when I go to the tab compile -> compile buffer in Basics.v, coqIDE doesn't create a .vo file or a .glob. None of the other buttons worked either. Running coqIDE as admin didn't make it work either, but I figured out I can get around this by manually dragging Basics.v into the coqc application file.

I had no issues with coq working during the first lesson, but in the next lesson we're meant to import the definitions from Basics.v into Induction.v, when I run what they say

From LF Require Export Basics.

I get the error The file C:\Users\...\Coq Files\Tutorial\lf\Basics.vo contains library Basics and not library LF.Basics even though the _CoqProject file contains "-Q . LF" as it should.

I can get around this error too by just writing "Require Export Basics." which properly loads, up until I actually try calling a definition from Basics

Running

Require Export Basics.
Example example: evenb 2 = true.

works until I get to evenb, and then gives the error The reference evenb was not found in the current environment. even though it's in Basics.v

If I get even more anal and try

Add LoadPath "C:\Users\...\Coq Files\Tutorial\lf".
From LF Require Export Basics.

I get the error

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

And then finally if I try

Add LoadPath "C:\Users\...\Coq Files\Tutorial\lf".
Require Export Basics.
Example example: evenb 2 = true.

Loads properly.

So I'm wondering how should I fix the load path so that the project works without putting that junk in every file and how do I make the compile tab work.

There were some people talking about "hitting make in the top-level" but I have no idea what that means. I tried it anyway and ran the Makefile as a .bat even though I already downloaded it properly so there shouldn't be any need, but the Makefile didn't change anything anyway.

I don't think I'm forgetting anything, thanks in advance.

Donald Sebastian Leung Donald Sebastian Leung · Accepted Answer · 2020-01-20T07:06:59

Instead of choosing Compile > Compile buffer, try Compile > Make instead (when browsing any one of the vernacular files in Logical Foundations) - I think that is what others meant by "hitting make in the top-level". But first, you may want to remove the workarounds you added in e.g. Induction.v, and save a trivial change in Basics.v such as adding/removing a newline somewhere in order to convince make to recompile it.

coqIDE is not properly connecting files in project and is not compiling

1 Answers