proper usage of `--import-dir`, or; how to use `hs-to-coq` on codebases with imports

[quinn-dougherty]

Hello!

I have a minimal example here. the hs-to-coq executable was created with stack install, but there is some nix in here

• ls/tree

$ ls 
edits Main.hs hs-to-coq/ shell.nix

• Main.hs

module Main where

import Control.Lens

data Datum = Datum { aString :: String, anInt :: Int } deriving Show

foo :: String -> Maybe String
foo "barski" = Just "barski"
foo _ = Nothing

someLens :: Datum -> Maybe Datum
someLens = lens aString (\datum string -> datum {aString = string}) foo

main :: IO ()
main = do
  let d = Datum "barski" 1
      e = Datum "bazzzz" 1
      d' = someLens d
      e' = someLens e
  print d'
  print e'

• shell.nix

{ pkgs ? import <nixpkgs> {}
, ghcVersion ? "ghc884"  # matches hs-to-coq/default.nix
}:
let
  hsenv = pkgs.haskell.packages.${ghcVersion}.ghcWithPackages (self: [
    self.lens
  ]);
  scratchDev = pkgs.stdenv.mkDerivation {
    name = "scratch-lens";
    src = ./.;
    buildInputs = [ hsenv ];
    buildPhase = ''
      ghc --version
      ghc-pkg list
    '';
    installPhase = "mkdir -p $out";
  };
in
pkgs.mkShell {
  # buildInputs is for dependencies you'd need "at run time",
  # were you to to use nix-build not nix-shell and build whatever you were working on
  buildInputs = [ scratchDev hsenv ];
}

Notice that lens appears in hs-to-coq.cabal.

• edits

rename value Datum.Datum = Datum.MkDatum

And when we run we fail

$ hs-to-coq --permissive -e hs-to-coq/base/edits --iface-dir hs-to-coq/base -e edits Main.hs -o .
Main.hs:3:1: error:
    Could not find module ‘Control.Lens’
    Use -v to see a list of the files searched for.
  |
3 | import Control.Lens
  | ^^^^^^^^^^^^^^^^^^^

Perhaps this is what --import-dir is for?

• where are my libraries for this version of ghc?

nix-shell
which ghc
# /nix/store/b33hk9dshra06v2z140zf0nr8gw9hk3h-ghc-8.8.4-with-packages/bin/ghc
ls /nix/store/b33hk9dshra06v2z140zf0nr8gw9hk3h-ghc-8.8.4-with-packages/lib/ghc-8.8.4/x86_64-linux-ghc-8.8.4/
# .... lens-4.19.2-DKB7mu1opy3FSq86GPdtGR ...

ok, lens is in that directory. So if we run...

hs-to-coq --permissive -e hs-to-coq/base/edits --iface-dir hs-to-coq/base --import-dir //nix/store/b33hk9dshra06v2z140zf0nr8gw9hk3h-ghc-8.8.4-with-packages/lib/ghc-8.8.4/x86_64-linux-ghc-8.8.4/ -e edits Main.hs -o .

...well, we get the same error.

Let's add

axiomatize module Control.Lens

to edits.

Same error.

It seems to me like there's a version of ghc running inside the executable. Is this basically correct? If so, it would make sense that another version of ghc wouldn't be able to make this work.

It'd be great to have isolation and not have to install packages to some global ghc that the hs-to-coq executable calls upon. Moreover, it'd be great to have observability into what packages are reachable by the ghc that the hs-to-coq executable calls upon.

[quinn-dougherty]

I briefly considered wiggling the hs-to-coq.cabal file thinking that would be the best way to effect the packages reachable by the version of ghc that lives inside the hs-to-coq executable, but realized that lens is the particular case that isn't working right now and lens is already in hs-to-coq.cabal.

[nomeata]

hs-to-coq is essentially a wrapper around ghc (included as a library), so ghc-specific paths are needed to make it aware of other packages, so you are correct in that.

Does running hs-to-coq inside stack exec help, so that the package environment created by stack is available?

Although for containers what we do is to pass to hs-to-coq flags to find the files directly, i.e. point it to a checked-out version of the library

	       --ghc -icontainers \
	       --ghc -icontainers/dist-install/build \
	       -Icontainers/include \

Maybe it’s more reliable this way than hoping ghc finds the package somehow.

[quinn-dougherty]

Thanks. Having trouble getting stack exec hs-to-coq to work (it put the executable in ~/.local/bin). I've also played with the --ghc flag with no luck.

$ stack exec hs-to-coq --help
<command line>: Package environment "-" (specified in GHC_ENVIRONMENT) not found```

I'm working on a new project flow, I want people to be able to clone down my template and clone their project as a subdirectory of my template (or even as a git submodule) then add an edits file then run make all then hop into theories and start proving specs. It's all nixified (and make calls nix-build and nix-shell currently so you can do the whole thing in make all). At this point, over in there, hs-to-coq runs perfectly fine on files with import Data.ByteString (with or without axiomatize module Data.ByteString in edits) and it's not until coqc sees Require Data.ByteString. that there's an error. Intuitively this makes sense: Data.ByteString isn't in hs-to-coq/base, but I would have hoped that axiomatize module Data.ByteString gives me a for-free workaround.

[nomeata]

I want people to be able to clone down my template and clone their project as a subdirectory of my template

Laudable! :-)

At this point, over in there, hs-to-coq runs perfectly fine on files with import Data.ByteString (with or without axiomatize module Data.ByteString in edits) and it's not until coqc sees Require Data.ByteString. that there's an error.

Ok, then you have successfully dealt with GHC packages etc, and “just” need Coq to find the right files, juggling -Q and -P parameters. Which error message precisely do you get?

axiomatize module Data.ByteString gives me a for-free workaround.

That creates axioms for all the definitoins, but you still need to process the file to get the definitoins, and downstream users will import (in Coq) the module as usual.

The only way I know to not depend on a module at all is to edit out all the uses of it. You can use the skip edit in a downstream module to skip the import, but then the resulting module will simply fail to build, because the occurrences of names from that module are still there. (The skip edit is not very useful, it’s mainly a safeguard and a way to say “fail loudly if X is still used”.)

[quinn-dougherty]

This is the precise error message re Require Data.ByteString

nix-shell --run "coqc -R result/hs-to-coq/base \"\" -Q src-coq Src src-coq/Types.v"
File "./src-coq/Types.v", line 15, characters 8-23:
Error: Unable to locate library Data.ByteString.

make: *** [Makefile:33: coqc-the-output] Error 1

Are you suggesting that I clone Data.ByteString source and run hs-to-coq on it so I can point to it with a coqc -R flag? It's a drastic move but it's my only idea.

coqc --help does not seem to reveal -P, but perhaps you meant -R (which I do understand)

[Lysxia]

That does seem like the right solution. You need a file Data/ByteString.v somehow, and running hs-to-coq on Data/ByteString.hs (with axiomatize module) is the easiest way, or you stub it manually.

[sweirich]

Another option is to axiomatize your Bytestring library by hand. This is useful if the library is large and complicated and includes features that hs-to-coq can't handle, even in axiomatization mode.

The wc example does this, and includes rename directives in the edit file to use this simplified version. While we could have axiomatized the Bytestring module, we had to do this for our model of the IO monad.

[quinn-dougherty]

I've been wrapping my head around the wc example, looks like it has the components I need, thanks!

That does seem like the right solution. You need a file Data/ByteString.v somehow, and running hs-to-coq on Data/ByteString.hs (with axiomatize module) is the easiest way, or you stub it manually.

I'm confused. If I have a Data/ByteString.hs, isn't running hs-to-coq on it a replacement for axiomatize module? in other words, doesn't having a .v file by running hs-to-coq make axiomatize module sort of obsolete (in the context of that particular need)? Is it because axiomatize module is used so as to not descend into the entire library and only convert one .hs file namely Data/ByteString.hs to .v, so the edits file would have to axiomatize module the deeper parts of the library while hs-to-coqing shallower parts?