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.

[JasonGross]

@MSoegtropIMC The concern is that the latest version of bedrock2 fails to compile on our Windows CI, and we are planning on removing Windows from our CI here to deal with that because none of us have time to debug Windows. I'm concerned about whether this will mean that fiat-crypto gets excluded from the Platform when the next release rolls around. The issue seems to be a bug in Coq, because as far as I can tell, coqc dies with an out of memory error while processing a beginning-of-file comment followed by Require Import Coq.Lists.List. (evidence: passing -timing-file to coqc results in an empty timing file) (cf coq/coq#20212), and time coqc does not record excessive memory usage. If you happen to have the time and inclination to test whether or not the latest dev version of coq-bedrock2 successfully compiles src/bedrock2Examples/kyberslash.v (I think From bedrock2Examples Require Import kyberslash. should work as a smoke test) on Windows, and potentially look at what the actual error is / post a reproducer on coq/coq#20212, that could help prevent accumulating divergences that might have to be fixed at platform-release-time.

[MSoegtropIMC]

@JasonGross : a stack overflow can also give an out of memory (depends on how stacks are organised). Afaik this changed in OCaml 5 from OCaml 4. In OCaml 5 (afaik) the initial process stack is not really used and a new thread with dynamic stack created (just hearsay - I have no solid knowledge about this). I have no idea how large these stacks are and if they can grow on Windows. With OCaml 4.X I can safely set the main thread stack size to arbitrary sizes by patching the binaries. This stack does grow. I currently do this for ocamlc, but not for coqc.

This is done here: https://github.com/coq/platform/blob/c64cb9a6d4282f03c39b0b6171cb87ef411a5021/shell_scripts/install_ocaml_stacksize.sh#L15

If one wants to do it for coqc, one would have to do it after coqc has been compiled. But if you have a Coq Platform cygwin the patch program is compiled and you can just call it for coqc after installing coq and before compiling bedrock.

I can have a look later this week. Is your Windows CI is Coq Platform based as the Coq CI?

[JasonGross]

I don't see how stack overflow could cause a failure without emitting anything to the timing file, though. And note that this is bedrock2, not fiat-crypto, and shouldn't require excessive stack.

I can have a look later this week. Is your Windows CI is Coq Platform based as the Coq CI?

Thank you! The setup is based on the setup-ocaml action + opam install coq, not based on the platform script. Happy to move to the platform script if that fixes things though.

[MSoegtropIMC]

OK, I will have a look - it will take a few days, though (busy with the platform release).

[OwenConoly]

If you can't compile Coq itself, you are doing something wrong.

Well yes, I figured that was the case! Could you help me see what I am doing wrong? I basically just installed opam in the way recommended on the opam website, and then I tried to install coq (and the other packages Jason said I should install) using opam, and it failed. Is the actual process more complicated than that?

Here is a complete transcript of everything I did, starting from installing windows 11 in a VM. Maybe you can point out the problem?

coq_installation_attempt.txt

Of course, it is quite understandable if you'd rather just look at the thing yourself rather than try to fix whatever I am doing wrong :)