diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-04-09 21:27:59 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-04-12 20:53:24 -0400 |
| commit | 1384a29170bbb8b166b90f73bafea8d1948568af (patch) | |
| tree | 71155a0b5501cd136c888255cb26164438521507 /src/Util/Bool/Reflect.v | |
| parent | f626f41c8c5df7eb4131d16f8cc6e05140fd509c (diff) | |
Replace the python script with Ltac code
We now rely on Ltac rather than python to generate the raw identifiers.
After | File Name | Before || Change | % Change
-----------------------------------------------------------------------------------------------
22m05.90s | Total | 21m51.87s || +0m14.03s | +1.07%
-----------------------------------------------------------------------------------------------
0m49.25s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m55.23s || -0m05.97s | -10.82%
0m19.14s | GENERATEDIdentifiersWithoutTypes.vo | 0m13.35s || +0m05.79s | +43.37%
0m36.52s | ExtractionHaskell/saturated_solinas | 0m32.60s || +0m03.92s | +12.02%
0m24.00s | SlowPrimeSynthesisExamples.vo | 0m27.22s || -0m03.21s | -11.82%
0m08.55s | ExtractionOCaml/saturated_solinas.ml | 0m05.49s || +0m03.06s | +55.73%
3m24.98s | p384_32.c | 3m22.52s || +0m02.45s | +1.21%
1m03.78s | ExtractionHaskell/word_by_word_montgomery | 1m01.13s || +0m02.64s | +4.33%
0m47.85s | p521_32.c | 0m45.77s || +0m02.07s | +4.54%
1m42.64s | Fancy/Barrett256.vo | 1m41.49s || +0m01.14s | +1.13%
0m40.30s | p521_64.c | 0m42.20s || -0m01.90s | -4.50%
0m18.02s | p256_32.c | 0m19.03s || -0m01.01s | -5.30%
0m14.70s | ExtractionOCaml/unsaturated_solinas | 0m13.33s || +0m01.36s | +10.27%
0m14.28s | p434_64.c | 0m15.39s || -0m01.11s | -7.21%
0m09.82s | p224_32.c | 0m08.77s || +0m01.05s | +11.97%
0m08.59s | p384_64.c | 0m07.36s || +0m01.22s | +16.71%
0m05.18s | ExtractionHaskell/saturated_solinas.hs | 0m06.59s || -0m01.41s | -21.39%
1m34.02s | RewriterWf2.vo | 1m34.23s || -0m00.20s | -0.22%
0m56.16s | Rewriter/ToFancyWithCasts.vo | 0m55.41s || +0m00.75s | +1.35%
0m45.85s | Rewriter/NBE.vo | 0m45.23s || +0m00.62s | +1.37%
0m44.51s | Rewriter/ArithWithCasts.vo | 0m44.12s || +0m00.39s | +0.88%
0m44.10s | RewriterInterpProofs1.vo | 0m43.89s || +0m00.21s | +0.47%
0m43.66s | ExtractionHaskell/unsaturated_solinas | 0m43.25s || +0m00.40s | +0.94%
0m36.46s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.36s || +0m00.10s | +0.27%
0m36.09s | RewriterWf1.vo | 0m36.07s || +0m00.02s | +0.05%
0m34.50s | Fancy/Montgomery256.vo | 0m34.30s || +0m00.20s | +0.58%
0m27.13s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.99s || +0m00.14s | +0.51%
0m24.70s | Rewriter/Arith.vo | 0m24.26s || +0m00.43s | +1.81%
0m22.75s | ExtractionOCaml/word_by_word_montgomery | 0m22.15s || +0m00.60s | +2.70%
0m20.96s | PushButtonSynthesis/BarrettReduction.vo | 0m20.74s || +0m00.22s | +1.06%
0m18.96s | p448_solinas_64.c | 0m19.32s || -0m00.35s | -1.86%
0m18.16s | secp256k1_32.c | 0m18.13s || +0m00.03s | +0.16%
0m14.62s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.77s || +0m00.84s | +6.17%
0m11.84s | ExtractionOCaml/saturated_solinas | 0m11.30s || +0m00.53s | +4.77%
0m09.55s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.14s || +0m00.41s | +4.48%
0m08.42s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.16s || +0m00.25s | +3.18%
0m06.96s | BoundsPipeline.vo | 0m06.85s || +0m00.11s | +1.60%
0m06.54s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.17s || -0m00.62s | -8.78%
0m03.57s | PushButtonSynthesis/Primitives.vo | 0m03.46s || +0m00.10s | +3.17%
0m03.35s | PushButtonSynthesis/SmallExamples.vo | 0m03.34s || +0m00.01s | +0.29%
0m03.30s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || +0m00.07s | +2.48%
0m02.83s | curve25519_32.c | 0m02.86s || -0m00.02s | -1.04%
0m02.70s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.63s || +0m00.07s | +2.66%
0m02.08s | Rewriter.vo | 0m02.02s || +0m00.06s | +2.97%
0m01.60s | curve25519_64.c | 0m01.82s || -0m00.21s | -12.08%
0m01.47s | secp256k1_64.c | 0m01.94s || -0m00.47s | -24.22%
0m01.34s | p224_64.c | 0m01.71s || -0m00.36s | -21.63%
0m01.33s | CLI.vo | 0m01.38s || -0m00.04s | -3.62%
0m01.32s | p256_64.c | 0m01.77s || -0m00.44s | -25.42%
0m01.28s | Rewriter/ToFancy.vo | 0m01.36s || -0m00.08s | -5.88%
0m01.23s | Rewriter/StripLiteralCasts.vo | 0m01.08s || +0m00.14s | +13.88%
0m01.16s | StandaloneHaskellMain.vo | 0m01.18s || -0m00.02s | -1.69%
0m01.13s | CompilersTestCases.vo | 0m01.18s || -0m00.05s | -4.23%
0m01.07s | StandaloneOCamlMain.vo | 0m01.12s || -0m00.05s | -4.46%
0m00.83s | RewriterAll.vo | 0m00.66s || +0m00.16s | +25.75%
0m00.78s | RewriterAllTactics.vo | 0m00.83s || -0m00.04s | -6.02%
Diffstat (limited to 'src/Util/Bool/Reflect.v')
0 files changed, 0 insertions, 0 deletions