Generate .mli files: { => Recursive} Extraction
#1292
Merged
Commits on Jun 11, 2022
-
Generate .mli files:
{ => Recursive} ExtractionThis 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>
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.