Skip to content
This repository has been archived by the owner on Nov 17, 2020. It is now read-only.

Cannot find a physical path bound to logical path matching suffix GHC. #144

Open
christinaburge opened this issue Feb 18, 2020 · 20 comments
Open

Cannot find a physical path bound to logical path matching suffix GHC. #144

christinaburge opened this issue Feb 18, 2020 · 20 comments

Comments

@christinaburge
Copy link

I get the error:

Cannot find a physical path bound to logical path matching suffix GHC.

This error occurs when attempting to verify the following line of code in the coq IDE on macOS:

Require GHC.Base.

Similarly, when I try to install hs-to-coq on my linux box, when I run make -C base I get the error:

coqc: --print-version: no such file or directory
COQC GHC/Base.v
coqc: -Q: no such file or directory
Makefile:656: recipe for target 'GHC/Base.vo' failed

It seems like a file (and therefore a step in your instructions) is missing. Thanks for taking a look! :)
@lastland
Copy link
Collaborator

It seems that the first problem was caused by either not having GHC.Base compiled, or not putting the directory containing GHC.Base in your _CoqProject or Makefile. Would you mind sharing more information about what you did before getting this error information (and probably with your _CoqProject file?)

I'm not sure what caused the second problem though. The error message seems to suggest that your coqc does not take arguments (it mistook --print-version and -Q as file names), but I don't know why this would happen...

@christinaburge
Copy link
Author

christinaburge commented Feb 19, 2020 via email

@christinaburge
Copy link
Author

christinaburge commented Feb 19, 2020 via email

@christinaburge
Copy link
Author

christinaburge commented Feb 19, 2020 via email

@christinaburge
Copy link
Author

christinaburge commented Feb 19, 2020 via email

@sweirich
Copy link
Collaborator

Thanks for the reports. Can you make a listing of all of the commands that you are running and their output so that we can figure out the issue?

@lastland
Copy link
Collaborator

File "./Data/Bits/Popcount.v", line 20, characters 33-41:

Error: The reference Is_power was not found in the current environment.

Is_power should come from a Coq's standard library, namely, Coq.ZArith.Zlogarithm. I don't know why coqc would fail to find that... Which Coq version are you using? (You can check that via coqc -v.) And like @sweirich said, a listing of all of the commands that you are running and their output would be helpful for us to understand what happened.

@christinaburge
Copy link
Author

I sent this via email but I just realised it never showed up here for some reason!

I'm following the instructions at https://hs-to-coq.readthedocs.io/en/latest/installation.html. Everything works fine (now that I manually complied the files in the base/GHC directory, using (e.g): coqc -Q . GHC Base.v)

Then I run:

make -C base
make: Entering directory '/home/chrbur02/Coq/hs-to-coq/base'
coq_makefile -f _CoqProject -o Makefile
Warning: No file should be installed at the root of Coq's library.
Warning: No logical path (-R, -Q) applies to these files:
Warning:  Prelude.v

COQC Prelude.v
COQC Data/OldList.v
COQC Control/Applicative.v
COQC Data/List/NonEmpty.v
COQC Data/Semigroup.v
COQC Control/Monad/Zip.v
COQC Data/Functor/Product.v
make: Leaving directory '/home/chrbur02/Coq/hs-to-coq/base'


make -C base-thy
make: Entering directory '/home/chrbur02/Coq/hs-to-coq/base-thy'
W: This Makefile was generated by Coq 8.8.1
W: while the current Coq version is 8.11.0
COQC GHC/Base.v
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
File "./GHC/Base.v", line 411, characters 7-29:
Warning: Nothing to inject.
COQC Data/Either.v
File "./Data/Either.v", line 5, characters 0-31:
Warning: Trying to mask the absolute name "GHC.Base"!
[masking-absolute-name,deprecated]
COQC GHC/List.v
File "./GHC/List.v", line 8, characters 0-31:
Warning: Trying to mask the absolute name "GHC.Base"!
[masking-absolute-name,deprecated]
COQC Data/Foldable.v
File "./Data/Foldable.v", line 4, characters 0-31:
Warning: Trying to mask the absolute name "GHC.Base"!
[masking-absolute-name,deprecated]
File "./Data/Foldable.v", line 5, characters 0-31:
Warning: Trying to mask the absolute name "GHC.List"!
[masking-absolute-name,deprecated]
COQC Data/Traversable.v
File "./Data/Traversable.v", line 4, characters 0-31:
Warning: Trying to mask the absolute name "GHC.Base"!
[masking-absolute-name,deprecated]
File "./Data/Traversable.v", line 5, characters 0-31:
Warning: Trying to mask the absolute name "GHC.List"!
[masking-absolute-name,deprecated]
COQC Data/Functor/Classes.v
File "./Data/Functor/Classes.v", line 4, characters 0-31:
Warning: Trying to mask the absolute name "GHC.Base"!
[masking-absolute-name,deprecated]
COQC Data/OldList.v
COQC Data/Ord.v
File "./Data/Ord.v", line 2, characters 0-31:
Warning: Trying to mask the absolute name "GHC.Base"!
[masking-absolute-name,deprecated]
COQC Data/Proxy.v
File "./Data/Proxy.v", line 2, characters 0-31:
Warning: Trying to mask the absolute name "GHC.Base"!
[masking-absolute-name,deprecated]
COQC Termination.v
File "./Termination.v", line 4, characters 0-31:
Warning: Trying to mask the absolute name "GHC.Base"!
[masking-absolute-name,deprecated]
COQC Data/Bits/Popcount.v
File "./Data/Bits/Popcount.v", line 20, characters 33-41:
Error: The reference Is_power was not found in the current environment.

Makefile:656: recipe for target 'Data/Bits/Popcount.vo' failed
make[1]: *** [Data/Bits/Popcount.vo] Error 1
Makefile:317: recipe for target 'all' failed
make: *** [all] Error 2
make: Leaving directory '/home/chrbur02/Coq/hs-to-coq/base-thy'

I have
The Glorious Glasgow Haskell Compilation System, version 8.6.5
The Coq Proof Assistant, version 8.11.0 (February 2020)
compiled on Feb 18 2020 22:17:58 with OCaml 4.09.0

@lastland
Copy link
Collaborator

@christinaburge Hi, the issue seems to arise from a different version of Coq. Currently, hs-to-coq only supports Coq 8.10, and Is_power comes from the Coq.ZArith.Zlogarithm library which was removed since Coq 8.11. To work with the current version hs-to-coq, you can either downgrade your Coq version (recommended) or change the source code in base-thy to use a different function---but I don't know if this would be the only compatibility issue.

@lastland
Copy link
Collaborator

@christinaburge If you want to keep using Coq 8.11, I have created a branch called coq-8.11 that fixes some compatibility issues. Although I have not managed to fix everything, you should be able to use it if what you want to do does not rely on our proofs for containers or ghc.

@lastland
Copy link
Collaborator

@christinaburge Hi, I have just updated the coq-8.11 branch. Now you can work with hs-to-coq and Coq 8.11 (and with our proofs for containers and ghc).

@christinaburge
Copy link
Author

Thanks for all your help! I'm now using coq-8.10, and everything now compiles, but I get errors with the line Require GHC.Base in my generated code.

If I use the Coq IDE, I get:

Compiled library GHC.Base (in file /Users/chrbur02/Coq/hs-to-coq/base/GHC/Base.vo) makes inconsistent assumptions over library Coq.Init.Logic

If I use coqtop -l <file.v>, I get:

Error: Cannot find a physical path bound to logical path matching suffix GHC.

@sweirich
Copy link
Collaborator

If I use the Coq IDE, I get:

Compiled library GHC.Base (in file /Users/chrbur02/Coq/hs-to-coq/base/GHC/Base.vo) makes inconsistent assumptions over library Coq.Init.Logic

Sometimes this happens if your coqide uses a different version of Coq than the one you used to compile the base libraries.

If I use coqtop -l <file.v>, I get:

Error: Cannot find a physical path bound to logical path matching suffix GHC.

You’ll need to supply the command line arguments, such as -Q and -R so that coqtop knows where to find the libraries. The easiest way to do so is to create a _CoqProject file in the same directory as your code. For example, you can take a look at our _CoqProject file for our bag example: https://github.com/antalsz/hs-to-coq/blob/master/examples/bag/_CoqProject.

@christinaburge
Copy link
Author

christinaburge commented Feb 27, 2020 •
edited
Loading

Thanks for that! As an experiment, I tried running:

coqtop -l Bag.v in the examples/bag directory, and I get the same error:

File "/Users/chrbur02/Coq/hs-to-coq/examples/bag/Bag.v", line 12, characters 15-23: Error: Cannot find a physical path bound to logical path matching suffix GHC.

Clearly I'm missing a step!

I wonder if the warning I got when I did make -C base is relevant?

Warning: No file should be installed at the root of Coq's library.
Warning: No logical path (-R, -Q) applies to these files:
Warning:  Prelude.v

@lastland
Copy link
Collaborator

lastland commented Feb 27, 2020 •
edited
Loading

Hi, the reason that Coq cannot find a "logical path matching suffix GHC" is that it relies on base library and you have not compiled it (because you ran into an error earlier, which failed the compilation). You will have to fix the issue with base first.

To fix base, I think you will need a make clean before compilation. I think you have this problem because you still have the remnant of previous compilation using Coq 8.11, and a make clean would fix that.

@christinaburge
Copy link
Author

output.txt

I've tried that, and it doesn't work, unfortunately! I've got the entire output of both make -C base and make -C base-thy here, in case you can spot the problem!

@christinaburge
Copy link
Author

Oh, I've tried adding

Add LoadPath "<filepath>/hs-to-coq/base". to the file I'm trying to load using coqtop -l <file.v>.

This gets rid of the error Error: Cannot find a physical path bound to logical path matching suffix GHC.

Perhaps this should be autogenerated along with the rest of the .v file?

@christinaburge
Copy link
Author

I now get the error: Error: Cannot find a physical path bound to logical path matching suffix System., which is related to this line:

Require System.IO.

I'm not sure what I need to have installed to make this work!

@lastland
Copy link
Collaborator

Hi, I think in both cases, the problem is that Coq does not find the corresponding Coq libraries translated from Haskell. Our general solution is specifying that in _CoqProject, rather than adding load-path to each individual file. For the bag example, if you run make instead of using coqtop or coqc directly, the code should compile. If make does not work for the same dependency error, it usually means there is something wrong with the _CoqProject file, or the libraries it depends on.

The second issue you raised should be caused by similar problems, but I cannot be sure why this happened without much information. Are you trying to translate a code of your own? If that's the case, you may want to skip the parts relevant to System.IO, as hs-to-coq does not translate IO functions at the moment. You will need to do that using edits: https://hs-to-coq.readthedocs.io/en/latest/edits.html#

@lastland
Copy link
Collaborator

lastland commented Mar 3, 2020 via email

@lastland lastland mentioned this issue Nov 3, 2020
Closed
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@lastland @sweirich @christinaburge