Cava building issue

[nanoeng]

Howdy,

Please, accept my apologies beforehand for the noob question.

I'm trying to build SilverOak on an Ubuntu 22.04 LTS box using the following framework

• Coq v8.15.0
• GHCi v8.8.4
• Cabal v3.0.0.0 (compiled using Cabal library v3.0.1.0)
• Verilator v4.210

When I try to build the Cava system I'm getting the error messages shown at the end of this post.

I tried building the system in two different Linux boxes with similar results. Am I missing anything obvious during the process?

Appreciate your help.

silveroak$ make
make -C third_party
make[1]: Entering directory '/home/user/silveroak/third_party'
make build-coqutil
make[2]: Entering directory '/home/user/silveroak/third_party'
make -C bedrock2/deps/coqutil all
make[3]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
Generating Makefile.coq.all
make -f Makefile.coq.all
make[4]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make[5]: Nothing to be done for 'real-all'.
make[4]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make[3]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make[2]: Leaving directory '/home/user/silveroak/third_party'
make build-bedrock2
make[2]: Entering directory '/home/user/silveroak/third_party'
make -C bedrock2/deps/coqutil all
make[3]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
Generating Makefile.coq.all
make -f Makefile.coq.all
make[4]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make[5]: Nothing to be done for 'real-all'.
make[4]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make[3]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make -C bedrock2 bedrock2_noex
make[3]: Entering directory '/home/user/silveroak/third_party/bedrock2'
make -C /home/user/silveroak/third_party/bedrock2/deps/coqutil
make[4]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
Generating Makefile.coq.all
make -f Makefile.coq.all
make[5]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make[6]: Nothing to be done for 'real-all'.
make[5]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make[4]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make -C /home/user/silveroak/third_party/bedrock2/bedrock2 noex
make[4]: Entering directory '/home/user/silveroak/third_party/bedrock2/bedrock2'
Generating Makefile.coq.noex
Warning: No common logical root.
Warning: In this case the -docroot option should be given.
Warning: Otherwise the install-doc target is going to install files
Warning: in orphan_bedrock2_bedrock2Examples_coqutil
rm -f .coqdeps.d
make -f Makefile.coq.noex
make[5]: Entering directory '/home/user/silveroak/third_party/bedrock2/bedrock2'
make[6]: Nothing to be done for 'real-all'.
make[5]: Leaving directory '/home/user/silveroak/third_party/bedrock2/bedrock2'
make[4]: Leaving directory '/home/user/silveroak/third_party/bedrock2/bedrock2'
make[3]: Leaving directory '/home/user/silveroak/third_party/bedrock2'
make -C bedrock2 compiler_noex
make[3]: Entering directory '/home/user/silveroak/third_party/bedrock2'
make -C /home/user/silveroak/third_party/bedrock2/deps/coqutil
make[4]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
Generating Makefile.coq.all
make -f Makefile.coq.all
make[5]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make[6]: Nothing to be done for 'real-all'.
make[5]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make[4]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coqutil'
make -C /home/user/silveroak/third_party/bedrock2/deps/coq-record-update
make[4]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coq-record-update'
make[5]: Entering directory '/home/user/silveroak/third_party/bedrock2/deps/coq-record-update'
COQTEST tests/RegressionTests.v (ref: tests/RegressionTests.ref)
--- tests/RegressionTests.ref 2022-05-18 22:09:17.101422264 -0500
+++ /tmp/tmp.550hjEGyOV 2022-05-20 10:41:45.602078768 -0500
@@ -1,3 +1,4 @@
+File "/home/user/silveroak/third_party/bedrock2/deps/coq-record-update/tests/RegressionTests.v", line 19, characters 2-66:
The command has indeed failed with message:
The following term contains unresolved implicit arguments:
(fun (r : X) (a : nat) => r <| getA := a |>)
make[6]: *** [Makefile.coq.local:37: tests/RegressionTests.vo] Error 1
make[5]: *** [Makefile.coq:387: all] Error 2
make[5]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coq-record-update'
make[4]: *** [Makefile:9: all] Error 2
make[4]: Leaving directory '/home/user/silveroak/third_party/bedrock2/deps/coq-record-update'
make[3]: *** [Makefile:53: coq-record-update] Error 2
make[3]: Leaving directory '/home/user/silveroak/third_party/bedrock2'
make[2]: *** [Makefile:35: build-bedrock2] Error 2
make[2]: Leaving directory '/home/user/silveroak/third_party'
make[1]: *** [Makefile:50: bedrock2] Error 2
make[1]: Leaving directory '/home/user/silveroak/third_party'
make: *** [Makefile:37: third_party] Error 2

[samuelgruetter]

I haven't built silveroak in a while, but here are some tricks that I'd try (some didn't work, but I'm still mentioning them because sometimes they do work):

• Go to the commits list, pick the latest commit with a geen CI tick, click on that tick to get to the details of the CI build, and try to find the versions of Coq & dependencies that were used on CI. Unfortunately, when I try to expand the log, it says Error: The log was not found. It may have been deleted based on retention settings., so no luck here. But I see that it runs nix-shell.
• So let's look for some nix config files: I don't understand nix, but the repo contains some files with nix in their name, and these two lines look interesting:
  

  silveroak/default.nix

  Lines 17 to 18 in cccfdb4

  	optionals withCoq [
  	coq_8_13

• That suggests that CI is using Coq 8.13, so I'd try Coq 8.13.2.
• But probably you don't want to erase Coq 8.15.0 from your system, so you could create a separate opam switch into which you install the older Coq version, so that it does not interfere with your other Coq installations. If you haven't used opam switches before, here's a quick guide on how to install an old Coq version.

Hope that helps, and feel free to post again if the build gets stuck somewhere else!

[nanoeng]

Thanks @samuelgruetter for the detailed reply!
Appreciate the descriptions associated to the installation/management of the CoQ framework.

[nanoeng]

@samuelgruetter, thanks for all the detailed suggestions! After playing around with the set up and making sure v8.13.2 was the CoQ version, I was able to build SilverOak without any error.

[blaxill]

Unfortunately no-one is actively maintaining Cava, and it appears a dependency (and also perhaps Cava itself) needs updating for recent versions of Coq.

If you are able to use nix, that will provide you with a snapshot of working dependencies. As per Sam's suggestion- if you are able to use Coq 8.13.x then everything should work. Otherwise you may have success manually updating the third_party/bedrock2 submodule, but unfortunately it might require additional fixes.

[nanoeng]

Thanks, @blaxill!

I'll have a look at nix.