Generate .mli files: { => Recursive} Extraction
#1292
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
JasonGross
force-pushed
the
with-mli
branch
7 times, most recently
from
b306da2
to
b0a4370
Compare
This way we can hopefully avoid coq/coq#7954 In order to do this, we need to stop inlining constants in modules that are ascribed types to work around coq/coq#16169 (it might be nicer if coq/coq#16170 were solved), and then we need to work around the lack of coq/coq#11987 for `int`. Unfortunately this slows down compilation by a fair bit. No idea why. :-( <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------------------------------- 15m05.68s | 2461832 ko | Total Time / Peak Mem | 8m33.36s | 2409628 ko || +6m32.32s || 52204 ko | +76.42% | +2.16% ------------------------------------------------------------------------------------------------------------------------------------------------------------------- 0m56.38s | 2461832 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m17.08s | 2008372 ko || +0m39.30s || 453460 ko | +230.09% | +22.57% 0m54.97s | 2461708 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery | 0m16.68s | 2008104 ko || +0m38.28s || 453604 ko | +229.55% | +22.58% 0m49.48s | 2144796 ko | ExtractionOCaml/word_by_word_montgomery | 0m16.30s | 2056088 ko || +0m33.17s || 88708 ko | +203.55% | +4.31% 0m40.26s | 1861984 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m11.41s | 1342628 ko || +0m28.84s || 519356 ko | +252.84% | +38.68% 0m39.93s | 1862080 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas | 0m11.29s | 1342384 ko || +0m28.64s || 519696 ko | +253.67% | +38.71% 0m38.29s | 1667096 ko | ExtractionOCaml/unsaturated_solinas | 0m10.30s | 1291116 ko || +0m27.98s || 375980 ko | +271.74% | +29.12% 0m37.60s | 1414524 ko | ExtractionOCaml/bedrock2_base_conversion | 0m09.98s | 1161104 ko || +0m27.62s || 253420 ko | +276.75% | +21.82% 0m35.44s | 1414488 ko | ExtractionOCaml/with_bedrock2_base_conversion | 0m09.83s | 1161084 ko || +0m25.60s || 253404 ko | +260.52% | +21.82% 0m35.39s | 1619444 ko | ExtractionOCaml/with_bedrock2_saturated_solinas | 0m09.78s | 1166256 ko || +0m25.60s || 453188 ko | +261.86% | +38.85% 0m35.30s | 1618712 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m09.75s | 1166292 ko || +0m25.54s || 452420 ko | +262.05% | +38.79% 0m33.21s | 1323400 ko | ExtractionOCaml/base_conversion | 0m09.14s | 1138648 ko || +0m24.07s || 184752 ko | +263.34% | +16.22% 0m32.94s | 1328028 ko | ExtractionOCaml/saturated_solinas | 0m09.20s | 1150352 ko || +0m23.73s || 177676 ko | +258.04% | +15.44% 0m30.84s | 1393964 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m08.47s | 1097264 ko || +0m22.36s || 296700 ko | +264.10% | +27.03% 0m27.81s | 1165240 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m07.83s | 967424 ko || +0m19.97s || 197816 ko | +255.17% | +20.44% 0m38.49s | 2132484 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml | 0m39.99s | 2409620 ko || -0m01.50s || -277136 ko | -3.75% | -11.50% 0m39.84s | 2132172 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m40.29s | 2409628 ko || -0m00.44s || -277456 ko | -1.11% | -11.51% 0m38.14s | 2031924 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m38.52s | 2283124 ko || -0m00.38s || -251200 ko | -0.98% | -11.00% 0m25.52s | 1641504 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml | 0m25.72s | 1807892 ko || -0m00.19s || -166388 ko | -0.77% | -9.20% 0m25.50s | 1641432 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m25.75s | 1807716 ko || -0m00.25s || -166284 ko | -0.97% | -9.19% 0m24.22s | 1563220 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m24.27s | 1708016 ko || -0m00.05s || -144796 ko | -0.20% | -8.47% 0m21.63s | 1562204 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m21.53s | 1716916 ko || +0m00.09s || -154712 ko | +0.46% | -9.01% 0m21.59s | 1562396 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml | 0m21.42s | 1716720 ko || +0m00.16s || -154324 ko | +0.79% | -8.98% 0m21.34s | 1562540 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m21.44s | 1714560 ko || -0m00.10s || -152020 ko | -0.46% | -8.86% 0m21.29s | 1562432 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml | 0m21.45s | 1714660 ko || -0m00.16s || -152228 ko | -0.74% | -8.87% 0m20.01s | 1503752 ko | ExtractionOCaml/saturated_solinas.ml | 0m19.04s | 1652768 ko || +0m00.97s || -149016 ko | +5.09% | -9.01% 0m19.85s | 1498708 ko | ExtractionOCaml/base_conversion.ml | 0m20.02s | 1647208 ko || -0m00.16s || -148500 ko | -0.84% | -9.01% 0m17.36s | 1491612 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m17.50s | 1825596 ko || -0m00.14s || -333984 ko | -0.80% | -18.29% 0m16.83s | 1423236 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m16.25s | 1779200 ko || +0m00.57s || -355964 ko | +3.56% | -20.00% 0m01.17s | 734920 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m01.18s | 735024 ko || -0m00.01s || -104 ko | -0.84% | -0.01% 0m01.08s | 746772 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m01.11s | 746688 ko || -0m00.03s || 84 ko | -2.70% | +0.01% 0m00.79s | 711948 ko | StandaloneOCamlMain.vo | 0m00.84s | 712080 ko || -0m00.04s || -132 ko | -5.95% | -0.01% 0m00.27s | 72544 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | N/A | N/A || +0m00.27s || 72544 ko | ∞ | ∞ 0m00.26s | 72320 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi | N/A | N/A || +0m00.26s || 72320 ko | ∞ | ∞ 0m00.25s | 72052 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi | N/A | N/A || +0m00.25s || 72052 ko | ∞ | ∞ 0m00.24s | 71844 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | N/A | N/A || +0m00.24s || 71844 ko | ∞ | ∞ 0m00.24s | 70448 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi | N/A | N/A || +0m00.24s || 70448 ko | ∞ | ∞ 0m00.23s | 70548 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | N/A | N/A || +0m00.23s || 70548 ko | ∞ | ∞ 0m00.23s | 70080 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | N/A | N/A || +0m00.23s || 70080 ko | ∞ | ∞ 0m00.23s | 69924 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi | N/A | N/A || +0m00.23s || 69924 ko | ∞ | ∞ 0m00.23s | 68380 ko | ExtractionOCaml/word_by_word_montgomery.cmi | N/A | N/A || +0m00.23s || 68380 ko | ∞ | ∞ 0m00.22s | 68028 ko | ExtractionOCaml/base_conversion.cmi | N/A | N/A || +0m00.22s || 68028 ko | ∞ | ∞ 0m00.22s | 66700 ko | ExtractionOCaml/saturated_solinas.cmi | N/A | N/A || +0m00.22s || 66700 ko | ∞ | ∞ 0m00.22s | 69916 ko | ExtractionOCaml/unsaturated_solinas.cmi | N/A | N/A || +0m00.22s || 69916 ko | ∞ | ∞ 0m00.20s | 60336 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | N/A | N/A || +0m00.20s || 60336 ko | ∞ | ∞ 0m00.16s | 59532 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | N/A | N/A || +0m00.16s || 59532 ko | ∞ | ∞ ``` </p> </details>
JasonGross
added a commit
to JasonGross/fiat-crypto
that referenced
this pull request
Jun 12, 2022
…)" This reverts commit d9f123f It did not work for fixing the extraction, so no need to slow down compilation.
JasonGross
added a commit
to JasonGross/fiat-crypto
that referenced
this pull request
Oct 2, 2022
Since d9f123f (mit-plv#1292) we've been using `Int.t` to work around a lack of coq/coq#11987. The `Int` module was added in OCaml 4.08. Dropping support for older OCaml is not such a big loss, as Coq 8.16 will require OCaml >= 4.09, (8.15 allows >= 4.05), Debian stable has 4.11, and Ubuntu LTS has 4.13 (even the old Ubuntu LTS has 4.08).
JasonGross
added a commit
that referenced
this pull request
Oct 2, 2022
Since d9f123f (#1292) we've been using `Int.t` to work around a lack of coq/coq#11987. The `Int` module was added in OCaml 4.08. Dropping support for older OCaml is not such a big loss, as Coq 8.16 will require OCaml >= 4.09, (8.15 allows >= 4.05), Debian stable has 4.11, and Ubuntu LTS has 4.13 (even the old Ubuntu LTS has 4.08).
OwenConoly
pushed a commit
that referenced
this pull request
Nov 13, 2022
Since d9f123f (#1292) we've been using `Int.t` to work around a lack of coq/coq#11987. The `Int` module was added in OCaml 4.08. Dropping support for older OCaml is not such a big loss, as Coq 8.16 will require OCaml >= 4.09, (8.15 allows >= 4.05), Debian stable has 4.11, and Ubuntu LTS has 4.13 (even the old Ubuntu LTS has 4.08).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This way we can hopefully avoid coq/coq#7954
Timing data coming soon