Add fiat-crypto and deps to released

[JasonGross]

Blocked on mit-plv/rupicola#52, but ready for review on the textual bits

For coq/platform#178

[palmskog]

@JasonGross packages look good, but two nitpicks:

• some synopsis fields end in a period, which raises a warning from opam lint (still allowed if you really want it)
• some packages are missing description fields - for Platform packages, it would be nice if these said a bit more about what the package actually contains (but skip if you prefer)

[JasonGross]

Can someone explain this error to me?

# File "./src/Bedrock/Group/Loops.v", line 3, characters 0-47:
# Error: Cannot find a physical path bound to logical path
# Rupicola.Lib.ControlFlow.DownTo.

Insofar as I can tell locally, the install target for rupicola does install lib/coq/user-contrib/Rupicola/Lib/ControlFlow/DownTo.vo

[silene]

There is no way it can ever work with the Github tarball. (I am even surprised that it works with the Git repository, but I guess git ls-files is exceedingly lenient when matching patterns.)

ALLDIR := $(shell cygpath -m "$$(pwd)" 2>/dev/null || pwd)/src/Rupicola
VS_ALL:=$(abspath $(shell git ls-files "$(ALLDIR)/*.v"))
Makefile.coq: force _CoqProject
	@$(COQ_MAKEFILE) $(VS_ALL) -o Makefile.coq

[JasonGross]

Ah, thanks! I'll fix it to use find when .git is missing

[silene]

Then, remember to add "conf-findutils" {build} in the depends section, in order to make sure find is available.

[JasonGross]

Then, remember to add "conf-findutils" {build} in the depends section, in order to make sure find is available.

I've added these. Is there a conf package for sed?

[silene]

I don't think so. But I would not be surprised if Sed itself is needed to build Opam, so it might implicitly be there. (Do not assume that this is GNU Sed, though.)

[palmskog]

Looks like we now got this "informative" error for fiat-crypto on 4.13:

# make: *** [Makefile.coq:764: src/Spec/Curve25519.vo] Error 1
# make: *** Waiting for unfinished jobs....

Could it be something with plugins/OCaml?

[JasonGross]

Looks like we now got this "informative" error for fiat-crypto on 4.13:

# make: *** [Makefile.coq:764: src/Spec/Curve25519.vo] Error 1
# make: *** Waiting for unfinished jobs....

Could it be something with plugins/OCaml?

I don't think that file uses any plugins / OCaml. I'm guessing timeout or OOM, unless the error is actually in a different file?

[silene]

I'm guessing timeout or OOM, unless the error is actually in a different file?

No, it really seems to be in that file:

File "./src/Spec/Curve25519.v", line 38, characters 17-49:
Error: The reference Pocklington_simple_computational was not found in the current environment.

[JasonGross]

Ah, this is an issue with coqprime. I think we need @thery to release a new version of coqprime with this change, and then set Fiat Crypto's minimum coqprime version to this not-yet-released version.

[palmskog]

@JasonGross looks like the only remaining failure (as opposed to timeout) is due to OOM:

# COQC src/ArithmeticCPS/ModOps.v
# COQC src/Curves/EdwardsMontgomery.v
# Killed
# make: *** [Makefile.coq:763: src/Curves/Weierstrass/AffineProofs.vo] Error 137
# make: *** Waiting for unfinished jobs....

Maybe we merge this even with the failure?

[JasonGross]

Great! Thanks for all the help making this work everyone!