Stream: hs-to-coq devs & users

Topic: error message when using hs-to-coq


view this post on Zulip Nicolas Magaud (Sep 27 2022 at 20:12):

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 ?

view this post on Zulip Nicolas Magaud (Dec 01 2022 at 14:56):

$ 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))

view this post on Zulip Stephanie Weirich (Dec 02 2022 at 15:21):

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