Update haskell code to use GHC 8.4/cabal 2.2 (Stackage LTS 12.7 snapshot)

[yanok]

This makes it possible to run a full test suite on my Mac.

All tests pass for the default arch setting.

Fixes #24

[lsf37]

Thank you! This looks promising. I'll pull it into our internal regression test to see how it plays with the infrastructure there.

[Xaphiosis]

Overall comments so far:

• general impression is favourable, thank you for your contribution
• hiding count{Leading,Trailing}Zeros can probably be translated into removing our versions of the functions which are copied from the Haskell Data.Bits anyway, but that will require a bit more tweaking

Question: when you say "all tests pass for the default arch setting", you are referring to ./run_tests ? Really glad to see that.

Some comments on conventions:

• usual prefix for "HaskellKernel" in commits is "haskell", similarly "lib"
• "start switching to newer GHC/cabal-install" - when looking back at this in future, "newer" will be unclear, please consider indicating a version
• "it will never hurt" - I suggest dropping future-predictive optimism, experience indicates everything hurts

@yanok : could you make the small commit cosmetic tweaks, and then we'll be able to merge this internally

@lsf37 : the above aside, I am in favour of this change; note this puts a nail in the "executable" spec being executable on ARM until its next resurrection

[yanok]

@Xaphiosis :

• I've thought about removing custom count{Leading,Trailing}Zeros and using the library functions instead. I think it will make Haskell look better, but at the same time it means they have to be implemented also in HaskellLib_H theory. That's not hard to do, but that will be two more functions for which we take for granted that the Isabelle translation matches the actual library code. So I decided it's probably better to leave the code as is and let the translator generate matching Isabelle code automatically.
• yep, I've used ./run_tests to verify I didn't break anything.
• I've addressed your comments regarding the commit messages.
• As for the "it will never hurt" part... I agree that it's a big vague and over-optimistic. At the same time I'm pretty confident that this change is safe: if a generated module uses unqualified Word type, it surely wants the one from the package itself, not from Prelude, so in that cases extra Prelude import will actually fix compilation. And if it doesn't use it, extra import won't change anything. The only problem I can see can arise if someone will put Prelude into BOOT-IMPORTS:. Should I add a check for that to the mkhsboot.pl script?

[lsf37]

Ok, from the regression test we get that all proofs work on all platforms, but actually running ghc fails with:

...
Downloaded ghc-8.4.3.
Unpacking GHC into /root/.stack/programs/x86_64-linux/ghc-8.4.3.temp/ ...
Configuring GHC ...
Installing GHC ...
Installed GHC.
Unable to load cabal files for snapshot

----
Deleting cached snapshot file: /root/.stack/build-plan/lts-12.7.yaml
Recommendation: try running again. If this fails again, open an upstream issue at:
https://github.com/fpco/lts-haskell/issues/new
----

Unable to parse cabal file for bhoogle-0.1.3.5@sha256:a3393794b22faabeb564c57f4a9506390b6b97b9792c6b4e130f15bf116099fd,1806: NoParse "license" 7
Makefile:74: recipe for target '.stack-work' failed
make: *** [.stack-work] Error 1

I haven't looked into yet what is going on precisely. Might just be something that needs to be installed on the regression test VMs. If it points to something obvious from your side, let me know.

[lsf37]

For count{Leading,Trailing}Zeros, the implementation in HaskellLib_H could just be what comes out of the current translation (i.e. the definition that gets generated in spec/design/Thread_H.thy). This wouldn't really change much apart from removing the special treatment from the Haskell source, which would be nice, I think.

[yanok]

@lsf37 When it breaks strangely like this, it is usually a sign that Stack itself needs to be updated, what version do you have installed? Could you try to run stack upgrade and make sure the new version is in PATH before the old one?

[lsf37]

Finally got around to doing that, and it indeed fixes the issue. The test is green now.

Only remaining question is the count{Leading,Trailing}Zeros. I don't actually mind much either way. @Xaphiosis, what do you think?

[Xaphiosis]

Agreed. I think we should leave those as is for now. We already have the implementations, and the proofs equating them to word_clz and word_ctz respectively, and there's not a fundamental reason to throw them away.

[lsf37]

Good. Rebased and merged internally -- it should appear on GitHub once the regression test passes.

[lsf37]

In case you're wondering what is taking so long, the regression test + automated push failed for a bunch of unrelated reasons, which should hopefully be resolved and we should see the merged PR in the next 24h.

[lsf37]

Has now appeared on github at 0044c57