Skip to content

update fiat-crypto and dependencies to Sep 2025 - #3529

Open
andres-erbsen wants to merge 4 commits into
rocq-prover:masterfrom
andres-erbsen:fiat-crypto-2025-09
Open

update fiat-crypto and dependencies to Sep 2025#3529
andres-erbsen wants to merge 4 commits into
rocq-prover:masterfrom
andres-erbsen:fiat-crypto-2025-09

Conversation

@andres-erbsen

Copy link
Copy Markdown
Contributor

I don't know what I'm doing; just semi-blindly following mit-plv/coqutil#141 (comment) with limited natural intelligence.

@andres-erbsen

Copy link
Copy Markdown
Contributor Author

# Fatal error: exception Invalid_argument("Sys.getcwd not implemented")

I don't knwo what this means. @JasonGross ?

@JasonGross

Copy link
Copy Markdown
Member

I think this means "4.07 is too old for the CI infra"? (This is a failure on ocaml-base-compiler.4.07.1). Hopefully the other tests will pass

Comment thread released/packages/coq-bedrock2/coq-bedrock2.0.0.9/opam Outdated
Comment thread released/packages/coq-riscv/coq-riscv.0.0.6/opam Outdated
Comment thread released/packages/coq-rupicola/coq-rupicola.0.0.11/opam Outdated
Comment thread released/packages/coq-kami/coq-kami.0.0.4-rv32i/opam Outdated
Comment thread released/packages/coq-fiat-crypto/coq-fiat-crypto.0.1.6/opam Outdated
synopsis: "A work-in-progress language and compiler for verified low-level programming"
tags: ["logpath:kami"]
url {
src: "https://github.com/mit-plv/kami/archive/refs/tags/v0.0.3.tar.gz"

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@andres-erbsen This should be 0.0.4, right?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did not write this line so if you think so you're probably right

@JasonGross

Copy link
Copy Markdown
Member

@andres-erbsen Could you also update the bedrock2-compiler package?

@silene

silene commented Oct 9, 2025

Copy link
Copy Markdown
Contributor
File "./Kami/Lib/NatLib.v", line 1, characters 15-29:
Error: Cannot find a physical path bound to logical path Stdlib.Arith.Div2.

@JasonGross

JasonGross commented Oct 9, 2025

Copy link
Copy Markdown
Member

Kami is not actually required, I believe, we can update the other packages without updating kami.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants