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

lastland · 2020-11-03T20:04:02Z

Issue by christinaburge
Tuesday Feb 18, 2020 at 14:18 GMT
Originally opened as antalsz/hs-to-coq#144

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! :)

The text was updated successfully, but these errors were encountered:

lastland · 2020-11-03T20:04:03Z

Comment by lastland
Tuesday Feb 18, 2020 at 18:44 GMT

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...

lastland · 2020-11-03T20:04:04Z

Comment by christinaburge
Wednesday Feb 19, 2020 at 09:29 GMT

Thanks for your quick reply! I fixed the second error, it was due to having an outdated version of Coqc.

As for the first error, I'm still confused! My _Coqproject file is attached. I think it all looks fine? Not picking up files in the same directory seems to be a common problem for Coqc, from a quick google!

Interestingly, if I try on the command line:

coqc -Q . "" "base/GHC/Base.v"

I get the error:

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

So then, I try:

coqc -Q src GHC "base/GHC/Base.v"

And I get the error:

Error: Unable to locate library GHC.Prim.

But it is there, in the same directory! All very mysterious.

Cheers,

Christina

From: Li Yao [email protected]
Sent: 18 February 2020 18:44
To: antalsz/hs-to-coq [email protected]
Cc: Christina Burge [email protected]; Author [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

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...

—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHubantalsz/hs-to-coq#144, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AJ6CBGMDI2LTTMXVXWRWM6LRDQUBTANCNFSM4KXFN76A.

IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

-Q . ""
GHC/Wf.v GHC/Skip.v GHC/DeferredFix.v GHC/DeferredFixImpl.v GHC/Num.v GHC/Char.v GHC/Real.v GHC/Enum.v Data/Bits.v GHC/Prim.v GHC/Types.v GHC/Tuple.v Data/Type/Equality.v GHC/Err.v GHC/Nat.v GHC/Unicode.v Prelude.v GHC/Base.v Data/Maybe.v GHC/List.v Data/List.v Data/OldList.v Data/Bool.v Data/Tuple.v Data/Void.v Data/Function.v Data/Ord.v Data/Functor.v Data/Either.v Data/Proxy.v Control/Monad.v Data/Monoid.v Data/Functor/Utils.v Data/Traversable.v Control/Monad/Fail.v Data/Foldable.v Control/Arrow.v Data/Functor/Identity.v Data/Functor/Const.v Control/Applicative.v Data/Functor/Classes.v Control/Category.v Data/Bifunctor.v Data/List/NonEmpty.v Data/Semigroup.v Data/Functor/Compose.v Data/Functor/Product.v Data/Functor/Sum.v Data/Bifoldable.v Data/Bitraversable.v Control/Monad/Zip.v Data/SemigroupInternal.v

lastland · 2020-11-03T20:04:06Z

Comment by christinaburge
Wednesday Feb 19, 2020 at 10:01 GMT

Aha! If I manually compile everything in the base/GHC directory, using (e.g):

coqc -Q . GHC Base.v

Then I can return to the top level and do make -C base successfully.

I now have a new error, when I do make -C base-thy:

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.

I'm sure I'll get to the bottom of it eventually!

From: Christina Burge [email protected]
Sent: 19 February 2020 09:29
To: antalsz/hs-to-coq [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

Thanks for your quick reply! I fixed the second error, it was due to having an outdated version of Coqc.

As for the first error, I'm still confused! My _Coqproject file is attached. I think it all looks fine? Not picking up files in the same directory seems to be a common problem for Coqc, from a quick google!

Interestingly, if I try on the command line:

coqc -Q . "" "base/GHC/Base.v"

I get the error:

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

So then, I try:

coqc -Q src GHC "base/GHC/Base.v"

And I get the error:

Error: Unable to locate library GHC.Prim.

But it is there, in the same directory! All very mysterious.

Cheers,

Christina

From: Li Yao [email protected]
Sent: 18 February 2020 18:44
To: antalsz/hs-to-coq [email protected]
Cc: Christina Burge [email protected]; Author [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

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...

—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHubantalsz/hs-to-coq#144, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AJ6CBGMDI2LTTMXVXWRWM6LRDQUBTANCNFSM4KXFN76A.

IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

lastland · 2020-11-03T20:04:07Z

Comment by christinaburge
Wednesday Feb 19, 2020 at 10:10 GMT

I should add, this is all on my linux machine, I'm currently revisiting the Mac version to see if I get any further there.

From: Christina Burge [email protected]
Sent: 19 February 2020 10:00
To: antalsz/hs-to-coq [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

Aha! If I manually compile everything in the base/GHC directory, using (e.g):

coqc -Q . GHC Base.v

Then I can return to the top level and do make -C base successfully.

I now have a new error, when I do make -C base-thy:

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.

I'm sure I'll get to the bottom of it eventually!

From: Christina Burge [email protected]
Sent: 19 February 2020 09:29
To: antalsz/hs-to-coq [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

Thanks for your quick reply! I fixed the second error, it was due to having an outdated version of Coqc.

As for the first error, I'm still confused! My _Coqproject file is attached. I think it all looks fine? Not picking up files in the same directory seems to be a common problem for Coqc, from a quick google!

Interestingly, if I try on the command line:

coqc -Q . "" "base/GHC/Base.v"

I get the error:

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

So then, I try:

coqc -Q src GHC "base/GHC/Base.v"

And I get the error:

Error: Unable to locate library GHC.Prim.

But it is there, in the same directory! All very mysterious.

Cheers,

Christina

From: Li Yao [email protected]
Sent: 18 February 2020 18:44
To: antalsz/hs-to-coq [email protected]
Cc: Christina Burge [email protected]; Author [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

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...

—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHubantalsz/hs-to-coq#144, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AJ6CBGMDI2LTTMXVXWRWM6LRDQUBTANCNFSM4KXFN76A.

IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

lastland · 2020-11-03T20:04:08Z

Comment by christinaburge
Wednesday Feb 19, 2020 at 11:57 GMT

Same error on Mac.

From: Christina Burge [email protected]
Sent: 19 February 2020 10:09
To: antalsz/hs-to-coq [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

I should add, this is all on my linux machine, I'm currently revisiting the Mac version to see if I get any further there.

From: Christina Burge [email protected]
Sent: 19 February 2020 10:00
To: antalsz/hs-to-coq [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

Aha! If I manually compile everything in the base/GHC directory, using (e.g):

coqc -Q . GHC Base.v

Then I can return to the top level and do make -C base successfully.

I now have a new error, when I do make -C base-thy:

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.

I'm sure I'll get to the bottom of it eventually!

From: Christina Burge [email protected]
Sent: 19 February 2020 09:29
To: antalsz/hs-to-coq [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

Thanks for your quick reply! I fixed the second error, it was due to having an outdated version of Coqc.

As for the first error, I'm still confused! My _Coqproject file is attached. I think it all looks fine? Not picking up files in the same directory seems to be a common problem for Coqc, from a quick google!

Interestingly, if I try on the command line:

coqc -Q . "" "base/GHC/Base.v"

I get the error:

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

So then, I try:

coqc -Q src GHC "base/GHC/Base.v"

And I get the error:

Error: Unable to locate library GHC.Prim.

But it is there, in the same directory! All very mysterious.

Cheers,

Christina

From: Li Yao [email protected]
Sent: 18 February 2020 18:44
To: antalsz/hs-to-coq [email protected]
Cc: Christina Burge [email protected]; Author [email protected]
Subject: Re: [antalsz/hs-to-coq] Cannot find a physical path bound to logical path matching suffix GHC. (#144)

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...

—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHubantalsz/hs-to-coq#144, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AJ6CBGMDI2LTTMXVXWRWM6LRDQUBTANCNFSM4KXFN76A.

IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

lastland · 2020-11-03T20:04:09Z

Comment by sweirich
Wednesday Feb 19, 2020 at 13:09 GMT

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 · 2020-11-03T20:04:10Z

Comment by lastland
Wednesday Feb 19, 2020 at 17:11 GMT

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.

lastland · 2020-11-03T20:04:11Z

Comment by christinaburge
Tuesday Feb 25, 2020 at 14:24 GMT

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 · 2020-11-03T20:04:12Z

Comment by lastland
Tuesday Feb 25, 2020 at 20:16 GMT

@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 · 2020-11-03T20:04:13Z

Comment by lastland
Wednesday Feb 26, 2020 at 02:18 GMT

@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 · 2020-11-03T20:04:14Z

Comment by lastland
Wednesday Feb 26, 2020 at 21:34 GMT

@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).

lastland · 2020-11-03T20:04:15Z

Comment by christinaburge
Thursday Feb 27, 2020 at 11:56 GMT

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.

lastland · 2020-11-03T20:04:16Z

Comment by sweirich
Thursday Feb 27, 2020 at 13:15 GMT

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.

lastland · 2020-11-03T20:04:17Z

Comment by christinaburge
Thursday Feb 27, 2020 at 14:09 GMT

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 · 2020-11-03T20:04:18Z

Comment by lastland
Thursday Feb 27, 2020 at 14:25 GMT

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.

lastland · 2020-11-03T20:04:19Z

Comment by christinaburge
Thursday Feb 27, 2020 at 16:21 GMT

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!

lastland · 2020-11-03T20:04:20Z

Comment by christinaburge
Friday Feb 28, 2020 at 11:57 GMT

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?

lastland · 2020-11-03T20:04:21Z

Comment by christinaburge
Friday Feb 28, 2020 at 17:08 GMT

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 · 2020-11-03T20:04:22Z

Comment by lastland
Friday Feb 28, 2020 at 19:55 GMT

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 · 2020-11-03T20:04:23Z

Comment by lastland
Tuesday Mar 03, 2020 at 19:43 GMT

Hi,

I think this time the problem happens on the Haskell side: a Haskell module with called ‘Main’ must have a function called ‘main’, and the type of the function must be 'IO a’ for some type ‘a’. My conjecture is that your Transp.hs file has a ‘module Main where’ at top, which causes this issue. A simple fix is to change the module name to something else (e.g., Transp).

Hs-to-coq relies on ghc to do some pre-processing on Haskell files, so you must be able to compile all your files with ghc before translating them.

PS: If you don’t mind sharing with us what you are exploring with hs-to-coq and your work-in-progress source code, we may be able to help you in more detail.

Best,
Yao

On Mar 2, 2020, at 5:52 AM, christinaburge [email protected] wrote:

Ah, I see. Does this mean that for the moment hs-to-coq does not handle anything that involves operations on lists as I cannot import Data.List?

I am trying to translate the code:

`import Data.List

transp :: Num a => [[a]] -> [[a]]
transp ([]:_) = []
transp a = (map head a) : transp (map tail a)`

And I get the error:

Transp.hs:1:1: error: The IO action ‘main’ is not defined in module ‘Main’

When I try to translate using the command:

stack exec -- hs-to-coq -e /Users/chrbur02/Coq/hs-to-coq/base/edits Transp.hs --iface-dir /Users/chrbur02/Coq/hs-to-coq/base -o .

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub antalsz/hs-to-coq#144, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAGPFJSLXCWQISHVJ4MJIRDRFOFXHANCNFSM4KXFN76A.

lastland · 2020-12-21T21:41:01Z

I'm closing this issue since there's no more update since March 2020.

lastland closed this as completed Dec 21, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Dec 21, 2020

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

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

Comments

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Nov 3, 2020

lastland commented Dec 21, 2020