I try and use hs-to-coq to translate this simple piece of Haskell
module Main (main) where import GHC.Base data ClosedAbove = V | B ClosedAbove ClosedAbove deriving(Eq,Show,Read) data UniquelyClosable = L ClosedAbove | A UniquelyClosable UniquelyClosable deriving(Eq,Show,Read) genA 0 =  genA n | n>0 = [ L x | x <- genB (n-1)] ++ [A x y | k<-[0..n-2], x<-genA k, y<-genA (n-2-k) ] genB 0 = [V] genB n | n>0 = [ B a b | k <- [0..n-2], a <- genB k, b <- genB (n-2-k) ] main = print (genA 4)
However when running
stack exec hs-to-coq -- -o output-directory/ example.hs
I get the following error message :
<command line>: Package environment "-" (specified in GHC_ENVIRONMENT) not found
Any advice ?
$ stack exec hs-to-coq -- -o output-directory/ ex.hs When looking up information about GHC.Classes.Eq in classDefns Could not find GHC/Classes.h2ci in any of these directories: Please either process GHC.Classes first, or skip declarations that mention GHC.Classes. Could not find information for the class `GHC.Classes.Eq' when defining the instance `Main.Eq__MyNat'
When running hs-to-coq, I get this error message and I do not know how to make hs-to-coq aware of the location of GHC/Classes.h2ci.
I use the simpliest example I could invent :
module Main (main) where import GHC.Base data MyNat = MyZero | MySucc MyNat deriving(Eq,Show,Read) main = print (MySucc (MySucc MyZero))
Hi! Take a look at the Makefiles in each of the examples subdirectories, such as https://github.com/plclub/hs-to-coq/blob/master/examples/simple/Makefile. Often you'll need to tell hs-to-coq where to find information about the base libraries.
Last updated: Feb 06 2023 at 05:03 UTC