Add a dependency on the bedrock2 compiler

[jadephilipoom]

This needs to be in place for an end-to-end proof of X25519. Pushing it early because I kind of suspect there'll be issues with some Coq version or another, but feel free not to merge until something actually using it is ready.

Unfortunately, the MMIO.v file that is extremely helpful for instantiating the compiler proof is in the compiler's "examples" folder, meaning we have to build all the examples from both bedrock2/bedrock2 and bedrock2/compiler. Could it be moved?

[JasonGross]

I think you'll need to rebase on #1046 to get the CI to pass

[JasonGross]

If you rebase on master now, this should hopefully build better

[JasonGross]

Issue 1:

make -C /home/runner/work/fiat-crypto/fiat-crypto/rupicola/bedrock2/deps/coq-record-update
COQTEST tests/coqpl_2021.v (ref: tests/coqpl_2021.ref)
tests/coqpl_2021.vo (real: 0.10, user: 0.05, sys: 0.04, mem: 82640 ko)
--- tests/coqpl_2021.ref	2021-11-15 01:25:57.860661525 +0000
+++ /tmp/tmp.R7U7DPLUjA	2021-11-15 01:34:33.430904862 +0000
@@ -22,14 +22,17 @@
 More precisely: 
 - ?Setter: Cannot infer the implicit parameter Setter of set whose type is
   "Setter get_A" (no type class instance found).
+File "/home/runner/work/fiat-crypto/fiat-crypto/rupicola/bedrock2/deps/coq-record-update/tests/coqpl_2021.v", line 60, characters 29-70:
 The command has indeed failed with message:
 In environment
 x : several_nats
 The term "Build_several_nats (nat1 x) (nat3 x)" has type
  "nat -> several_nats" while it is expected to have type 
 "several_nats".
+File "./src/RecordSet.v", line 25, characters 11-23:
 The command has indeed failed with message:
 Tactic failure: incorrect settable! declaration (perhaps fields are out-of-order?).
+File "./src/RecordSet.v", line 25, characters 11-23:
 The command has indeed failed with message:
 Tactic failure: incorrect settable! declaration (perhaps fields are out-of-order?).
 The command has indeed failed with message:
make[4]: *** [Makefile.coq.local:37: tests/coqpl_2021.vo] Error 1

Issue 2:

make: *** No rule to make target 'bedrock2-compiler', needed by 'deps'.  Stop.

Very confused by this one.

[JasonGross]

Is it possible that make doesn't like recipes that start with #? What happens if you do

Suggested change

	# We have to build the compiler *including* examples to get compilerExamples/MMIO.v
	@# We have to build the compiler *including* examples to get compilerExamples/MMIO.v

instead?

[jadephilipoom]

Adjusted to try that. The "no rule" error is especially weird because this does build locally with make.

[jadephilipoom]

Same error. Fascinating.

[JasonGross]

Strange. Does coq-record-update build fine for you locally? Maybe it makes sense to first fix the coq-record-update failure and then look into this failure after?

[andres-erbsen]

@JasonGross Do you understand what is up with coq-record-update? https://github.com/mit-plv/bedrock2/runs/4257766583?check_suite_focus=true#step:6:1477 is a succeeding run on coq master.

[JasonGross]

I'm guessing that the trick we pull to get warning annotations at

fiat-crypto/etc/ci/github-actions-make.sh

Line 23 in edba07d

reportify="COQC='$(pwd)/etc/coq-scripts/github/reportify-coq.sh'${reportify} ${COQBIN}coqc"

is messing with the output of COQTEST somehow such that https://github.com/tchajed/coq-record-update/blob/f2467e2b614bf35913c5e2406be4d67fbd85e7a4/test-normalizer.sed#L9 is not working right? But I don't see how this is happening. I've pushed a change to master that should give us more information when the CI fails (by re-running make with VERBOSE=1), and will force-push a rebase of this on master to see if it helps.

[andres-erbsen]

I think it's just that the bedrock2 referenced here doesn't include tchajed/coq-record-update@f2467e2 yet.

[JasonGross]

I think it's just that the bedrock2 referenced here doesn't include tchajed/coq-record-update@f2467e2 yet.

Ah, that sounds right

[JasonGross]

And the extra text from the debug invocation suggests that the failure message is some weird interaction between include and failed dependencies and the fact that deps depends on both bedrock2 and bedrock2-compiler and bedrock2 itself depends on bedrock2-compiler, which is not necessary:

Considering target file 'deps'.
 File 'deps' does not exist.
  Considering target file 'rewriter'.
  File 'rewriter' was considered already.
  Considering target file 'bedrock2'.
  File 'bedrock2' was considered already.
  Considering target file 'bedrock2-compiler'.
  Recently tried and failed to update file 'bedrock2-compiler'.
make: *** No rule to make target 'bedrock2-compiler', needed by 'deps'.  Stop.

[JasonGross]

I've rebased this, now that the rupicola bump is merged

[JasonGross]

CI passes, so I'm going to merge this