aboutsummaryrefslogtreecommitdiff
path: root/src/GENERATEDIdentifiersWithoutTypesProofs.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 ```
* 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 support for reifying `zrange` and `option`Gravatar Jason Gross2019-02-18
| | | | This is needed to reify statements for the rewriter.
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 00:59:37 +0000