search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

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

Open christinaburge opened 4 years ago

christinaburge commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 notifications@github.com Sent: 18 February 2020 18:44 To: antalsz/hs-to-coq hs-to-coq@noreply.github.com Cc: Christina Burge Christina.Burge@arm.com; Author author@noreply.github.com 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 GitHubhttps://github.com/antalsz/hs-to-coq/issues/144?email_source=notifications&email_token=AJ6CBGJDOS2NOPAMVQARLOTRDQUBTA5CNFSM4KXFN76KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMDLDSQ#issuecomment-587641290, 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

christinaburge commented 4 years ago

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 Christina.Burge@arm.com Sent: 19 February 2020 09:29 To: antalsz/hs-to-coq reply@reply.github.com 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 notifications@github.com Sent: 18 February 2020 18:44 To: antalsz/hs-to-coq hs-to-coq@noreply.github.com Cc: Christina Burge Christina.Burge@arm.com; Author author@noreply.github.com 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 GitHubhttps://github.com/antalsz/hs-to-coq/issues/144?email_source=notifications&email_token=AJ6CBGJDOS2NOPAMVQARLOTRDQUBTA5CNFSM4KXFN76KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMDLDSQ#issuecomment-587641290, 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.

christinaburge commented 4 years ago

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 Christina.Burge@arm.com Sent: 19 February 2020 10:00 To: antalsz/hs-to-coq reply@reply.github.com 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 Christina.Burge@arm.com Sent: 19 February 2020 09:29 To: antalsz/hs-to-coq reply@reply.github.com 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 notifications@github.com Sent: 18 February 2020 18:44 To: antalsz/hs-to-coq hs-to-coq@noreply.github.com Cc: Christina Burge Christina.Burge@arm.com; Author author@noreply.github.com 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 GitHubhttps://github.com/antalsz/hs-to-coq/issues/144?email_source=notifications&email_token=AJ6CBGJDOS2NOPAMVQARLOTRDQUBTA5CNFSM4KXFN76KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMDLDSQ#issuecomment-587641290, 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.

christinaburge commented 4 years ago

Same error on Mac.

From: Christina Burge Christina.Burge@arm.com Sent: 19 February 2020 10:09 To: antalsz/hs-to-coq reply@reply.github.com 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 Christina.Burge@arm.com Sent: 19 February 2020 10:00 To: antalsz/hs-to-coq reply@reply.github.com 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 Christina.Burge@arm.com Sent: 19 February 2020 09:29 To: antalsz/hs-to-coq reply@reply.github.com 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 notifications@github.com Sent: 18 February 2020 18:44 To: antalsz/hs-to-coq hs-to-coq@noreply.github.com Cc: Christina Burge Christina.Burge@arm.com; Author author@noreply.github.com 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 GitHubhttps://github.com/antalsz/hs-to-coq/issues/144?email_source=notifications&email_token=AJ6CBGJDOS2NOPAMVQARLOTRDQUBTA5CNFSM4KXFN76KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMDLDSQ#issuecomment-587641290, 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.

sweirich commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

@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 commented 4 years ago

@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 commented 4 years ago

@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 commented 4 years ago

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 commented 4 years ago

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 , 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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 notifications@github.com 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 https://github.com/antalsz/hs-to-coq/issues/144?email_source=notifications&email_token=AAGPFJX33AK6S6ML3CXQVY3RFOFXHA5CNFSM4KXFN76KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOENO3DIQ#issuecomment-593342882, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAGPFJSLXCWQISHVJ4MJIRDRFOFXHANCNFSM4KXFN76A.