antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Upgrade hs-to-coq to GHC 8.6, 8.8, 8.10 #165

Closed Lysxia closed 4 years ago

Lysxia commented 4 years ago

This also makes sure to still work with 8.4

I think this PR is already in a mergeable state on its own, but here are some TODOs for the near future:

lastland commented 4 years ago

Thanks! This looks good.

Unfortunately, examples/ghc does not seem to be working with hs-to-coq of later GHC versions. We still need this example, but maybe this shouldn't keep us from compiling hs-to-coq with later versions of GHC? Maybe we can merge this version and document this in README.

lastland commented 4 years ago

Another issue is examples/ghc depends on this version of base. Updating base would also impact examples/ghc. Maybe to keep examples like ghc work and support later versions of Haskell base library we would need to have separate versions of translated base and separate base/edits.

An alternative may be using Git branches to keep different versions of base in different branches. Not sure if this would be a good idea though...

Lysxia commented 4 years ago

Oh that is a bummer.

Maybe there is a way to fix the build, for example if it's a sufficiently small patch? I made a little more progress to translate examples/base-src with this new version of hs-to-coq by enabling -XNoStarIsType but after that I'm stuck on a real GHC panic for now.

That said, one would most likely want to use a translation of the same base version as the one hs-to-coq was compiled with. So for this support for multiple versions of GHC to be useful, we have to figure out how to maintain multiple Coqified versions of base anyway.

The ideal setup I can imagine is to only maintain edits files and a few handwritten .v files to handle whatever hardwiring GHC does. We would only need to track a small enough number of files in git, so it can all be done in a single branch for all supported versions of GHC, base, etc.. From that we would generate the translated base automatically on the fly for any chosen version. (The main concern for that checking that into the repo would be too much bloat.) How feasible does that sound?

For releases we can have a separate repo with the Coqified base + theories, updated periodically for Opam packaging.