Jason Gross

QuickChick fails when modules are open with "Error: Unbound value quickchick"

1

``` (* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "." "QC" "-top" "QC.EverythingQCRequires") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 24 lines...

Add rocq-lean-import to the platform

2

Could https://github.com/rocq-community/rocq-lean-import be added to the Platform?

Build fails on master, blocking Coq bench

1

Coq has not been benching fiat crypto for a while because bedrock 2 is [failing with](https://coq.gitlabpages.inria.fr/-/coq/-/jobs/6368987/artifacts/_bench/logs/coq-bedrock2.NEW.opam_install.1.stderr.log) ``` # [...] # The term "impl1_refl" has type "impl1 (seps Frame) (seps Frame)"...

``` COQFLAGS="-Q src/bedrock2 bedrock2 -Q src/bedrock2Examples bedrock2Examples -Q D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil " ../etc/bytedump.py bedrock2.PrintListByte.allBytes > special/BytedumpTest.out.tmp No module named 'resource' Coq < Coq < Coq < Toplevel input, characters 25-35: >...

Following up on #2218, I see ``` Run echo "=== Disk space usage ===" === Disk space usage === Filesystem Size Used Avail Use% Mounted on /dev/root 72G 65G 6.7G...

It seems to take around 6h, which is about 2x the time of MacOS 14. Can we speed things up at all?

Replaces #2055 Closes #2055 Fixes #2050

Reverts mit-plv/fiat-crypto#2045 #2043 redux Waiting on merge of: - #2044