Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generate single binary for all synthesis #1724

Closed
JasonGross opened this issue Nov 13, 2023 · 0 comments · Fixed by #1730
Closed

Generate single binary for all synthesis #1724

JasonGross opened this issue Nov 13, 2023 · 0 comments · Fixed by #1730

Comments

@JasonGross
Copy link
Collaborator

It would be nice to be able to call something like synthesize word-by-word-montgomery args or fiat-cryptography word-by-word-montgomery args or whatever, instead of having separate binaries for each synthesis pipeline. To do this, I think we should add another module below

fiat-crypto/src/CLI.v

Lines 1333 to 1339 in dcd5678

Definition PipelineMain
{supported_languages : supported_languagesT}
{A}
{io_driver : IODriverAPI A}
(argv : list string)
: A
:= Parameterized.PipelineMain argv.

that contains a main function that reads argv into prog::kind::args, checks to see if kind is one of the recognized kinds and delegates to the relevant main method if so, and otherwise printing out USAGE: $0 <possible options>. Presumably we can reuse the infrastructure for parsing output languages to parse the possible kinds. parse_argv might need to be generalized to take an implicit argument of how many arguments to ignore for the program name, or else we'll have to adjust the quoting at https://github.com/mit-plv/fiat-crypto/blob/dcd567854191ad4e1abd293ddecd2a8df1048d8d/src/CLI.v#L1015C19-L1015C19

We can then replace

Definition main_gen
{supported_languages : ForExtraction.supported_languagesT}
(PipelineMain : forall (A := _)
(argv : list String.string),
A)
: IO_unit
:= cast_io
(argv <- getArgs;
prog <- getProgName;
PipelineMain
(prog::argv)).

and
Definition main_gen
{supported_languages : ForExtraction.supported_languagesT}
(PipelineMain : forall (A := _)
(argv : list String.string),
A)
: unit
:= let argv := List.map string_to_Coq_string sys_argv in
PipelineMain argv.

with a single main function (for #1720 we'll probably want first a function that specializes to all of the language-specific calls, and then finally something that passes in Sys.argv? Or we can just have a separate StandaloneJSofOCaml that implements all the language-specific stuff separately?).

JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
@JasonGross JasonGross mentioned this issue Nov 14, 2023
6 tasks
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
Fixes mit-plv#1724

<details><summary>Timing Diff</summary>
<p>

```
     Time |   Peak Mem | File Name
----------------------------------------------------------------------------------
53m02.47s | 2463008 ko | Total Time / Peak Mem
----------------------------------------------------------------------------------
 2m21.70s | 2462928 ko | ExtractionOCaml/fiat_crypto
 2m19.85s | 2463008 ko | ExtractionOCaml/bedrock2_fiat_crypto
 1m53.82s | 1863716 ko | ExtractionOCaml/solinas_reduction
 1m36.75s | 2462904 ko | ExtractionOCaml/with_bedrock2_fiat_crypto
 1m33.30s | 2316820 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml
 1m30.98s | 2300660 ko | ExtractionOCaml/fiat_crypto.ml
 1m30.25s | 2075840 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
 1m26.51s | 2074640 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
 1m25.26s | 1829432 ko | ExtractionOCaml/word_by_word_montgomery
 1m22.38s | 1780504 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
 1m20.72s | 2147524 ko | ExtractionOCaml/bedrock2_solinas_reduction
 1m20.62s | 2336764 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml
 1m18.57s | 1416332 ko | ExtractionOCaml/with_bedrock2_base_conversion
 1m16.74s | 1469000 ko | ExtractionOCaml/bedrock2_dettman_multiplication
 1m14.80s | 1780196 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
 1m14.67s | 1415232 ko | ExtractionOCaml/base_conversion
 1m08.91s | 1416276 ko | ExtractionOCaml/bedrock2_base_conversion
 1m08.90s | 1415436 ko | ExtractionOCaml/dettman_multiplication
 1m07.90s | 1415368 ko | ExtractionOCaml/saturated_solinas
 1m07.63s | 1525784 ko | ExtractionOCaml/unsaturated_solinas
 1m07.23s | 1449720 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication
 1m07.09s | 1447196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
 1m07.02s | 1439752 ko | ExtractionOCaml/bedrock2_saturated_solinas
 1m06.29s | 1448860 ko | ExtractionOCaml/with_bedrock2_solinas_reduction
 1m05.35s | 2190452 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml
 1m03.87s | 2137192 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
 1m01.18s | 2137308 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
 0m58.53s | 2057100 ko | ExtractionOCaml/solinas_reduction.ml
 0m56.27s | 2063328 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
 0m55.76s | 1836424 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
 0m55.38s | 2030208 ko | ExtractionOCaml/word_by_word_montgomery.ml
 0m52.90s | 1413320 ko | ExtractionOCaml/perf_unsaturated_solinas
 0m51.44s | 2063536 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
 0m51.16s | 1950720 ko | ExtractionOCaml/bedrock2_base_conversion.ml
 0m50.96s | 1989736 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml
 0m49.61s | 1936244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml
 0m49.39s | 1936412 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
 0m49.38s | 1753040 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
 0m48.72s | 1938204 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml
 0m48.29s | 1952524 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
 0m48.16s | 1938444 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
 0m47.28s | 1962520 ko | ExtractionOCaml/unsaturated_solinas.ml
 0m46.15s | 1823484 ko | ExtractionOCaml/base_conversion.ml
 0m42.74s | 1413036 ko | ExtractionOCaml/perf_word_by_word_montgomery
 0m41.95s | 1882704 ko | ExtractionOCaml/dettman_multiplication.ml
 0m38.36s | 1846056 ko | ExtractionOCaml/saturated_solinas.ml
 0m04.57s | 1035968 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
 0m00.93s |  106556 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
 0m00.90s |  102844 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi
 0m00.89s |  103608 ko | ExtractionOCaml/dettman_multiplication.cmi
 0m00.87s |  105352 ko | ExtractionOCaml/unsaturated_solinas.cmi
 0m00.84s |  102728 ko | ExtractionOCaml/fiat_crypto.cmi
 0m00.83s |  103608 ko | ExtractionOCaml/saturated_solinas.cmi
 0m00.83s |  103844 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi
 0m00.81s |  102720 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
 0m00.80s |  103684 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
 0m00.76s |  102640 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi
 0m00.76s |  107620 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
 0m00.75s |  102300 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi
 0m00.75s |  103592 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
 0m00.75s |  102900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
 0m00.74s |  102780 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
 0m00.72s |  103088 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
 0m00.71s |  105644 ko | ExtractionOCaml/word_by_word_montgomery.cmi
 0m00.70s |  103272 ko | ExtractionOCaml/base_conversion.cmi
 0m00.69s |  103100 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi
 0m00.67s |  102580 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi
 0m00.67s |  103236 ko | ExtractionOCaml/solinas_reduction.cmi
 0m00.42s |   58808 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi
 0m00.39s |   60084 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi

```
</p>
</details>
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 14, 2023
Fixes mit-plv#1724

Note that we keep the non-unified binaries (and use them to build
generated files) to avoid OOMs on Coq's CI.

It's unfortunate that compilation is so slow here, taking almost an hour
on my machine just to extract and compile the various binaries.

<details><summary>Timing Diff</summary>
<p>

```
     Time |   Peak Mem | File Name
----------------------------------------------------------------------------------
53m02.47s | 2463008 ko | Total Time / Peak Mem
----------------------------------------------------------------------------------
 2m21.70s | 2462928 ko | ExtractionOCaml/fiat_crypto
 2m19.85s | 2463008 ko | ExtractionOCaml/bedrock2_fiat_crypto
 1m53.82s | 1863716 ko | ExtractionOCaml/solinas_reduction
 1m36.75s | 2462904 ko | ExtractionOCaml/with_bedrock2_fiat_crypto
 1m33.30s | 2316820 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml
 1m30.98s | 2300660 ko | ExtractionOCaml/fiat_crypto.ml
 1m30.25s | 2075840 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
 1m26.51s | 2074640 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
 1m25.26s | 1829432 ko | ExtractionOCaml/word_by_word_montgomery
 1m22.38s | 1780504 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
 1m20.72s | 2147524 ko | ExtractionOCaml/bedrock2_solinas_reduction
 1m20.62s | 2336764 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml
 1m18.57s | 1416332 ko | ExtractionOCaml/with_bedrock2_base_conversion
 1m16.74s | 1469000 ko | ExtractionOCaml/bedrock2_dettman_multiplication
 1m14.80s | 1780196 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
 1m14.67s | 1415232 ko | ExtractionOCaml/base_conversion
 1m08.91s | 1416276 ko | ExtractionOCaml/bedrock2_base_conversion
 1m08.90s | 1415436 ko | ExtractionOCaml/dettman_multiplication
 1m07.90s | 1415368 ko | ExtractionOCaml/saturated_solinas
 1m07.63s | 1525784 ko | ExtractionOCaml/unsaturated_solinas
 1m07.23s | 1449720 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication
 1m07.09s | 1447196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
 1m07.02s | 1439752 ko | ExtractionOCaml/bedrock2_saturated_solinas
 1m06.29s | 1448860 ko | ExtractionOCaml/with_bedrock2_solinas_reduction
 1m05.35s | 2190452 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml
 1m03.87s | 2137192 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
 1m01.18s | 2137308 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
 0m58.53s | 2057100 ko | ExtractionOCaml/solinas_reduction.ml
 0m56.27s | 2063328 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
 0m55.76s | 1836424 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
 0m55.38s | 2030208 ko | ExtractionOCaml/word_by_word_montgomery.ml
 0m52.90s | 1413320 ko | ExtractionOCaml/perf_unsaturated_solinas
 0m51.44s | 2063536 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
 0m51.16s | 1950720 ko | ExtractionOCaml/bedrock2_base_conversion.ml
 0m50.96s | 1989736 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml
 0m49.61s | 1936244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml
 0m49.39s | 1936412 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
 0m49.38s | 1753040 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
 0m48.72s | 1938204 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml
 0m48.29s | 1952524 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
 0m48.16s | 1938444 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
 0m47.28s | 1962520 ko | ExtractionOCaml/unsaturated_solinas.ml
 0m46.15s | 1823484 ko | ExtractionOCaml/base_conversion.ml
 0m42.74s | 1413036 ko | ExtractionOCaml/perf_word_by_word_montgomery
 0m41.95s | 1882704 ko | ExtractionOCaml/dettman_multiplication.ml
 0m38.36s | 1846056 ko | ExtractionOCaml/saturated_solinas.ml
 0m04.57s | 1035968 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
 0m00.93s |  106556 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
 0m00.90s |  102844 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi
 0m00.89s |  103608 ko | ExtractionOCaml/dettman_multiplication.cmi
 0m00.87s |  105352 ko | ExtractionOCaml/unsaturated_solinas.cmi
 0m00.84s |  102728 ko | ExtractionOCaml/fiat_crypto.cmi
 0m00.83s |  103608 ko | ExtractionOCaml/saturated_solinas.cmi
 0m00.83s |  103844 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi
 0m00.81s |  102720 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
 0m00.80s |  103684 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
 0m00.76s |  102640 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi
 0m00.76s |  107620 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
 0m00.75s |  102300 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi
 0m00.75s |  103592 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
 0m00.75s |  102900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
 0m00.74s |  102780 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
 0m00.72s |  103088 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
 0m00.71s |  105644 ko | ExtractionOCaml/word_by_word_montgomery.cmi
 0m00.70s |  103272 ko | ExtractionOCaml/base_conversion.cmi
 0m00.69s |  103100 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi
 0m00.67s |  102580 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi
 0m00.67s |  103236 ko | ExtractionOCaml/solinas_reduction.cmi
 0m00.42s |   58808 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi
 0m00.39s |   60084 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi

```
</p>
</details>
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 15, 2023
Fixes mit-plv#1724

Note that we keep the non-unified binaries (and use them to build
generated files) to avoid OOMs on Coq's CI.

It's unfortunate that compilation is so slow here, taking almost an hour
on my machine just to extract and compile the various binaries.

<details><summary>Timing Diff</summary>
<p>

```
     Time |   Peak Mem | File Name
----------------------------------------------------------------------------------
53m02.47s | 2463008 ko | Total Time / Peak Mem
----------------------------------------------------------------------------------
 2m21.70s | 2462928 ko | ExtractionOCaml/fiat_crypto
 2m19.85s | 2463008 ko | ExtractionOCaml/bedrock2_fiat_crypto
 1m53.82s | 1863716 ko | ExtractionOCaml/solinas_reduction
 1m36.75s | 2462904 ko | ExtractionOCaml/with_bedrock2_fiat_crypto
 1m33.30s | 2316820 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml
 1m30.98s | 2300660 ko | ExtractionOCaml/fiat_crypto.ml
 1m30.25s | 2075840 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
 1m26.51s | 2074640 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
 1m25.26s | 1829432 ko | ExtractionOCaml/word_by_word_montgomery
 1m22.38s | 1780504 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
 1m20.72s | 2147524 ko | ExtractionOCaml/bedrock2_solinas_reduction
 1m20.62s | 2336764 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml
 1m18.57s | 1416332 ko | ExtractionOCaml/with_bedrock2_base_conversion
 1m16.74s | 1469000 ko | ExtractionOCaml/bedrock2_dettman_multiplication
 1m14.80s | 1780196 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
 1m14.67s | 1415232 ko | ExtractionOCaml/base_conversion
 1m08.91s | 1416276 ko | ExtractionOCaml/bedrock2_base_conversion
 1m08.90s | 1415436 ko | ExtractionOCaml/dettman_multiplication
 1m07.90s | 1415368 ko | ExtractionOCaml/saturated_solinas
 1m07.63s | 1525784 ko | ExtractionOCaml/unsaturated_solinas
 1m07.23s | 1449720 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication
 1m07.09s | 1447196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
 1m07.02s | 1439752 ko | ExtractionOCaml/bedrock2_saturated_solinas
 1m06.29s | 1448860 ko | ExtractionOCaml/with_bedrock2_solinas_reduction
 1m05.35s | 2190452 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml
 1m03.87s | 2137192 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
 1m01.18s | 2137308 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
 0m58.53s | 2057100 ko | ExtractionOCaml/solinas_reduction.ml
 0m56.27s | 2063328 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
 0m55.76s | 1836424 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
 0m55.38s | 2030208 ko | ExtractionOCaml/word_by_word_montgomery.ml
 0m52.90s | 1413320 ko | ExtractionOCaml/perf_unsaturated_solinas
 0m51.44s | 2063536 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
 0m51.16s | 1950720 ko | ExtractionOCaml/bedrock2_base_conversion.ml
 0m50.96s | 1989736 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml
 0m49.61s | 1936244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml
 0m49.39s | 1936412 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
 0m49.38s | 1753040 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
 0m48.72s | 1938204 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml
 0m48.29s | 1952524 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
 0m48.16s | 1938444 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
 0m47.28s | 1962520 ko | ExtractionOCaml/unsaturated_solinas.ml
 0m46.15s | 1823484 ko | ExtractionOCaml/base_conversion.ml
 0m42.74s | 1413036 ko | ExtractionOCaml/perf_word_by_word_montgomery
 0m41.95s | 1882704 ko | ExtractionOCaml/dettman_multiplication.ml
 0m38.36s | 1846056 ko | ExtractionOCaml/saturated_solinas.ml
 0m04.57s | 1035968 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
 0m00.93s |  106556 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
 0m00.90s |  102844 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi
 0m00.89s |  103608 ko | ExtractionOCaml/dettman_multiplication.cmi
 0m00.87s |  105352 ko | ExtractionOCaml/unsaturated_solinas.cmi
 0m00.84s |  102728 ko | ExtractionOCaml/fiat_crypto.cmi
 0m00.83s |  103608 ko | ExtractionOCaml/saturated_solinas.cmi
 0m00.83s |  103844 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi
 0m00.81s |  102720 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
 0m00.80s |  103684 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
 0m00.76s |  102640 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi
 0m00.76s |  107620 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
 0m00.75s |  102300 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi
 0m00.75s |  103592 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
 0m00.75s |  102900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
 0m00.74s |  102780 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
 0m00.72s |  103088 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
 0m00.71s |  105644 ko | ExtractionOCaml/word_by_word_montgomery.cmi
 0m00.70s |  103272 ko | ExtractionOCaml/base_conversion.cmi
 0m00.69s |  103100 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi
 0m00.67s |  102580 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi
 0m00.67s |  103236 ko | ExtractionOCaml/solinas_reduction.cmi
 0m00.42s |   58808 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi
 0m00.39s |   60084 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi

```
</p>
</details>
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 15, 2023
Fixes mit-plv#1724

Note that we keep the non-unified binaries (and use them to build
generated files) to avoid OOMs on Coq's CI.

It's unfortunate that compilation is so slow here, taking almost an hour
on my machine just to extract and compile the various binaries.

<details><summary>Timing Diff</summary>
<p>

```
     Time |   Peak Mem | File Name
----------------------------------------------------------------------------------
53m02.47s | 2463008 ko | Total Time / Peak Mem
----------------------------------------------------------------------------------
 2m21.70s | 2462928 ko | ExtractionOCaml/fiat_crypto
 2m19.85s | 2463008 ko | ExtractionOCaml/bedrock2_fiat_crypto
 1m53.82s | 1863716 ko | ExtractionOCaml/solinas_reduction
 1m36.75s | 2462904 ko | ExtractionOCaml/with_bedrock2_fiat_crypto
 1m33.30s | 2316820 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml
 1m30.98s | 2300660 ko | ExtractionOCaml/fiat_crypto.ml
 1m30.25s | 2075840 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
 1m26.51s | 2074640 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
 1m25.26s | 1829432 ko | ExtractionOCaml/word_by_word_montgomery
 1m22.38s | 1780504 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
 1m20.72s | 2147524 ko | ExtractionOCaml/bedrock2_solinas_reduction
 1m20.62s | 2336764 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml
 1m18.57s | 1416332 ko | ExtractionOCaml/with_bedrock2_base_conversion
 1m16.74s | 1469000 ko | ExtractionOCaml/bedrock2_dettman_multiplication
 1m14.80s | 1780196 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
 1m14.67s | 1415232 ko | ExtractionOCaml/base_conversion
 1m08.91s | 1416276 ko | ExtractionOCaml/bedrock2_base_conversion
 1m08.90s | 1415436 ko | ExtractionOCaml/dettman_multiplication
 1m07.90s | 1415368 ko | ExtractionOCaml/saturated_solinas
 1m07.63s | 1525784 ko | ExtractionOCaml/unsaturated_solinas
 1m07.23s | 1449720 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication
 1m07.09s | 1447196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
 1m07.02s | 1439752 ko | ExtractionOCaml/bedrock2_saturated_solinas
 1m06.29s | 1448860 ko | ExtractionOCaml/with_bedrock2_solinas_reduction
 1m05.35s | 2190452 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml
 1m03.87s | 2137192 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
 1m01.18s | 2137308 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
 0m58.53s | 2057100 ko | ExtractionOCaml/solinas_reduction.ml
 0m56.27s | 2063328 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
 0m55.76s | 1836424 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
 0m55.38s | 2030208 ko | ExtractionOCaml/word_by_word_montgomery.ml
 0m52.90s | 1413320 ko | ExtractionOCaml/perf_unsaturated_solinas
 0m51.44s | 2063536 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
 0m51.16s | 1950720 ko | ExtractionOCaml/bedrock2_base_conversion.ml
 0m50.96s | 1989736 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml
 0m49.61s | 1936244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml
 0m49.39s | 1936412 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
 0m49.38s | 1753040 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
 0m48.72s | 1938204 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml
 0m48.29s | 1952524 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
 0m48.16s | 1938444 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
 0m47.28s | 1962520 ko | ExtractionOCaml/unsaturated_solinas.ml
 0m46.15s | 1823484 ko | ExtractionOCaml/base_conversion.ml
 0m42.74s | 1413036 ko | ExtractionOCaml/perf_word_by_word_montgomery
 0m41.95s | 1882704 ko | ExtractionOCaml/dettman_multiplication.ml
 0m38.36s | 1846056 ko | ExtractionOCaml/saturated_solinas.ml
 0m04.57s | 1035968 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
 0m00.93s |  106556 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
 0m00.90s |  102844 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi
 0m00.89s |  103608 ko | ExtractionOCaml/dettman_multiplication.cmi
 0m00.87s |  105352 ko | ExtractionOCaml/unsaturated_solinas.cmi
 0m00.84s |  102728 ko | ExtractionOCaml/fiat_crypto.cmi
 0m00.83s |  103608 ko | ExtractionOCaml/saturated_solinas.cmi
 0m00.83s |  103844 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi
 0m00.81s |  102720 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
 0m00.80s |  103684 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
 0m00.76s |  102640 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi
 0m00.76s |  107620 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
 0m00.75s |  102300 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi
 0m00.75s |  103592 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
 0m00.75s |  102900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
 0m00.74s |  102780 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
 0m00.72s |  103088 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
 0m00.71s |  105644 ko | ExtractionOCaml/word_by_word_montgomery.cmi
 0m00.70s |  103272 ko | ExtractionOCaml/base_conversion.cmi
 0m00.69s |  103100 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi
 0m00.67s |  102580 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi
 0m00.67s |  103236 ko | ExtractionOCaml/solinas_reduction.cmi
 0m00.42s |   58808 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi
 0m00.39s |   60084 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi

```
</p>
</details>
JasonGross added a commit to JasonGross/fiat-crypto that referenced this issue Nov 15, 2023
Fixes mit-plv#1724

Note that we keep the non-unified binaries (and use them to build
generated files) to avoid OOMs on Coq's CI.

It's unfortunate that compilation is so slow here, taking almost an hour
on my machine just to extract and compile the various binaries.

<details><summary>Timing Diff</summary>
<p>

```
     Time |   Peak Mem | File Name
----------------------------------------------------------------------------------
53m02.47s | 2463008 ko | Total Time / Peak Mem
----------------------------------------------------------------------------------
 2m21.70s | 2462928 ko | ExtractionOCaml/fiat_crypto
 2m19.85s | 2463008 ko | ExtractionOCaml/bedrock2_fiat_crypto
 1m53.82s | 1863716 ko | ExtractionOCaml/solinas_reduction
 1m36.75s | 2462904 ko | ExtractionOCaml/with_bedrock2_fiat_crypto
 1m33.30s | 2316820 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml
 1m30.98s | 2300660 ko | ExtractionOCaml/fiat_crypto.ml
 1m30.25s | 2075840 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
 1m26.51s | 2074640 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
 1m25.26s | 1829432 ko | ExtractionOCaml/word_by_word_montgomery
 1m22.38s | 1780504 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
 1m20.72s | 2147524 ko | ExtractionOCaml/bedrock2_solinas_reduction
 1m20.62s | 2336764 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml
 1m18.57s | 1416332 ko | ExtractionOCaml/with_bedrock2_base_conversion
 1m16.74s | 1469000 ko | ExtractionOCaml/bedrock2_dettman_multiplication
 1m14.80s | 1780196 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
 1m14.67s | 1415232 ko | ExtractionOCaml/base_conversion
 1m08.91s | 1416276 ko | ExtractionOCaml/bedrock2_base_conversion
 1m08.90s | 1415436 ko | ExtractionOCaml/dettman_multiplication
 1m07.90s | 1415368 ko | ExtractionOCaml/saturated_solinas
 1m07.63s | 1525784 ko | ExtractionOCaml/unsaturated_solinas
 1m07.23s | 1449720 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication
 1m07.09s | 1447196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
 1m07.02s | 1439752 ko | ExtractionOCaml/bedrock2_saturated_solinas
 1m06.29s | 1448860 ko | ExtractionOCaml/with_bedrock2_solinas_reduction
 1m05.35s | 2190452 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml
 1m03.87s | 2137192 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
 1m01.18s | 2137308 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
 0m58.53s | 2057100 ko | ExtractionOCaml/solinas_reduction.ml
 0m56.27s | 2063328 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
 0m55.76s | 1836424 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
 0m55.38s | 2030208 ko | ExtractionOCaml/word_by_word_montgomery.ml
 0m52.90s | 1413320 ko | ExtractionOCaml/perf_unsaturated_solinas
 0m51.44s | 2063536 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
 0m51.16s | 1950720 ko | ExtractionOCaml/bedrock2_base_conversion.ml
 0m50.96s | 1989736 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml
 0m49.61s | 1936244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml
 0m49.39s | 1936412 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
 0m49.38s | 1753040 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
 0m48.72s | 1938204 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml
 0m48.29s | 1952524 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
 0m48.16s | 1938444 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
 0m47.28s | 1962520 ko | ExtractionOCaml/unsaturated_solinas.ml
 0m46.15s | 1823484 ko | ExtractionOCaml/base_conversion.ml
 0m42.74s | 1413036 ko | ExtractionOCaml/perf_word_by_word_montgomery
 0m41.95s | 1882704 ko | ExtractionOCaml/dettman_multiplication.ml
 0m38.36s | 1846056 ko | ExtractionOCaml/saturated_solinas.ml
 0m04.57s | 1035968 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
 0m00.93s |  106556 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
 0m00.90s |  102844 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi
 0m00.89s |  103608 ko | ExtractionOCaml/dettman_multiplication.cmi
 0m00.87s |  105352 ko | ExtractionOCaml/unsaturated_solinas.cmi
 0m00.84s |  102728 ko | ExtractionOCaml/fiat_crypto.cmi
 0m00.83s |  103608 ko | ExtractionOCaml/saturated_solinas.cmi
 0m00.83s |  103844 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi
 0m00.81s |  102720 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
 0m00.80s |  103684 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
 0m00.76s |  102640 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi
 0m00.76s |  107620 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
 0m00.75s |  102300 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi
 0m00.75s |  103592 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
 0m00.75s |  102900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
 0m00.74s |  102780 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
 0m00.72s |  103088 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
 0m00.71s |  105644 ko | ExtractionOCaml/word_by_word_montgomery.cmi
 0m00.70s |  103272 ko | ExtractionOCaml/base_conversion.cmi
 0m00.69s |  103100 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi
 0m00.67s |  102580 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi
 0m00.67s |  103236 ko | ExtractionOCaml/solinas_reduction.cmi
 0m00.42s |   58808 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi
 0m00.39s |   60084 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi

```
</p>
</details>
JasonGross added a commit that referenced this issue Nov 15, 2023
Fixes #1724

Note that we keep the non-unified binaries (and use them to build
generated files) to avoid OOMs on Coq's CI.

It's unfortunate that compilation is so slow here, taking almost an hour
on my machine just to extract and compile the various binaries.

<details><summary>Timing Diff</summary>
<p>

```
     Time |   Peak Mem | File Name
----------------------------------------------------------------------------------
53m02.47s | 2463008 ko | Total Time / Peak Mem
----------------------------------------------------------------------------------
 2m21.70s | 2462928 ko | ExtractionOCaml/fiat_crypto
 2m19.85s | 2463008 ko | ExtractionOCaml/bedrock2_fiat_crypto
 1m53.82s | 1863716 ko | ExtractionOCaml/solinas_reduction
 1m36.75s | 2462904 ko | ExtractionOCaml/with_bedrock2_fiat_crypto
 1m33.30s | 2316820 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml
 1m30.98s | 2300660 ko | ExtractionOCaml/fiat_crypto.ml
 1m30.25s | 2075840 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
 1m26.51s | 2074640 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
 1m25.26s | 1829432 ko | ExtractionOCaml/word_by_word_montgomery
 1m22.38s | 1780504 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
 1m20.72s | 2147524 ko | ExtractionOCaml/bedrock2_solinas_reduction
 1m20.62s | 2336764 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml
 1m18.57s | 1416332 ko | ExtractionOCaml/with_bedrock2_base_conversion
 1m16.74s | 1469000 ko | ExtractionOCaml/bedrock2_dettman_multiplication
 1m14.80s | 1780196 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
 1m14.67s | 1415232 ko | ExtractionOCaml/base_conversion
 1m08.91s | 1416276 ko | ExtractionOCaml/bedrock2_base_conversion
 1m08.90s | 1415436 ko | ExtractionOCaml/dettman_multiplication
 1m07.90s | 1415368 ko | ExtractionOCaml/saturated_solinas
 1m07.63s | 1525784 ko | ExtractionOCaml/unsaturated_solinas
 1m07.23s | 1449720 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication
 1m07.09s | 1447196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
 1m07.02s | 1439752 ko | ExtractionOCaml/bedrock2_saturated_solinas
 1m06.29s | 1448860 ko | ExtractionOCaml/with_bedrock2_solinas_reduction
 1m05.35s | 2190452 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml
 1m03.87s | 2137192 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
 1m01.18s | 2137308 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
 0m58.53s | 2057100 ko | ExtractionOCaml/solinas_reduction.ml
 0m56.27s | 2063328 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
 0m55.76s | 1836424 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
 0m55.38s | 2030208 ko | ExtractionOCaml/word_by_word_montgomery.ml
 0m52.90s | 1413320 ko | ExtractionOCaml/perf_unsaturated_solinas
 0m51.44s | 2063536 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
 0m51.16s | 1950720 ko | ExtractionOCaml/bedrock2_base_conversion.ml
 0m50.96s | 1989736 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml
 0m49.61s | 1936244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml
 0m49.39s | 1936412 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
 0m49.38s | 1753040 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
 0m48.72s | 1938204 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml
 0m48.29s | 1952524 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
 0m48.16s | 1938444 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
 0m47.28s | 1962520 ko | ExtractionOCaml/unsaturated_solinas.ml
 0m46.15s | 1823484 ko | ExtractionOCaml/base_conversion.ml
 0m42.74s | 1413036 ko | ExtractionOCaml/perf_word_by_word_montgomery
 0m41.95s | 1882704 ko | ExtractionOCaml/dettman_multiplication.ml
 0m38.36s | 1846056 ko | ExtractionOCaml/saturated_solinas.ml
 0m04.57s | 1035968 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
 0m00.93s |  106556 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
 0m00.90s |  102844 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi
 0m00.89s |  103608 ko | ExtractionOCaml/dettman_multiplication.cmi
 0m00.87s |  105352 ko | ExtractionOCaml/unsaturated_solinas.cmi
 0m00.84s |  102728 ko | ExtractionOCaml/fiat_crypto.cmi
 0m00.83s |  103608 ko | ExtractionOCaml/saturated_solinas.cmi
 0m00.83s |  103844 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi
 0m00.81s |  102720 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
 0m00.80s |  103684 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
 0m00.76s |  102640 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi
 0m00.76s |  107620 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
 0m00.75s |  102300 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi
 0m00.75s |  103592 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
 0m00.75s |  102900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
 0m00.74s |  102780 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
 0m00.72s |  103088 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
 0m00.71s |  105644 ko | ExtractionOCaml/word_by_word_montgomery.cmi
 0m00.70s |  103272 ko | ExtractionOCaml/base_conversion.cmi
 0m00.69s |  103100 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi
 0m00.67s |  102580 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi
 0m00.67s |  103236 ko | ExtractionOCaml/solinas_reduction.cmi
 0m00.42s |   58808 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi
 0m00.39s |   60084 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi

```
</p>
</details>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
Development

Successfully merging a pull request may close this issue.

1 participant