aboutsummaryrefslogtreecommitdiff
path: root/src/GENERATEDIdentifiersWithoutTypes.v
Commit message (Collapse)AuthorAge
* Do less reduction in GENERATEDIdentifiersWithoutTypesGravatar Jason Gross2019-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since more of the definitions are now done in Gallina, hopefully these should be easier to factor out / parameterize over the type of identifiers, now. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 21m28.78s | Total | 21m49.80s || -0m21.01s | -1.60% ----------------------------------------------------------------------------------------------- 0m22.98s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m49.53s || -0m26.55s | -53.60% 0m47.26s | p521_32.c | 0m44.08s || +0m03.17s | +7.21% 0m36.30s | ExtractionHaskell/saturated_solinas | 0m32.96s || +0m03.33s | +10.13% 1m00.34s | ExtractionHaskell/word_by_word_montgomery | 1m02.45s || -0m02.10s | -3.37% 0m26.90s | SlowPrimeSynthesisExamples.vo | 0m24.35s || +0m02.54s | +10.47% 0m16.06s | GENERATEDIdentifiersWithoutTypes.vo | 0m19.05s || -0m02.99s | -15.69% 0m14.89s | ExtractionOCaml/unsaturated_solinas | 0m12.83s || +0m02.06s | +16.05% 0m43.92s | ExtractionHaskell/unsaturated_solinas | 0m42.40s || +0m01.52s | +3.58% 0m20.11s | ExtractionOCaml/word_by_word_montgomery | 0m21.19s || -0m01.08s | -5.09% 0m20.06s | p256_32.c | 0m21.81s || -0m01.75s | -8.02% 0m17.96s | secp256k1_32.c | 0m19.45s || -0m01.48s | -7.66% 0m13.58s | ExtractionOCaml/word_by_word_montgomery.ml | 0m14.89s || -0m01.31s | -8.79% 0m07.27s | ExtractionOCaml/saturated_solinas.ml | 0m05.75s || +0m01.51s | +26.43% 3m23.62s | p384_32.c | 3m23.29s || +0m00.33s | +0.16% 1m42.18s | Fancy/Barrett256.vo | 1m41.69s || +0m00.49s | +0.48% 1m33.94s | RewriterWf2.vo | 1m34.43s || -0m00.49s | -0.51% 0m55.14s | Rewriter/ToFancyWithCasts.vo | 0m55.92s || -0m00.78s | -1.39% 0m46.15s | Rewriter/NBE.vo | 0m46.06s || +0m00.08s | +0.19% 0m44.70s | Rewriter/ArithWithCasts.vo | 0m44.55s || +0m00.15s | +0.33% 0m43.96s | RewriterInterpProofs1.vo | 0m44.18s || -0m00.21s | -0.49% 0m39.78s | p521_64.c | 0m38.84s || +0m00.93s | +2.42% 0m36.72s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.54s || +0m00.17s | +0.49% 0m35.92s | RewriterWf1.vo | 0m36.26s || -0m00.33s | -0.93% 0m34.57s | Fancy/Montgomery256.vo | 0m34.64s || -0m00.07s | -0.20% 0m27.29s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.17s || +0m00.11s | +0.44% 0m23.67s | Rewriter/Arith.vo | 0m24.59s || -0m00.91s | -3.74% 0m20.78s | PushButtonSynthesis/BarrettReduction.vo | 0m20.69s || +0m00.08s | +0.43% 0m18.97s | p448_solinas_64.c | 0m18.10s || +0m00.86s | +4.80% 0m14.02s | p434_64.c | 0m13.37s || +0m00.65s | +4.86% 0m11.26s | ExtractionOCaml/unsaturated_solinas.ml | 0m10.61s || +0m00.65s | +6.12% 0m10.76s | ExtractionOCaml/saturated_solinas | 0m11.65s || -0m00.89s | -7.63% 0m08.76s | p224_32.c | 0m09.58s || -0m00.82s | -8.55% 0m08.07s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.96s || +0m00.11s | +1.38% 0m07.88s | p384_64.c | 0m08.81s || -0m00.93s | -10.55% 0m06.98s | BoundsPipeline.vo | 0m06.97s || +0m00.01s | +0.14% 0m06.41s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.52s || +0m00.89s | +16.12% 0m05.21s | ExtractionHaskell/saturated_solinas.hs | 0m04.48s || +0m00.72s | +16.29% 0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.61s || -0m00.06s | -1.93% 0m03.33s | PushButtonSynthesis/SmallExamples.vo | 0m03.38s || -0m00.04s | -1.47% 0m03.20s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || -0m00.02s | -0.62% 0m03.05s | curve25519_32.c | 0m02.76s || +0m00.29s | +10.50% 0m02.63s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.70s || -0m00.07s | -2.59% 0m02.53s | Rewriter.vo | 0m02.04s || +0m00.48s | +24.01% 0m02.10s | curve25519_64.c | 0m01.80s || +0m00.30s | +16.66% 0m01.94s | p224_64.c | 0m01.52s || +0m00.41s | +27.63% 0m01.85s | secp256k1_64.c | 0m01.55s || +0m00.30s | +19.35% 0m01.40s | CLI.vo | 0m01.33s || +0m00.06s | +5.26% 0m01.36s | p256_64.c | 0m01.84s || -0m00.48s | -26.08% 0m01.33s | Rewriter/StripLiteralCasts.vo | 0m01.22s || +0m00.11s | +9.01% 0m01.23s | CompilersTestCases.vo | 0m01.14s || +0m00.09s | +7.89% 0m01.15s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.03s | +3.60% 0m01.13s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.04s | -3.41% 0m01.11s | Rewriter/ToFancy.vo | 0m01.07s || +0m00.04s | +3.73% 0m00.80s | RewriterAll.vo | 0m00.80s || +0m00.00s | +0.00% 0m00.74s | RewriterAllTactics.vo | 0m00.91s || -0m00.17s | -18.68% The diff in the .ml files is quite small, and is effectively just variable renaming: ```diff diff --git a/src/ExtractionOCaml/saturated_solinas.ml b/src/ExtractionOCaml/saturated_solinas.ml index fd8a9d3..e9afa49 100644 --- a/src/ExtractionOCaml/saturated_solinas.ml +++ b/src/ExtractionOCaml/saturated_solinas.ml @@ -39856,7 +39856,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -39962,7 +39962,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40068,7 +40068,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40174,7 +40174,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40280,7 +40280,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49466,8 +49466,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None diff --git a/src/ExtractionOCaml/unsaturated_solinas.ml b/src/ExtractionOCaml/unsaturated_solinas.ml index 473992c..4d4d604 100644 --- a/src/ExtractionOCaml/unsaturated_solinas.ml +++ b/src/ExtractionOCaml/unsaturated_solinas.ml @@ -40045,7 +40045,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -40151,7 +40151,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40257,7 +40257,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40363,7 +40363,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40469,7 +40469,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49655,8 +49655,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None diff --git a/src/ExtractionOCaml/word_by_word_montgomery.ml b/src/ExtractionOCaml/word_by_word_montgomery.ml index f955bc6..a672b5d 100644 --- a/src/ExtractionOCaml/word_by_word_montgomery.ml +++ b/src/ExtractionOCaml/word_by_word_montgomery.ml @@ -39944,7 +39944,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -40050,7 +40050,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40156,7 +40156,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40262,7 +40262,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40368,7 +40368,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49554,8 +49554,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None ```
* Fix around coq/coq#262Gravatar Jason Gross2019-04-12
| | | | Reported as https://github.com/coq/coq/issues/9955
* Replace the python script with Ltac codeGravatar Jason Gross2019-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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%
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
|
* Add eager_nth_defaultGravatar Jason Gross2019-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------------- 36m12.92s | Total | 35m47.30s || +0m25.61s | +1.19% ----------------------------------------------------------------------------------------------------------- 3m17.05s | p384_32.c | 3m13.40s || +0m03.65s | +1.88% 0m35.31s | AbstractInterpretationZRangeProofs.vo | 0m32.23s || +0m03.08s | +9.55% 2m54.44s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m51.77s || +0m02.66s | +1.55% 1m49.48s | RewriterRulesInterpGood.vo | 1m47.32s || +0m02.15s | +2.01% 1m08.68s | GENERATEDIdentifiersWithoutTypesProofs.vo | 1m06.34s || +0m02.34s | +3.52% 0m43.79s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m45.80s || -0m02.00s | -4.38% 0m42.94s | UnderLetsProofs.vo | 0m40.56s || +0m02.37s | +5.86% 0m24.06s | ExtractionOCaml/word_by_word_montgomery | 0m21.22s || +0m02.83s | +13.38% 2m40.36s | Fancy/Compiler.vo | 2m38.94s || +0m01.42s | +0.89% 2m01.11s | RewriterWf2.vo | 1m59.26s || +0m01.85s | +1.55% 1m55.19s | RewriterRulesGood.vo | 1m56.66s || -0m01.46s | -1.26% 1m47.22s | Fancy/Barrett256.vo | 1m45.62s || +0m01.59s | +1.51% 0m58.84s | ExtractionHaskell/word_by_word_montgomery | 0m57.60s || +0m01.24s | +2.15% 0m31.40s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m29.80s || +0m01.59s | +5.36% 0m29.65s | ExtractionHaskell/saturated_solinas | 0m31.01s || -0m01.36s | -4.38% 0m25.82s | SlowPrimeSynthesisExamples.vo | 0m24.58s || +0m01.24s | +5.04% 0m18.46s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m16.98s || +0m01.48s | +8.71% 0m14.02s | ExtractionOCaml/unsaturated_solinas | 0m12.74s || +0m01.27s | +10.04% 0m07.66s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.32s || +0m01.33s | +21.20% 1m21.57s | Rewriter.vo | 1m22.53s || -0m00.96s | -1.16% 0m55.21s | RewriterInterpProofs1.vo | 0m56.14s || -0m00.92s | -1.65% 0m54.08s | AbstractInterpretationWf.vo | 0m54.37s || -0m00.28s | -0.53% 0m46.95s | p521_32.c | 0m46.27s || +0m00.67s | +1.46% 0m44.37s | LanguageInversion.vo | 0m43.42s || +0m00.94s | +2.18% 0m41.31s | ExtractionHaskell/unsaturated_solinas | 0m41.46s || -0m00.14s | -0.36% 0m40.51s | p521_64.c | 0m40.38s || +0m00.12s | +0.32% 0m37.50s | Fancy/Montgomery256.vo | 0m37.46s || +0m00.03s | +0.10% 0m36.28s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.34s || -0m00.06s | -0.16% 0m33.28s | AbstractInterpretationProofs.vo | 0m33.19s || +0m00.09s | +0.27% 0m29.56s | LanguageWf.vo | 0m29.64s || -0m00.08s | -0.26% 0m26.86s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.96s || -0m00.10s | -0.37% 0m25.33s | RewriterWf1.vo | 0m25.65s || -0m00.32s | -1.24% 0m19.81s | p256_32.c | 0m20.11s || -0m00.30s | -1.49% 0m18.70s | secp256k1_32.c | 0m19.18s || -0m00.48s | -2.50% 0m18.62s | p448_solinas_64.c | 0m19.51s || -0m00.89s | -4.56% 0m16.73s | CStringification.vo | 0m16.25s || +0m00.48s | +2.95% 0m15.03s | p434_64.c | 0m15.84s || -0m00.81s | -5.11% 0m13.45s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.80s || -0m00.35s | -2.53% 0m13.44s | GENERATEDIdentifiersWithoutTypes.vo | 0m13.30s || +0m00.13s | +1.05% 0m10.74s | ExtractionOCaml/saturated_solinas | 0m10.38s || +0m00.35s | +3.46% 0m09.11s | p224_32.c | 0m08.93s || +0m00.17s | +2.01% 0m08.78s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.92s || +0m00.85s | +10.85% 0m08.74s | p384_64.c | 0m08.50s || +0m00.24s | +2.82% 0m08.66s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.47s || -0m00.81s | -8.55% 0m07.90s | ExtractionOCaml/saturated_solinas.ml | 0m06.93s || +0m00.97s | +13.99% 0m06.80s | BoundsPipeline.vo | 0m06.73s || +0m00.06s | +1.04% 0m06.57s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.78s || -0m00.20s | -3.09% 0m05.68s | Fancy/Prod.vo | 0m05.78s || -0m00.10s | -1.73% 0m05.36s | ExtractionHaskell/saturated_solinas.hs | 0m05.40s || -0m00.04s | -0.74% 0m03.86s | MiscCompilerPassesProofs.vo | 0m04.20s || -0m00.34s | -8.09% 0m03.37s | PushButtonSynthesis/Primitives.vo | 0m03.41s || -0m00.04s | -1.17% 0m03.36s | PushButtonSynthesis/SmallExamples.vo | 0m03.22s || +0m00.13s | +4.34% 0m03.20s | PushButtonSynthesis/BarrettReduction.vo | 0m03.16s || +0m00.04s | +1.26% 0m03.19s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.12s || +0m00.06s | +2.24% 0m03.00s | curve25519_32.c | 0m02.62s || +0m00.37s | +14.50% 0m02.83s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.82s || +0m00.01s | +0.35% 0m02.02s | curve25519_64.c | 0m02.12s || -0m00.10s | -4.71% 0m01.61s | p224_64.c | 0m01.48s || +0m00.13s | +8.78% 0m01.60s | secp256k1_64.c | 0m01.70s || -0m00.09s | -5.88% 0m01.48s | p256_64.c | 0m01.28s || +0m00.19s | +15.62% 0m01.34s | CompilersTestCases.vo | 0m01.24s || +0m00.10s | +8.06% 0m01.30s | CLI.vo | 0m01.35s || -0m00.05s | -3.70% 0m01.30s | Language.vo | 0m01.33s || -0m00.03s | -2.25% 0m01.28s | AbstractInterpretation.vo | 0m01.28s || +0m00.00s | +0.00% 0m01.24s | RewriterProofs.vo | 0m01.16s || +0m00.08s | +6.89% 0m01.07s | StandaloneHaskellMain.vo | 0m01.26s || -0m00.18s | -15.07% 0m01.04s | StandaloneOCamlMain.vo | 0m01.27s || -0m00.23s | -18.11% 0m00.76s | MiscCompilerPasses.vo | 0m00.82s || -0m00.05s | -7.31% 0m00.61s | PushButtonSynthesis/LegacySynthesisTactics.vo | 0m00.66s || -0m00.05s | -7.57% 0m00.57s | PushButtonSynthesis/ReificationCache.vo | 0m00.52s || +0m00.04s | +9.61% 0m00.48s | UnderLets.vo | 0m00.51s || -0m00.03s | -5.88%
* Add list_rect_arrowGravatar Jason Gross2019-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------------- 36m06.27s | Total | 35m50.70s || +0m15.57s | +0.72% ----------------------------------------------------------------------------------------------------------- 2m45.00s | Fancy/Compiler.vo | 2m40.67s || +0m04.32s | +2.69% 1m05.90s | GENERATEDIdentifiersWithoutTypesProofs.vo | 1m02.06s || +0m03.84s | +6.18% 0m19.29s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m16.24s || +0m03.05s | +18.78% 2m55.24s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m57.84s || -0m02.59s | -1.46% 1m56.35s | RewriterRulesGood.vo | 1m54.16s || +0m02.18s | +1.91% 0m41.32s | ExtractionHaskell/unsaturated_solinas | 0m39.10s || +0m02.21s | +5.67% 0m34.84s | AbstractInterpretationProofs.vo | 0m32.77s || +0m02.07s | +6.31% 0m17.77s | p448_solinas_64.c | 0m20.12s || -0m02.35s | -11.67% 2m01.09s | RewriterWf2.vo | 1m59.61s || +0m01.48s | +1.23% 1m48.15s | RewriterRulesInterpGood.vo | 1m49.56s || -0m01.40s | -1.28% 1m21.56s | Rewriter.vo | 1m22.98s || -0m01.42s | -1.71% 0m57.30s | ExtractionHaskell/word_by_word_montgomery | 0m58.76s || -0m01.46s | -2.48% 0m47.94s | p521_32.c | 0m46.84s || +0m01.09s | +2.34% 0m38.63s | Fancy/Montgomery256.vo | 0m37.28s || +0m01.35s | +3.62% 0m26.01s | SlowPrimeSynthesisExamples.vo | 0m24.90s || +0m01.11s | +4.45% 0m13.56s | ExtractionOCaml/unsaturated_solinas | 0m12.32s || +0m01.24s | +10.06% 0m09.90s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.70s || +0m01.20s | +13.79% 3m16.06s | p384_32.c | 3m15.80s || +0m00.25s | +0.13% 1m46.10s | Fancy/Barrett256.vo | 1m47.02s || -0m00.92s | -0.85% 0m56.15s | RewriterInterpProofs1.vo | 0m56.60s || -0m00.45s | -0.79% 0m54.38s | AbstractInterpretationWf.vo | 0m53.72s || +0m00.66s | +1.22% 0m44.40s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m44.48s || -0m00.07s | -0.17% 0m43.51s | LanguageInversion.vo | 0m42.77s || +0m00.73s | +1.73% 0m41.61s | UnderLetsProofs.vo | 0m41.02s || +0m00.58s | +1.43% 0m39.63s | p521_64.c | 0m39.86s || -0m00.22s | -0.57% 0m36.21s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.25s || -0m00.03s | -0.11% 0m32.80s | AbstractInterpretationZRangeProofs.vo | 0m33.19s || -0m00.39s | -1.17% 0m30.94s | ExtractionHaskell/saturated_solinas | 0m30.24s || +0m00.70s | +2.31% 0m29.79s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m30.53s || -0m00.74s | -2.42% 0m29.47s | LanguageWf.vo | 0m29.89s || -0m00.42s | -1.40% 0m26.82s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.79s || +0m00.03s | +0.11% 0m25.66s | RewriterWf1.vo | 0m25.60s || +0m00.05s | +0.23% 0m22.53s | ExtractionOCaml/word_by_word_montgomery | 0m22.10s || +0m00.42s | +1.94% 0m19.93s | secp256k1_32.c | 0m19.65s || +0m00.28s | +1.42% 0m19.36s | p256_32.c | 0m19.96s || -0m00.60s | -3.00% 0m16.44s | CStringification.vo | 0m16.20s || +0m00.24s | +1.48% 0m16.13s | p434_64.c | 0m15.73s || +0m00.39s | +2.54% 0m13.93s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.21s || +0m00.71s | +5.45% 0m12.76s | GENERATEDIdentifiersWithoutTypes.vo | 0m12.35s || +0m00.41s | +3.31% 0m09.96s | ExtractionOCaml/saturated_solinas | 0m10.05s || -0m00.08s | -0.89% 0m09.08s | p224_32.c | 0m08.38s || +0m00.69s | +8.35% 0m08.38s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.55s || -0m00.16s | -1.98% 0m07.65s | p384_64.c | 0m08.54s || -0m00.88s | -10.42% 0m06.72s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.69s || +0m00.02s | +0.44% 0m06.64s | BoundsPipeline.vo | 0m06.58s || +0m00.05s | +0.91% 0m06.58s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.48s || +0m00.09s | +1.54% 0m06.50s | ExtractionOCaml/saturated_solinas.ml | 0m07.02s || -0m00.51s | -7.40% 0m05.84s | Fancy/Prod.vo | 0m05.75s || +0m00.08s | +1.56% 0m04.96s | ExtractionHaskell/saturated_solinas.hs | 0m05.78s || -0m00.82s | -14.18% 0m03.50s | PushButtonSynthesis/Primitives.vo | 0m03.35s || +0m00.14s | +4.47% 0m03.41s | PushButtonSynthesis/SmallExamples.vo | 0m03.29s || +0m00.12s | +3.64% 0m03.19s | PushButtonSynthesis/BarrettReduction.vo | 0m03.26s || -0m00.06s | -2.14% 0m03.18s | curve25519_32.c | 0m02.47s || +0m00.71s | +28.74% 0m03.14s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.25s || -0m00.10s | -3.38% 0m02.86s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.73s || +0m00.12s | +4.76% 0m02.85s | MiscCompilerPassesProofs.vo | 0m03.76s || -0m00.90s | -24.20% 0m02.15s | curve25519_64.c | 0m02.16s || -0m00.01s | -0.46% 0m01.59s | secp256k1_64.c | 0m01.68s || -0m00.08s | -5.35% 0m01.36s | Language.vo | 0m01.25s || +0m00.11s | +8.80% 0m01.35s | CLI.vo | 0m01.35s || +0m00.00s | +0.00% 0m01.29s | p224_64.c | 0m01.59s || -0m00.30s | -18.86% 0m01.29s | p256_64.c | 0m01.33s || -0m00.04s | -3.00% 0m01.25s | CompilersTestCases.vo | 0m01.55s || -0m00.30s | -19.35% 0m01.22s | AbstractInterpretation.vo | 0m01.28s || -0m00.06s | -4.68% 0m01.12s | StandaloneHaskellMain.vo | 0m01.14s || -0m00.01s | -1.75% 0m01.12s | StandaloneOCamlMain.vo | 0m01.10s || +0m00.02s | +1.81% 0m01.01s | RewriterProofs.vo | 0m01.14s || -0m00.12s | -11.40% 0m00.74s | MiscCompilerPasses.vo | 0m00.68s || +0m00.05s | +8.82% 0m00.70s | PushButtonSynthesis/ReificationCache.vo | 0m00.50s || +0m00.19s | +39.99% 0m00.69s | PushButtonSynthesis/LegacySynthesisTactics.vo | 0m00.64s || +0m00.04s | +7.81% 0m00.49s | UnderLets.vo | 0m00.51s || -0m00.02s | -3.92%
* Add a couple more identifiers to support eager recGravatar Jason Gross2019-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This will allow us to write rewrite rules that eagerly evaluate recursion principles on the RHS. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------------- 35m52.89s | Total | 35m21.19s || +0m31.69s | +1.49% ----------------------------------------------------------------------------------------------------------- 1m03.44s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m52.51s || +0m10.92s | +20.81% 0m42.76s | UnderLetsProofs.vo | 0m37.59s || +0m05.16s | +13.75% 1m50.02s | RewriterRulesInterpGood.vo | 1m46.65s || +0m03.37s | +3.15% 3m14.40s | p384_32.c | 3m16.54s || -0m02.13s | -1.08% 1m53.47s | RewriterRulesGood.vo | 1m56.16s || -0m02.68s | -2.31% 0m34.80s | AbstractInterpretationZRangeProofs.vo | 0m32.33s || +0m02.46s | +7.63% 0m22.80s | ExtractionOCaml/word_by_word_montgomery | 0m20.53s || +0m02.26s | +11.05% 2m55.61s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m53.77s || +0m01.84s | +1.05% 2m37.56s | Fancy/Compiler.vo | 2m39.51s || -0m01.94s | -1.22% 1m47.71s | Fancy/Barrett256.vo | 1m46.42s || +0m01.29s | +1.21% 0m59.28s | ExtractionHaskell/word_by_word_montgomery | 0m57.33s || +0m01.95s | +3.40% 0m42.71s | LanguageInversion.vo | 0m40.75s || +0m01.96s | +4.80% 0m40.95s | ExtractionHaskell/unsaturated_solinas | 0m39.76s || +0m01.19s | +2.99% 0m32.88s | AbstractInterpretationProofs.vo | 0m31.38s || +0m01.50s | +4.78% 0m28.98s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m27.08s || +0m01.90s | +7.01% 0m17.39s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m18.95s || -0m01.55s | -8.23% 0m12.51s | GENERATEDIdentifiersWithoutTypes.vo | 0m11.11s || +0m01.40s | +12.60% 0m12.30s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.84s || -0m01.53s | -11.12% 0m07.16s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.67s || +0m01.49s | +26.27% 0m05.84s | ExtractionHaskell/saturated_solinas.hs | 0m04.84s || +0m01.00s | +20.66% 2m01.25s | RewriterWf2.vo | 2m01.06s || +0m00.18s | +0.15% 1m22.67s | Rewriter.vo | 1m22.48s || +0m00.18s | +0.23% 0m54.42s | AbstractInterpretationWf.vo | 0m55.26s || -0m00.83s | -1.52% 0m53.40s | RewriterInterpProofs1.vo | 0m52.85s || +0m00.54s | +1.04% 0m46.26s | p521_32.c | 0m46.58s || -0m00.32s | -0.68% 0m44.94s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m45.20s || -0m00.26s | -0.57% 0m40.17s | p521_64.c | 0m39.49s || +0m00.67s | +1.72% 0m37.93s | Fancy/Montgomery256.vo | 0m37.31s || +0m00.61s | +1.66% 0m36.59s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.22s || +0m00.37s | +1.02% 0m30.06s | ExtractionHaskell/saturated_solinas | 0m29.33s || +0m00.73s | +2.48% 0m29.61s | LanguageWf.vo | 0m29.48s || +0m00.12s | +0.44% 0m26.76s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.77s || -0m00.00s | -0.03% 0m26.23s | SlowPrimeSynthesisExamples.vo | 0m26.36s || -0m00.12s | -0.49% 0m25.30s | RewriterWf1.vo | 0m25.47s || -0m00.16s | -0.66% 0m20.01s | p448_solinas_64.c | 0m19.97s || +0m00.04s | +0.20% 0m19.56s | p256_32.c | 0m20.04s || -0m00.48s | -2.39% 0m19.28s | secp256k1_32.c | 0m18.86s || +0m00.42s | +2.22% 0m16.08s | CStringification.vo | 0m15.70s || +0m00.37s | +2.42% 0m16.04s | p434_64.c | 0m15.20s || +0m00.83s | +5.52% 0m13.39s | ExtractionOCaml/unsaturated_solinas | 0m13.13s || +0m00.25s | +1.98% 0m09.57s | p224_32.c | 0m08.95s || +0m00.62s | +6.92% 0m09.27s | ExtractionOCaml/saturated_solinas | 0m10.22s || -0m00.95s | -9.29% 0m08.70s | p384_64.c | 0m07.93s || +0m00.76s | +9.70% 0m08.43s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.07s || -0m00.64s | -7.05% 0m07.44s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.35s || -0m00.90s | -10.89% 0m06.97s | ExtractionOCaml/saturated_solinas.ml | 0m07.28s || -0m00.31s | -4.25% 0m06.81s | BoundsPipeline.vo | 0m06.78s || +0m00.02s | +0.44% 0m06.72s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.85s || -0m00.12s | -1.89% 0m05.77s | Fancy/Prod.vo | 0m06.07s || -0m00.30s | -4.94% 0m04.06s | MiscCompilerPassesProofs.vo | 0m03.84s || +0m00.21s | +5.72% 0m03.71s | PushButtonSynthesis/Primitives.vo | 0m03.34s || +0m00.37s | +11.07% 0m03.34s | PushButtonSynthesis/SmallExamples.vo | 0m03.26s || +0m00.08s | +2.45% 0m03.16s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || -0m00.06s | -1.86% 0m03.15s | PushButtonSynthesis/BarrettReduction.vo | 0m03.29s || -0m00.14s | -4.25% 0m02.84s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.90s || -0m00.06s | -2.06% 0m02.79s | curve25519_32.c | 0m02.92s || -0m00.12s | -4.45% 0m02.12s | curve25519_64.c | 0m02.13s || -0m00.00s | -0.46% 0m01.70s | secp256k1_64.c | 0m01.55s || +0m00.14s | +9.67% 0m01.64s | p256_64.c | 0m01.23s || +0m00.40s | +33.33% 0m01.57s | p224_64.c | 0m01.68s || -0m00.10s | -6.54% 0m01.36s | Language.vo | 0m01.33s || +0m00.03s | +2.25% 0m01.33s | CLI.vo | 0m01.32s || +0m00.01s | +0.75% 0m01.26s | AbstractInterpretation.vo | 0m01.25s || +0m00.01s | +0.80% 0m01.13s | RewriterProofs.vo | 0m01.18s || -0m00.05s | -4.23% 0m01.13s | StandaloneOCamlMain.vo | 0m01.04s || +0m00.08s | +8.65% 0m01.10s | CompilersTestCases.vo | 0m01.16s || -0m00.05s | -5.17% 0m01.04s | StandaloneHaskellMain.vo | 0m01.18s || -0m00.13s | -11.86% 0m00.76s | MiscCompilerPasses.vo | 0m00.74s || +0m00.02s | +2.70% 0m00.60s | PushButtonSynthesis/LegacySynthesisTactics.vo | 0m00.66s || -0m00.06s | -9.09% 0m00.46s | UnderLets.vo | 0m00.48s || -0m00.01s | -4.16% 0m00.44s | PushButtonSynthesis/ReificationCache.vo | 0m00.52s || -0m00.08s | -15.38%
* Add some things to GENERATED rewriter fileGravatar Jason Gross2019-03-04
|
* Add support for reifying `zrange` and `option`Gravatar Jason Gross2019-02-18
| | | | This is needed to reify statements for the rewriter.
* Support Nat.eqb in reificationGravatar Jason Gross2019-01-25
|
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 09:25:08 +0000