Gaëtan Gilbert (Oct 08 2022 at 11:02): Gaëtan Gilbert (Oct 08 2022 at 11:02):IIRC the current project timeout of 1 day was because of the windows job, should we use something shorter now?
Emilio Jesús Gallego Arias (Oct 08 2022 at 13:53):Yes
Gaëtan Gilbert (Oct 12 2022 at 18:15):what to?
@Jason Gross how long is fiat-crypto supposed to take these days?
Ali Caglayan (Oct 12 2022 at 18:18):Recent runs suggest 4hrs https://github.com/mit-plv/fiat-crypto/actions/runs/3213712759/jobs/5253586660
Ali Caglayan (Oct 12 2022 at 18:18):Though we are only running a subset in the CI
Jason Gross (Oct 12 2022 at 18:42):Yeah, 4h sounds about right
Gaëtan Gilbert (Oct 12 2022 at 19:06):that's kind of a lot, can we cut it down to 2h or even 1h30?
Jason Gross (Oct 13 2022 at 16:39):On GH Actions, with -j2, building fiat-crypto's deps (rewriter, bedrock2, etc) takes about 40m (62m if done with -j1), and building fiat-crypto proper takes another 1h30m (2h40m if done with -j1). validate/coqchk takes another 40m. So it seems plausible that building more of fiat-crypto with -j2 could cut it down to 1.5--2h on Coq's CI. But we stopped using -j2 because we have a couple of files that take more than 2GB RAM, and the CI runners seem memory-starved...
Maxime Dénès (Oct 13 2022 at 17:59):The current runners have 4GiB total memory
Jason Gross (Oct 14 2022 at 07:31):The heaviest files in fiat-crypto memory-wise are:
Time | Peak Mem | File Name
------------------------------------------------------------------------------------------------------------------------------------------
217m05.57s | 5261276 ko | Total Time / Peak Mem
------------------------------------------------------------------------------------------------------------------------------------------
10m12.13s | 5261276 ko | Bedrock/End2End/X25519/GarageDoor.vo
4m13.18s | 4060544 ko | Curves/EdwardsMontgomery.vo
3m13.39s | 2906972 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo
2m05.77s | 2752144 ko | /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.vo
5m25.01s | 2720684 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo
4m15.66s | 2534848 ko | Assembly/WithBedrock/Proofs.vo
1m50.34s | 2118952 ko | Fancy/Barrett256.vo
7m16.76s | 2072424 ko | Curves/Weierstrass/AffineProofs.vo
0m29.60s | 2068968 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
0m29.43s | 2068908 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
We've managed to get Bedrock/End2End/X25519/GarageDoor.vo down to just over 2GB, but the others are still there.
Last updated: Jun 05 2023 at 10:01 UTC