switch GarageDoor to LeakageSemantics

[OwenConoly]

Resolves #2007.

This needs mit-plv/bedrock2#445 to be merged first.

[andres-erbsen]

To be merged after dependencies and CI.

[andres-erbsen]

For merging this, I think a simple plan would be to wait for the bedrock2 change to get into rupicola, then, bump rupicola synchronously with the GarageDoor changes in this PR. IIUC either wouldn't build without the other.

[andres-erbsen]

@JasonGross any guesses for what's up with windows? I wouldn't have expected the file in question to be heavy.

[JasonGross]

Almost certainly this is an issue with building deps with -j2.

https://docs.github.com/en/actions/using-github-hosted-runners/using-github-hosted-runners/about-github-hosted-runners#supported-runners-and-hardware-resources says Windows runners have 16 GB RAM.

The last successful Windows run claims a peak memory usage on deps of 19666352 ko for Rewriter/Rewriter/Reify.vo, which seems bogus, probably time can't measure memory on Windows accurately?

MacOS 13 and Windows both claim to be using Coq 8.18, and MacOS on this PR claims a peak memory usage on deps of 2282440 ko for rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo which is a lot more reasonable.

For kyberslash MacOS claims

 /Users/runner/work/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/kyberslash.vo (real: 20.35, user: 19.86, sys: 0.38, mem: 687276 ko)

which is indeed not that heavy.

It's hard to see what's running at the same time as kyberslash, so let's rebase on top of #2010 to remove --output-sync so we can see things a bit better.

[andres-erbsen]

I can't find any concurrency in the log.

D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo (real: 128.19, user: 0.12, sys: 0.42, mem: 289064 ko)
make[4]: *** [D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/kyberslash.vo] Deleting file 'D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/kyberslash.glob'
COQC D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/kyberslash.v
While loading initial state:
Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler,default]
Fatal error: out of memory
Command exited with non-zero status 3
D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/kyberslash.vo (real: 1074.22, user: 0.04, sys: 0.27, mem: 128372 ko)
Error: make[4]: *** [Makefile.coq.ex:838: D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/kyberslash.vo] Error 3
Error: make[3]: *** [Makefile.coq.ex:409: all] Error 2
Error: make[2]: *** [Makefile:71: ex] Error 2
Error: make[1]: *** [Makefile:90: bedrock2_ex] Error 2
+ python ./etc/coq-scripts/timing/make-one-time-file.py --real time-of-build.log time-of-build-pretty.log
make: *** No rule to make target 'bedrock2', needed by 'deps'.  Stop.
+ git status
HEAD detached at pull/2009/merge
Changes not staged for commit:
  (use "git add <file>..." to update what will be committed)
  (use "git restore <file>..." to discard changes in working directory)
  (commit or discard the untracked or modified content in submodules)
	modified:   rupicola (untracked content)

no changes added to commit (use "git add" and/or "git commit -a")
+ git ls-files --others --exclude-standard
+ git diff
+ cat time-of-build-pretty.log
     Time |    Peak Mem | File Name                                                                                                                   
------------------------------------------------------------------------------------------------------------------------------------------------------
43m52.00s | 19715484 ko | Total Time / Peak Mem                                                                                                       
------------------------------------------------------------------------------------------------------------------------------------------------------
17m54.22s |   128372 ko | D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/kyberslash.vo                                  
 2m08.19s |   289064 ko | D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo                                   

[JasonGross]

Can you tell the CI to upload files on failure? If we can look at D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/kyberslash.v.timing, we can see how far it got before failing.

[andres-erbsen]

https://github.com/mit-plv/fiat-crypto/actions/runs/13168644056

windows
No files were found with the provided path: timing-files.zip. No artifacts will be uploaded.

Does either of you have windows with coq set up to repro locally? I am puzzled by this failure and if it only happens on GithHub actions I think we should not block the merge on it.

[JasonGross]

https://github.com/mit-plv/fiat-crypto/actions/runs/13168644056

windows
No files were found with the provided path: timing-files.zip. No artifacts will be uploaded.

Sorry, fixed by 66b7bf5, let's try again

[JasonGross]

Does either of you have windows with coq set up to repro locally?

I don't have time to investigate right now (and am now on Mac), but you can get a Windows 11 VM on kvm.

I am puzzled by this failure and if it only happens on GithHub actions I think we should not block the merge on it.

I'd like to at least get a separate bedrock2 target, etc, that excludes these files from the build, and modify the windows CI to skip the files that don't build on Windows.

[OwenConoly]

Does either of you have windows with coq set up to repro locally?

I have a laptop with Windows 10 --- setting up Coq there would probably (?) be easy. Or I could try the Windows 11 VM. Do you think one of these things is worth doing?

[JasonGross]

Do you think one of these things is worth doing?

Yes, please!

There is something weird going on with kyberslash. The .timing file is empty, suggesting that it fails to even run the first Require Import, if that can be believed? The log claims it takes 784.50s (771.68s the second time through). This is obscenely longer than the 14.89s it takes on alpine edge (compare with lightbulb, which takes 134.28s on Windows and 100.40s on alpine).

If you can match the version & install config we use on CI (Coq 8.18.0, OCaml 4.13.1, install opam and then opam install conf-time conf-gcc 'ocamlfind>=1.9.7' && opam pin add --kind=version coq 8.18.0 and then opam exec -- make COQEXTRAFLAGS="-async-proofs-j 1" NJOBS="2" ...), then that makes it more likely you'll see similar behavior. It might be the case that simply moving to a different version of Coq or OCaml will fix the issue (in which case I'll record the incompatible version in the opam file and we can just update the CI). But if it's still present on newer versions of Coq, maybe there's a Coq or OCaml bug lurking here (maybe for some reason the comment at the top of the file triggers some weird issue?)

[OwenConoly]

Windows makes everything difficult, apparently. I've tried a couple ways to install Coq 8.18.0 and have given up for now.

Do you know off the top of your head what the attached error message means?
[ERROR] The compilation of coq-stdlib.txt

The error code "-1073741515" is meaningless, so far as I can tell from googling it...

[OwenConoly]

I get the same error code with a fresh install of windows in a VM, so it is probably not due to "corrupted system files or damaged operating system files", as a vague answer on the impressively useless website https://answers.microsoft.com suggests.

[andres-erbsen]

Let's drop windows altogether? We're at least as short on maintainer time as ever, and if we're not using it actively, I don't think it's wise to spend time trying to learn it to fix it.

[JasonGross]

Let's at least try updating first, see if that fixes anything

[JasonGross]

Seems a bit of a shame to lose one of the few intensive CI tests of Coq on Windows, and I imagine there will be some issues when the next Coq platform is released (cc @MSoegtropIMC), but you're right, not worth spending time on given limited resources.

[MSoegtropIMC]

I can't say I understand what this thread is about, but Coq Platform should work fine on Windows. I switched to arbitrary stack size and arbitrary path length in the 2024.10 release (for all picks, including 8.18 put only for executables which were known to require very large stack sizes). If Coq Platform (which provides a full fledged build environment if installed from sources) doesn't work for you I can have a look. E.g. if there is an opam package to try, give me the name. The only thing which is known to not work on Windows is plugins using Posix forks. If you can't compile Coq itself, you are doing something wrong.

Note that virus scanners frequently result in issues because they keep open on exe files freshly created exe files for a few seconds and you cannot delete an open file on WIndows (on Linux one can do this). I recently patched later versions of dune to just retry. You should keep virus scanners in a scan only mode for building Coq. If you can't do this it would likely be easy to fix this at the root (via retries) - I didn't do so as yet because it is hard to reproduce.

[MSoegtropIMC]

P.S.: for sure you can't compile fiat-crypto on Windows without Coq Platform - you need the large stack size patches.