Adapt to https://github.com/coq/coq/pull/19530

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat

http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf

Other

717 stars 147 forks source link

Adapt to https://github.com/coq/coq/pull/19530 #1957

Closed proux01 closed 2 months ago

proux01 commented 2 months ago

Adapt to https://github.com/coq/coq/pull/19530 This should be backward compatible and can be merged at your convenience, before the upstream PR.

JasonGross commented 2 months ago

@proux01

File "./src/Bedrock/End2End/RupicolaCrypto/Spec.v", line 1, characters 0-29:
Error: Required library Byte matches several files in path (found
/home/coq/.opam/4.13.1+flambda/lib/coq/theories/Init/Byte.vo and
/home/coq/.opam/4.13.1+flambda/lib/coq/theories/Strings/Byte.vo).

Why not leave the intermediates (From Coq Require Import Init.Byte or similar)? That would also be more future-proof against other duplicate names

proux01 commented 2 months ago

Why not leave the intermediates (From Coq Require Import Init.Byte or similar)?

Indeed it's required for Byte, done

That would also be more future-proof against other duplicate names

There should be no other duplicates, there is a check to ensure that in the CI of the new repository.

JasonGross commented 2 months ago

Only wasm is failing, I'm working on that in #1958, #1960, let's merge

proux01 commented 2 months ago

Thanks