Split out the examples from the source code

[antalsz]

There's a lot going on in this repository:

1. The hs-to-coq conversion tool itself
2. An abandoned GHC plugin that enables converting between structurally isomorphic types
3. The converted parts of the base library
4. Other converted examples

It would be nice to split this up into multiple repositories, because they're conceptually separate. The downside, of course, is that the examples depend on base which depends on hs-to-coq.

[antalsz]

One possible new structure:

1. An hs-to-coq repo containing hs-to-coq, along with a couple of examples showing how to use the tool. These examples should be static – they're documentation. Possible examples:

   1. One example (Succs?) that can be built without base
   2. One example (Hutton's razor?) that uses base.

2. A base-in-coq repo containing just base. Depends on hs-to-coq

3. A ghc-in-coq repo containing our converted parts of GHC. Depends on hs-to-coq and base-in-coq.

4. Maybe a repo for the plugin, if it still seems useful.

[nomeata]

I am in favor of removing the abandoned plugin and getting rid of the extra subdirectory.

Otherwise, I think it is far too early to do this. We are still in a change where we need to make changes that affect both the tool and all the developments (adding edits, changing how certain things are translated or named). Having to make highly coupled changes in independent repositories will cause great confusion and friction.

Also, the best test suite we have is … all of example. They serve as regression test suite that we sorely need, otherwise changes to the code will break some of these, and will not be noticed much later.

Once we find, empirically, that most work on stuff in examples can proceed without changes to the code, and that most changes to the code do not affect the examples, then this becomes a viable and desirable goal. But unfortunately, we are not there yet…

(Note that for precisely this reason, GHC eventually moved testsuite/ and libraries/base into the GHC repository – and that is a mature compiler…)

[nomeata]

It might interesting, though, to think of a better way of managing the generated files in examples/ghc-base/lib (and, maybe examples/ghc/lib). They should be easily accessible without a GHC checkout, but having them in the repo is not ideal (although useful – I look at the diff to see what my changes to the code did).

One could put them in a git submodule which lives on a different branch of the same repository.