Stream: Coq devs & plugin devs

Topic: pipeline timeout


view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2022 at 13:53):

Yes

view this post on Zulip Gaëtan Gilbert (Oct 12 2022 at 18:15):

what to?
@Jason Gross how long is fiat-crypto supposed to take these days?

view this post on Zulip Ali Caglayan (Oct 12 2022 at 18:18):

Recent runs suggest 4hrs https://github.com/mit-plv/fiat-crypto/actions/runs/3213712759/jobs/5253586660

view this post on Zulip Ali Caglayan (Oct 12 2022 at 18:18):

Though we are only running a subset in the CI

view this post on Zulip Jason Gross (Oct 12 2022 at 18:42):

Yeah, 4h sounds about right

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Maxime Dénès (Oct 13 2022 at 17:59):

The current runners have 4GiB total memory

view this post on Zulip 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: Feb 06 2023 at 01:02 UTC