search

siegebell / vscoq

Coq Support for Visual Studio Code
MIT License
92 stars 9 forks source link

OSX LoadPath inconsistencies #137

Open natelaunchbury opened 7 years ago

natelaunchbury commented 7 years ago

There appears to be some inconsistencies in the LoadPath when running vscoq versus coqtop from the terminal. This is preventing me from being able to load Coq files despite the correct .vo files being in the directory.

From _CoqProject: 

-Q src ""

When I load the Coq file in vscoq it is able to execute coqtop 

exec: coqtop -main-channel 127.0.0.1:55483:55484 -control-channel 127.0.0.1:55485:55486 -ideslave -async-proofs on -Q src ""
coqtop started with pid 7310

But I get the error message: 

message: Error: Cannot find library Coqlib in loadpath

Inserting a Print LoadPath at the top of the file yields: 

Logical Path:                 Physical path:
""                            /Users/nate/Desktop/Galois/cryptol-semantics/src

I am able to Require Import Coqlib manually using coqtop from the terminal but running Print Loadpath there instead yields: 

Logical Path:                 Physical path:
<>                            /Users/nate/Desktop/Galois/cryptol-semantics/src
natelaunchbury commented 7 years ago

Adding Add LoadPath "<src dir>". to the top of the Coq files is a temporary fix for this issue