Open quinn-dougherty opened 2 years ago
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
.
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.
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.
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”.)
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)
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.
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.
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 runninghs-to-coq
onData/ByteString.hs
(withaxiomatize 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-coq
ing shallower parts?
Hello!
I have a minimal example here. the
hs-to-coq
executable was created withstack install
, but there is some nix in hereMain.hs
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'
Notice that
lens
appears inhs-to-coq.cabal
.edits
And when we run we fail
Perhaps this is what
--import-dir
is for?where are my libraries for this version of ghc?
ok,
lens
is in that directory. So if we run......well, we get the same error.
Let's add
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 ofghc
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 thehs-to-coq
executable calls upon. Moreover, it'd be great to have observability into what packages are reachable by theghc
that thehs-to-coq
executable calls upon.