Cabal build is not working for me

[jadephilipoom]

I don't know if I have the wrong cabal version or a missing dependency (base?), but after a checkout of main and a make clean I get this error from the cava haskell target:

./FixupHaskell
mv Ascii2.hs Ascii.hs
mv ByteVector2.hs ByteVector.hs
cabal build
Resolving dependencies...
cabal: Could not resolve dependencies:
[__0] trying: Cava2HDL-0.1.0.0 (user goal)
[__1] trying: base-4.13.0.0/installed-4.1... (dependency of Cava2HDL)
[__2] next goal: cava-examples (user goal)
[__2] rejecting: cava-examples-0.1.0.0 (conflict:
base==4.13.0.0/installed-4.1..., cava-examples => base>=4.14 && <4.15)
[__2] fail (backjumping, conflict set: base, cava-examples)
After searching the rest of the dependency tree exhaustively, these were the
goals I've had most trouble fulfilling: base, Cava2HDL, cava-examples

[satnam6502]

I've not been following along about how we got here, but why are we using cabal for the examples?

[blaxill]

Can you tell me your Haskell version ghc --version? We updated to GHC 8.10 a few weeks back, upgrading your Haskell should solve the issue, but also the constraints on base (GHC package) are unnecessarily strict and so I'll relax that too.
Edit: I also need to update the main README.md

[jadephilipoom]

That's probably it, then -- I have version 8.8.4. That's also the latest version on the gLinux package manager, though, and I'd prefer not to have to maintain a from-source installation if possible.

[blaxill]

I've not been following along about how we got here, but why are we using cabal for the examples?

There are definitely some benefits to using cabal:

• builds are sandboxed and don't require installing packages system wide
• project level configuration effecting our cava/pinmux/aes etc
• cabal is pretty ubiquitous in the haskell world these days, and issues from prior years around cabal dependency solving issues are mostly solved

The cabal changes will be easiest to roll back if there are usability issues, but i expect things to be simpler going forward (after potentially some speed bumps such as this). In the long run I still see us potentially removing Haskell and moving all logic to Coq.

I'd like to make a few more changes to simplify our source tree in #742 such that we only have source/project files in our source tree and artefacts/compilation objects are put into other directories (dune being the simplest way to achieve this for Coq). That in turn will simplify browsing through the directory hierarchy but also more tangible benefits like simplifying our makefile building and cleaning rules.

[blaxill]

That's probably it, then -- I have version 8.8.4. That's also the latest version on the gLinux package manager, though, and I'd prefer not to have to maintain a from-source installation if possible.

Let me relax the constraints in the cabal files, we should be fine with 8.8.4

[atondwal]

that doesn't seem to fix it: running make clean; nix-shell and then make

[nix-shell:~/src/silveroak]$ make
make -C third_party
make[1]: Entering directory '/home/atondwal/src/silveroak/third_party'
make build-coqutil
make[2]: Entering directory '/home/atondwal/src/silveroak/third_party'
make -C bedrock2/deps/coqutil all
make[3]: Entering directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
Generating Makefile.coq.all
make -f Makefile.coq.all
make[4]: Entering directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
make[5]: Nothing to be done for 'real-all'.
make[4]: Leaving directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
make[3]: Leaving directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
make[2]: Leaving directory '/home/atondwal/src/silveroak/third_party'
make build-bedrock2
make[2]: Entering directory '/home/atondwal/src/silveroak/third_party'
make -C bedrock2/deps/coqutil all
make[3]: Entering directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
Generating Makefile.coq.all
make -f Makefile.coq.all
make[4]: Entering directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
make[5]: Nothing to be done for 'real-all'.
make[4]: Leaving directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
make[3]: Leaving directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
make -C bedrock2 bedrock2_noex
make[3]: Entering directory '/home/atondwal/src/silveroak/third_party/bedrock2'
make -C /home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil
make[4]: Entering directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
Generating Makefile.coq.all
make -f Makefile.coq.all
make[5]: Entering directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
make[6]: Nothing to be done for 'real-all'.
make[5]: Leaving directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
make[4]: Leaving directory '/home/atondwal/src/silveroak/third_party/bedrock2/deps/coqutil'
make -C /home/atondwal/src/silveroak/third_party/bedrock2/bedrock2 noex
make[4]: Entering directory '/home/atondwal/src/silveroak/third_party/bedrock2/bedrock2'
Generating Makefile.coq.noex
rm -f .coqdeps.d
make -f Makefile.coq.noex
make[5]: Entering directory '/home/atondwal/src/silveroak/third_party/bedrock2/bedrock2'
make[6]: Nothing to be done for 'real-all'.
make[5]: Leaving directory '/home/atondwal/src/silveroak/third_party/bedrock2/bedrock2'
make[4]: Leaving directory '/home/atondwal/src/silveroak/third_party/bedrock2/bedrock2'
make[3]: Leaving directory '/home/atondwal/src/silveroak/third_party/bedrock2'
make[2]: Leaving directory '/home/atondwal/src/silveroak/third_party'
make build-extlib
make[2]: Entering directory '/home/atondwal/src/silveroak/third_party'
make -C coq-ext-lib theories
make[3]: Entering directory '/home/atondwal/src/silveroak/third_party/coq-ext-lib'
make -f Makefile.coq
make[4]: Entering directory '/home/atondwal/src/silveroak/third_party/coq-ext-lib'
W: This Makefile was generated by Coq 8.12.0
W: while the current Coq version is 8.13.1
make[5]: Nothing to be done for 'real-all'.
make[4]: Leaving directory '/home/atondwal/src/silveroak/third_party/coq-ext-lib'
make[3]: Leaving directory '/home/atondwal/src/silveroak/third_party/coq-ext-lib'
make[2]: Leaving directory '/home/atondwal/src/silveroak/third_party'
make build-record-update
make[2]: Entering directory '/home/atondwal/src/silveroak/third_party'
make -C coq-record-update
make[3]: Entering directory '/home/atondwal/src/silveroak/third_party/coq-record-update'
make[4]: Entering directory '/home/atondwal/src/silveroak/third_party/coq-record-update'
W: This Makefile was generated by Coq 8.12.0
W: while the current Coq version is 8.13.1
make[5]: Nothing to be done for 'real-all'.
make[4]: Leaving directory '/home/atondwal/src/silveroak/third_party/coq-record-update'
make[3]: Leaving directory '/home/atondwal/src/silveroak/third_party/coq-record-update'
make[2]: Leaving directory '/home/atondwal/src/silveroak/third_party'
make[1]: Leaving directory '/home/atondwal/src/silveroak/third_party'
make -C cava
make[1]: Entering directory '/home/atondwal/src/silveroak/cava'
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq
make[2]: Entering directory '/home/atondwal/src/silveroak/cava'
COQDEP VFILES
make[3]: Nothing to be done for 'real-all'.
make[2]: Leaving directory '/home/atondwal/src/silveroak/cava'
./FixupHaskell
mv Ascii2.hs Ascii.hs
mv ByteVector2.hs ByteVector.hs
cabal build
Warning: The package list for 'hackage.haskell.org' does not exist. Run 'cabal
update' to download it.RemoteRepo {remoteRepoName = RepoName
"hackage.haskell.org", remoteRepoURI = http://hackage.haskell.org/,
remoteRepoSecure = Just True, remoteRepoRootKeys =
["fe331502606802feac15e514d9b9ea83fee8b6ffef71335479a2e68d84adc6b0","1ea9ba32c526d1cc91ab5e5bd364ec5e9e8cb67179a471872f6e26f0ae773d42","2c6c3627bd6c982990239487f1abd02e08a02e6cf16edb105a8012d
444d870c3","0a5c7ea47cd1b15f01f5f51a33adda7e655bc0f0b0615baa8e271f4c3351e21d","51f0161b906011b52c6613376b1ae937670da69322113a246a09f807c62f6921"],
remoteRepoKeyThreshold = 3, remoteRepoShouldTryHttps = True}
Resolving dependencies...
Build profile: -w ghc-8.10.4 -O1
In order, the following will be built (use -v for more details):
 - Cava2HDL-0.1.0.0 (lib) (first run)
Configuring library for Cava2HDL-0.1.0.0..
Preprocessing library for Cava2HDL-0.1.0.0..
cabal: can't find source for Number in .,
/home/atondwal/src/silveroak/dist-newstyle/build/x86_64-linux/ghc-8.10.4/Cava2HDL-0.1.0.0/build/autogen,
/home/atondwal/src/silveroak/dist-newstyle/build/x86_64-linux/ghc-8.10.4/Cava2HDL-0.1.0.0/build/global-autogen

make[1]: *** [Makefile:38: haskell] Error 1
make[1]: Leaving directory '/home/atondwal/src/silveroak/cava'
make: *** [Makefile:37: cava] Error 2

[nix-shell:~/src/silveroak]$

[jadephilipoom]

I think it's a different issue -- my issue was fixed by #749, and this one is telling you it can't find Number. I think it's from this change in #741 : https://github.com/project-oak/silveroak/pull/741/files#diff-63ce5a2c3979e210134e4c38ee5a561a605a34edca190ac7d1e5b780dc28b1f2L90

A make clean might fix it.

[atondwal]

Yep, I was just using the wrong make clean, since the underscore confused me.