Stream: hs-to-coq devs & users

Topic: Maybe.v file

Julin S (Sep 11 2022 at 17:58):

Hi. I was trying the hs-to-coq tutorial in here and got a coq file which has this line in it:

Require GHC.Maybe.

But base/GHC doesn't have a Maybe.v file.

So when I try to compile, it complains saying that it can't find a file named Maybe.

How can this be fixed?

I'm using coq v8.13. Should I go with an earlier version?

Julin S (Sep 11 2022 at 18:00):

But the Queue.v file in the repo in here doesn't have that GHC.Maybe.

Julin S (Sep 11 2022 at 18:02):

A simple queue type in haskell is what is being translated to coq.

The pop function in the repo directly uses Coq's option (eg: None).

But the one I got uses values like GHC.Maybe.Nothing.

Julin S (Sep 11 2022 at 18:03):

The pop function I got is:

Definition pop {a : Type} : Queue a -> GHC.Maybe.Maybe (a * Queue a)%type :=
  fun arg_0__ =>
    match arg_0__ with
    | MkQueue (cons elem front') back =>
        GHC.Maybe.Just (pair elem (MkQueue front' back))
    | MkQueue nil back =>
        match GHC.List.reverse back with
        | nil => GHC.Maybe.Nothing
        | cons elem back' => GHC.Maybe.Just (pair elem (MkQueue back' nil))
        end
    end.

Julin S (Sep 11 2022 at 20:51):

I had tried building hs-to-coq with nix.

nix-build -A haskellPackages.hs-to-coq

Li-yao (Sep 12 2022 at 09:27):

What version of GHC do you have? IIRC it only works out-of-the-box with GHC 8.4. For other versions, you can try fixing the edits file to rename GHC.Maybe and other new modules to old ones, but you may also have to just re-translate base.

Li-yao (Sep 12 2022 at 09:29):

For example in hs-to-coq/base/edits there is rename type GHC.Base.Maybe = option, so that breaks when Maybe is moved to GHC.Maybe.

Julin S (Sep 12 2022 at 10:04):

I'm on ghc v9.0.2.

Julin S (Sep 12 2022 at 10:05):

(On another copy of the hs-to-coq repo, while compiling base and base-thy, I tried replacing omega with lia but couldn't go much further than that.)

Julin S (Sep 12 2022 at 10:05):

Maybe I'll try the older coq haskell.

Li-yao (Sep 12 2022 at 10:18):

Yeah, try extending the tutorial's edits to get something compatible with the existing base, you may have some luck, but if not, switching to an older GHC seems like the next simplest solution.

Last updated: Feb 06 2023 at 06:29 UTC