Less memory-hungry build
JasonGross opened this issue · 0 comments
JasonGross commented
It would be nice to get all files to under 2 GB so that Coq's CI could build with -j2. As of 637c7ce the most memory-hungry files 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 | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo
2m05.77s | 2752144 ko | 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
though according to
#1427 (comment) GarageDoor is down to 2332608 ko