| f020c4e | Jason Gross | 13 July 2021, 22:47:13 UTC | Add logs for previous OOM up to 20GB with 1h timeout ``` grep -A 2 memory time-of-build-perf.log | grep -o 'File "[^"]*' | sed s',File "./,,g' | sort | uniq | sed s'/\.v/\.log/g' | xargs time make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync -kj3 PERF_MAX_TIME=3600 PERF_MAX_MEM=20000000 2>&1 | tee -a time-of-build-perf-20.log ``` ``` 1044575.40user 5179.76system 97:46:10elapsed 298%CPU (0avgtext+0avgdata 15855332maxresident)k 424inputs+607713784outputs (0major+3386228715minor)pagefaults 0swaps ``` | 15 July 2021, 00:28:57 UTC |
| 55b2915 | Jason Gross | 05 July 2021, 02:51:43 UTC | Make all perf-only-computed-vos up to 3600s ``` real 1870m59.951s user 9251m0.351s sys 4m47.998s ``` ``` time make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync -kj5 perf-only-computed-vos PERF_MAX_TIME=3600 2>&1 | tee -a time-of-build-perf.log ``` | 15 July 2021, 00:28:57 UTC |
| 47776f4 | Jason Gross | 03 July 2021, 17:10:23 UTC | Add perf-except-computed-vos up to 1h ``` time make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync -kj5 perf-except-computed-vos PERF_MAX_TIME=3600 2>&1 | tee -a time-of-build-perf.log ``` ``` real 2591m28.408s user 12868m33.767s sys 53m26.833s ``` | 15 July 2021, 00:28:57 UTC |
| 93e04c7 | Jason Gross | 01 July 2021, 21:30:09 UTC | Add perf-extraction logs ``` make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync -kj5 perf-extraction PERF_MAX_TIME=36000 2>&1 | tee -a time-of-build-perf.log ``` | 15 July 2021, 00:28:57 UTC |
| bc7928d | Jason Gross | 01 July 2021, 16:31:22 UTC | Add logs with 10 minute timeout ``` make COQBIN="$HOME/.local64/coq/coq-8.11.1/bin/" SKIP_BEDROCK2=1 TIMED=1 --output-sync -kj5 perf 2>&1 | tee -a time-of-build-perf.log ``` | 15 July 2021, 00:28:57 UTC |
| 0368b16 | Jason Gross | 28 June 2021, 20:34:32 UTC | Add timing log for 8.11.1 The Coq Proof Assistant, version 8.11.1 (April 2020) compiled on Apr 4 2020 17:41:20 with OCaml 4.06.1 <details><summary>Timing Diff</summary> <p> ``` Time | Peak Mem | File Name --------------------------------------------------------------------------------------------- 154m57.11s | 5393136 ko | Total Time / Peak Mem --------------------------------------------------------------------------------------------- 9m38.82s | 1100568 ko | fiat-json/src/p384_32.json 9m07.58s | 2416924 ko | Curves/Weierstrass/AffineProofs.vo 8m15.09s | 938944 ko | fiat-go/32/p384/p384.go 8m13.84s | 939020 ko | fiat-c/src/p384_32.c 8m10.06s | 1074260 ko | fiat-rust/src/p384_32.rs 7m19.62s | 1028320 ko | fiat-zig/src/p384_32.zig 7m02.93s | 1074344 ko | fiat-java/src/FiatP384.java 4m57.45s | 2020172 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo 3m59.26s | 1608244 ko | Rewriter/Passes/ArithWithCasts.vo 3m48.45s | 2017408 ko | Curves/Montgomery/XZProofs.vo 3m39.47s | 1300204 ko | Curves/Weierstrass/Projective.vo 3m36.92s | 1259636 ko | Fancy/Compiler.vo 3m13.00s | 1444416 ko | Rewriter/Passes/NBE.vo 3m12.73s | 1252056 ko | Curves/Montgomery/AffineProofs.vo 2m37.55s | 1481732 ko | Rewriter/Passes/ToFancyWithCasts.vo 2m31.45s | 962280 ko | AbstractInterpretation/Wf.vo 1m57.12s | 958760 ko | Rewriter/Rewriter/Wf.vo 1m51.43s | 1541516 ko | Fancy/Barrett256.vo 1m43.87s | 571692 ko | Spec/Test/X25519.vo 1m34.08s | 1454884 ko | SlowPrimeSynthesisExamples.vo 1m23.19s | 881068 ko | AbstractInterpretation/ZRangeProofs.vo 1m20.07s | 1168340 ko | Curves/Weierstrass/Jacobian.vo 1m18.24s | 789636 ko | AbstractInterpretation/Proofs.vo 1m16.92s | 865976 ko | Rewriter/Language/UnderLetsProofs.vo 1m16.81s | 1132364 ko | UnsaturatedSolinasHeuristics/Tests.vo 1m11.08s | 1312400 ko | Fancy/Montgomery256.vo 1m10.37s | 1105200 ko | Rewriter/Passes/MultiRetSplit.vo 1m08.38s | 5393136 ko | Rewriter/PerfTesting/Core.vo 1m04.22s | 956596 ko | Rewriter/Rewriter/InterpProofs.vo 1m01.74s | 773632 ko | Rewriter/RulesProofs.vo 0m58.57s | 1057304 ko | Rewriter/Passes/Arith.vo 0m56.82s | 874064 ko | Rewriter/Rewriter/ProofsCommon.vo 0m54.90s | 648712 ko | Demo.vo 0m53.35s | 2103332 ko | ExtractionOCaml/word_by_word_montgomery 0m52.38s | 963324 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo 0m51.43s | 806092 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo 0m50.75s | 214664 ko | fiat-json/src/secp256k1_32.json 0m44.13s | 212628 ko | fiat-json/src/p256_32.json 0m42.00s | 882088 ko | Rewriter/Passes/MulSplit.vo 0m41.97s | 965052 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo 0m36.99s | 2284284 ko | ExtractionOCaml/word_by_word_montgomery.ml 0m36.46s | 151824 ko | fiat-json/src/p434_64.json 0m35.19s | 811208 ko | Rewriter/Rewriter/Examples.vo 0m34.68s | 56376 ko | fiat-json/src/p448_solinas_32.json 0m34.25s | 569628 ko | Arithmetic/Saturated.vo 0m33.65s | 1212804 ko | ExtractionOCaml/unsaturated_solinas 0m33.35s | 1033764 ko | PushButtonSynthesis/BYInversionReificationCache.vo 0m32.89s | 812220 ko | Rewriter/Rewriter/Examples/PrefixSums.vo 0m32.38s | 212808 ko | fiat-zig/src/secp256k1_32.zig 0m32.37s | 242252 ko | fiat-java/src/FiatSecp256K1.java 0m32.36s | 1053280 ko | ExtractionOCaml/perf_word_by_word_montgomery 0m32.15s | 188664 ko | fiat-go/32/secp256k1/secp256k1.go 0m31.88s | 214188 ko | fiat-c/src/secp256k1_32.c 0m31.80s | 186884 ko | fiat-rust/src/secp256k1_32.rs 0m31.72s | 188540 ko | fiat-zig/src/p256_32.zig 0m31.55s | 899464 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo 0m31.24s | 187340 ko | fiat-go/32/p256/p256.go 0m31.14s | 758704 ko | Rewriter/Language/Wf.vo 0m30.83s | 1055052 ko | ExtractionOCaml/saturated_solinas 0m30.83s | 212496 ko | fiat-rust/src/p256_32.rs 0m30.59s | 1055060 ko | ExtractionOCaml/base_conversion 0m28.65s | 1004604 ko | Assembly/Parse/TestAsm.vo 0m28.54s | 187028 ko | fiat-java/src/FiatP256.java 0m28.13s | 191204 ko | fiat-c/src/p256_32.c 0m28.00s | 1054740 ko | ExtractionOCaml/perf_unsaturated_solinas 0m26.20s | 907280 ko | PushButtonSynthesis/UnsaturatedSolinas.vo 0m26.00s | 670292 ko | Util/ZUtil/ArithmeticShiftr.vo 0m25.95s | 934280 ko | PushButtonSynthesis/WordByWordMontgomery.vo 0m24.90s | 805908 ko | Curves/Edwards/AffineProofs.vo 0m24.44s | 765688 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo 0m23.80s | 149284 ko | fiat-go/64/p434/p434.go 0m23.73s | 144088 ko | fiat-zig/src/p434_64.zig 0m23.69s | 135416 ko | fiat-c/src/p434_64.c 0m23.60s | 153832 ko | fiat-rust/src/p434_64.rs 0m23.03s | 1653120 ko | ExtractionOCaml/unsaturated_solinas.ml 0m22.83s | 637788 ko | Rewriter/Language/Inversion.vo 0m22.56s | 117224 ko | fiat-json/src/p224_32.json 0m21.83s | 649836 ko | Arithmetic/WordByWordMontgomery.vo 0m21.56s | 606060 ko | Arithmetic/BarrettReduction.vo 0m19.81s | 828980 ko | Curves/Edwards/XYZT/Basic.vo 0m19.66s | 1538868 ko | ExtractionOCaml/base_conversion.ml 0m19.20s | 2095128 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml 0m18.92s | 2080672 ko | ExtractionOCaml/perf_unsaturated_solinas.ml 0m18.88s | 571076 ko | Arithmetic/Core.vo 0m18.81s | 748044 ko | Language/IdentifiersGENERATED.vo 0m18.72s | 1555312 ko | ExtractionOCaml/saturated_solinas.ml 0m18.18s | 1870044 ko | ExtractionHaskell/word_by_word_montgomery.hs 0m17.86s | 763788 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo 0m17.73s | 467984 ko | Arithmetic/BarrettReduction/RidiculousFish.vo 0m17.55s | 659020 ko | Stringification/IR.vo 0m16.69s | 686216 ko | Util/ZRange/LandLorBounds.vo 0m16.55s | 695192 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo 0m16.33s | 521972 ko | Algebra/Field.vo 0m16.27s | 649668 ko | Language/IdentifiersGENERATEDProofs.vo 0m15.79s | 95880 ko | fiat-json/src/p384_64.json 0m14.53s | 142164 ko | fiat-java/src/FiatP224.java 0m14.42s | 114360 ko | fiat-rust/src/p224_32.rs 0m14.35s | 131916 ko | fiat-go/32/p224/p224.go 0m14.33s | 745468 ko | Rewriter/Demo.vo 0m14.23s | 143868 ko | fiat-zig/src/p224_32.zig 0m14.10s | 125620 ko | fiat-c/src/p224_32.c 0m13.33s | 1497732 ko | ExtractionHaskell/unsaturated_solinas.hs 0m12.73s | 633032 ko | Rewriter/Language/IdentifiersLibraryProofs.vo 0m12.35s | 541576 ko | Primitives/MxDHRepChange.vo 0m12.26s | 1439060 ko | ExtractionHaskell/saturated_solinas.hs 0m11.69s | 561500 ko | Arithmetic/FancyMontgomeryReduction.vo 0m11.42s | 1410696 ko | ExtractionHaskell/base_conversion.hs 0m11.30s | 502592 ko | Algebra/Ring.vo 0m11.20s | 85660 ko | fiat-c/src/p384_64.c 0m11.00s | 99332 ko | fiat-go/64/p384/p384.go 0m10.82s | 95184 ko | fiat-rust/src/p384_64.rs 0m10.51s | 849756 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo 0m10.17s | 100600 ko | fiat-zig/src/p384_64.zig 0m09.98s | 780540 ko | PushButtonSynthesis/SmallExamples.vo 0m09.23s | 511396 ko | Arithmetic/BarrettReduction/Generalized.vo 0m09.14s | 793540 ko | PushButtonSynthesis/BaseConversion.vo 0m09.13s | 513516 ko | Util/ZRange/CornersMonotoneBounds.vo 0m09.12s | 639660 ko | Language/IdentifiersBasicGENERATED.vo 0m08.65s | 787528 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo 0m08.13s | 45660 ko | fiat-zig/src/p448_solinas_32.zig 0m08.11s | 510360 ko | Util/ListUtil.vo 0m08.05s | 45832 ko | fiat-rust/src/p448_solinas_32.rs 0m07.80s | 641564 ko | Rewriter/Passes/NoSelect.vo 0m07.78s | 509412 ko | Rewriter/Util/ListUtil.vo 0m07.76s | 45388 ko | fiat-c/src/p448_solinas_32.c 0m07.53s | 710380 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo 0m07.51s | 814480 ko | PushButtonSynthesis/Primitives.vo 0m07.44s | 631712 ko | Arithmetic/BYInv.vo 0m07.43s | 507944 ko | Util/ZUtil/Modulo.vo 0m07.11s | 784340 ko | PushButtonSynthesis/BarrettReduction.vo 0m07.09s | 651252 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo 0m06.80s | 681856 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo 0m06.75s | 503036 ko | Util/MSets/Sum.vo 0m06.57s | 676780 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo 0m06.00s | 709228 ko | BoundsPipeline.vo 0m05.97s | 502384 ko | Util/ZRange/BasicLemmas.vo 0m05.88s | 28304 ko | fiat-json/src/p521_64.json 0m05.85s | 622804 ko | Fancy/Prod.vo 0m05.82s | 596512 ko | COperationSpecifications.vo 0m05.81s | 575804 ko | Curves/Edwards/Pre.vo 0m05.75s | 470956 ko | Util/ZUtil/ZSimplify/Autogenerated.vo 0m05.55s | 858220 ko | StandaloneDebuggingExamples.vo 0m05.51s | 516824 ko | Util/FsatzAutoLemmas.vo 0m05.44s | 486816 ko | Arithmetic/MontgomeryReduction/Proofs.vo 0m05.39s | 608452 ko | Language/InversionExtra.vo 0m05.21s | 543176 ko | UnsaturatedSolinasHeuristics.vo 0m05.16s | 714352 ko | Assembly/Syntax.vo 0m04.69s | 542332 ko | Algebra/Field_test.vo 0m04.60s | 29948 ko | fiat-json/src/curve25519_32.json 0m04.56s | 529044 ko | Rewriter/Language/IdentifiersBasicLibrary.vo 0m04.50s | 541012 ko | Util/ZUtil/Morphisms.vo 0m04.42s | 552900 ko | Curves/Montgomery/Affine.vo 0m04.37s | 509740 ko | CastLemmas.vo 0m04.29s | 786004 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo 0m04.27s | 42800 ko | fiat-json/src/secp256k1_64.json 0m04.22s | 29948 ko | fiat-json/src/p448_solinas_64.json 0m04.14s | 535376 ko | Arithmetic/UniformWeight.vo 0m04.14s | 774888 ko | PushButtonSynthesis/SaturatedSolinas.vo 0m04.01s | 569084 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo 0m03.99s | 487152 ko | Util/ZUtil/LandLorShiftBounds.vo 0m03.82s | 505228 ko | Util/ZUtil/LandLorBounds.vo 0m03.75s | 486340 ko | Arithmetic/BarrettReduction/HAC.vo 0m03.58s | 416660 ko | Algebra/Group.vo 0m03.57s | 618260 ko | PushButtonSynthesis/BaseConversionReificationCache.vo 0m03.48s | 584112 ko | Rewriter/Passes/Test.vo 0m03.48s | 42656 ko | fiat-json/src/p224_64.json 0m03.46s | 31236 ko | fiat-go/64/p521/p521.go 0m03.39s | 791808 ko | CLI.vo 0m03.34s | 605072 ko | Rewriter/Passes/AddAssocLeft.vo 0m03.33s | 544744 ko | Assembly/Semantics.vo 0m03.33s | 43344 ko | fiat-json/src/p256_64.json 0m03.26s | 26128 ko | fiat-c/src/p521_64.c 0m03.22s | 26116 ko | fiat-rust/src/p521_64.rs 0m03.08s | 523284 ko | MiscCompilerPassesProofs.vo 0m03.00s | 488720 ko | Util/MSets/Iso.vo 0m02.92s | 598576 ko | Rewriter/Passes/FlattenThunkedRects.vo 0m02.87s | 24808 ko | fiat-zig/src/p521_64.zig 0m02.76s | 40420 ko | fiat-go/64/secp256k1/secp256k1.go 0m02.72s | 510380 ko | Spec/MontgomeryCurve.vo 0m02.70s | 46096 ko | fiat-rust/src/secp256k1_64.rs 0m02.67s | 39800 ko | fiat-zig/src/secp256k1_64.zig 0m02.63s | 43416 ko | fiat-c/src/secp256k1_64.c 0m02.59s | 479256 ko | Arithmetic/Primitives.vo 0m02.57s | 542176 ko | Arithmetic/Freeze.vo 0m02.52s | 613536 ko | Stringification/Language.vo 0m02.50s | 479628 ko | Util/ZUtil/Shift.vo 0m02.45s | 1323848 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo 0m02.41s | 475580 ko | Util/ZUtil/Div.vo 0m02.39s | 477872 ko | Util/ZUtil/ModInv.vo 0m02.33s | 595564 ko | Rewriter/Passes/UnfoldValueBarrier.vo 0m02.31s | 593588 ko | Rewriter/Passes/StripLiteralCasts.vo 0m02.26s | 526700 ko | Arithmetic/BaseConversion.vo 0m02.25s | 389416 ko | Util/Wf2.vo 0m02.25s | 472244 ko | Util/ZUtil/TwosComplement.vo 0m02.22s | 793628 ko | StandaloneOCamlMain.vo 0m02.20s | 793264 ko | StandaloneHaskellMain.vo 0m02.17s | 647496 ko | CompilersTestCases.vo 0m02.16s | 29324 ko | fiat-go/64/p448solinas/p448solinas.go 0m02.11s | 43816 ko | fiat-go/64/p224/p224.go 0m02.09s | 593380 ko | Rewriter/Passes/ToFancy.vo 0m02.07s | 513032 ko | Arithmetic/ModularArithmeticTheorems.vo 0m02.05s | 533944 ko | Arithmetic/ModOps.vo 0m02.05s | 467888 ko | Util/ZUtil/Testbit.vo 0m02.05s | 39200 ko | fiat-zig/src/p224_64.zig 0m02.04s | 43028 ko | fiat-c/src/p224_64.c 0m02.03s | 43140 ko | fiat-rust/src/p224_64.rs 0m02.02s | 40512 ko | fiat-zig/src/p256_64.zig 0m02.00s | 566928 ko | AbstractInterpretation/AbstractInterpretation.vo 0m02.00s | 40124 ko | fiat-rust/src/p256_64.rs 0m01.99s | 25816 ko | fiat-c/src/p448_solinas_64.c 0m01.99s | 24856 ko | fiat-rust/src/p448_solinas_64.rs 0m01.98s | 583324 ko | AbstractInterpretation/ZRange.vo 0m01.96s | 39300 ko | fiat-c/src/p256_64.c 0m01.95s | 40248 ko | fiat-go/64/p256/p256.go 0m01.95s | 24804 ko | fiat-zig/src/p448_solinas_64.zig 0m01.91s | 509460 ko | Assembly/Parse.vo 0m01.90s | 486968 ko | Util/ZUtil/Bitwise.vo 0m01.88s | 25044 ko | fiat-java/src/FiatCurve25519.java 0m01.87s | 458424 ko | Util/NatUtil.vo 0m01.85s | 580568 ko | Stringification/Go.vo 0m01.84s | 469740 ko | Util/Tuple.vo 0m01.82s | 24792 ko | fiat-c/src/curve25519_32.c 0m01.81s | 26208 ko | fiat-zig/src/curve25519_32.zig 0m01.80s | 24904 ko | fiat-go/32/curve25519/curve25519.go 0m01.78s | 24956 ko | fiat-rust/src/curve25519_32.rs 0m01.77s | 456796 ko | Rewriter/Util/NatUtil.vo 0m01.76s | 546892 ko | Arithmetic/PrimeFieldTheorems.vo 0m01.71s | 482108 ko | Spec/WeierstrassCurve.vo 0m01.68s | 579580 ko | Stringification/JSON.vo 0m01.67s | 599344 ko | Assembly/Equivalence.vo 0m01.67s | 466136 ko | Util/Bool/Reflect.vo 0m01.61s | 522616 ko | Rewriter/Language/IdentifiersLibrary.vo 0m01.61s | 492412 ko | Util/ZRange/SplitRangeBounds.vo 0m01.60s | 462756 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.vo 0m01.60s | 466444 ko | Rewriter/Util/Bool/Reflect.vo 0m01.59s | 576892 ko | Stringification/Zig.vo 0m01.58s | 463148 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised.vo 0m01.57s | 579564 ko | Stringification/C.vo 0m01.56s | 576172 ko | Stringification/Java.vo 0m01.51s | 464336 ko | Util/ZUtil/Pow2Mod.vo 0m01.50s | 450856 ko | Algebra/ScalarMult.vo 0m01.49s | 575660 ko | Stringification/Rust.vo 0m01.47s | 460804 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.vo 0m01.43s | 475316 ko | Util/ZUtil/Quot.vo 0m01.40s | 512592 ko | Arithmetic/Partition.vo 0m01.40s | 520508 ko | Rewriter/Rewriter/Rewriter.vo 0m01.40s | 484068 ko | Util/ZRange/SplitBounds.vo 0m01.38s | 493796 ko | Curves/Edwards/XYZT/Precomputed.vo 0m01.38s | 449344 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness.vo 0m01.32s | 447016 ko | Coqprime/PrimalityTest/EGroup 0m01.32s | 489920 ko | Fancy/Spec.vo 0m01.26s | 559640 ko | Language/APINotations.vo 0m01.26s | 519576 ko | Rewriter/Rewriter/Reify.vo 0m01.23s | 481708 ko | Rewriter/Language/Language.vo 0m01.22s | 615916 ko | Rewriter/All.vo 0m01.21s | 463596 ko | Util/ZUtil/Ones.vo 0m01.20s | 443904 ko | Util/ListUtil/Forall.vo 0m01.17s | 443628 ko | Rewriter/Util/ListUtil/Forall.vo 0m01.17s | 449144 ko | Util/ZUtil/Rshi.vo 0m01.16s | 557388 ko | PushButtonSynthesis/ReificationCache.vo 0m01.16s | 539956 ko | Rewriter/Rewriter/AllTactics.vo 0m01.15s | 559816 ko | AbstractInterpretation/WfExtra.vo 0m01.15s | 553972 ko | Language/WfExtra.vo 0m01.15s | 553076 ko | MiscCompilerPassesProofsExtra.vo 0m01.15s | 372288 ko | Util/Wf1.vo 0m01.13s | 452096 ko | Util/ZUtil/AddGetCarry.vo 0m01.11s | 479672 ko | Curves/Montgomery/AffineInstances.vo 0m01.11s | 464080 ko | Util/ZUtil/OnesFrom.vo 0m01.08s | 552128 ko | Language/API.vo 0m01.07s | 440672 ko | Coqprime/Z/ZCAux 0m01.07s | 554232 ko | Language/UnderLetsProofsExtra.vo 0m01.02s | 560652 ko | Rewriter/AllTacticsExtra.vo 0m01.00s | 482280 ko | Rewriter/Rules.vo 0m00.99s | 523948 ko | Rewriter/Rewriter/ProofsCommonTactics.vo 0m00.99s | 451068 ko | Util/Strings/String_as_OT.vo 0m00.95s | 23396 ko | fiat-json/src/curve25519_64.json 0m00.93s | 447144 ko | Algebra/NsatzTactic.vo 0m00.91s | 508488 ko | Rewriter/Language/IdentifiersGenerate.vo 0m00.90s | 469888 ko | Arithmetic/BarrettReduction/Wikipedia.vo 0m00.90s | 506608 ko | MiscCompilerPasses.vo 0m00.90s | 534468 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo 0m00.87s | 473464 ko | Util/NumTheoryUtil.vo 0m00.86s | 442288 ko | Coqprime/Z/ZSum 0m00.86s | 531716 ko | Rewriter/Util/plugins/RewriterBuild.vo 0m00.85s | 509152 ko | ArithmeticCPS/Freeze.vo 0m00.85s | 466504 ko | Util/ZUtil/TruncatingShiftl.vo 0m00.83s | 460260 ko | Algebra/IntegralDomain.vo 0m00.83s | 508464 ko | Rewriter/Language/IdentifiersGenerateProofs.vo 0m00.82s | 507064 ko | ArithmeticCPS/WordByWordMontgomery.vo 0m00.81s | 531088 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo 0m00.81s | 459596 ko | Util/CPSUtil.vo 0m00.80s | 445216 ko | Coqprime/PrimalityTest/Cyclic 0m00.80s | 473944 ko | Util/Arg.vo 0m00.78s | 529540 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo 0m00.78s | 488636 ko | Util/QUtil.vo 0m00.77s | 503524 ko | ArithmeticCPS/ModOps.vo 0m00.77s | 419020 ko | Coqprime/PrimalityTest/Root 0m00.77s | 322204 ko | Util/PartiallyReifiedProp.vo 0m00.77s | 477548 ko | Util/ZRange/OperationsBounds.vo 0m00.77s | 466460 ko | Util/ZUtil/CC.vo 0m00.75s | 448392 ko | Rewriter/Rewriter/Examples/PerfTesting/Sample.vo 0m00.74s | 503480 ko | ArithmeticCPS/BaseConversion.vo 0m00.73s | 493804 ko | ArithmeticCPS/Core.vo 0m00.73s | 491652 ko | ArithmeticCPS/Saturated.vo 0m00.72s | 485092 ko | Assembly/Equality.vo 0m00.71s | 461184 ko | Algebra/SubsetoidRing.vo 0m00.71s | 441596 ko | Util/OptionList.vo 0m00.68s | 439640 ko | Util/Loops.vo 0m00.68s | 440168 ko | Util/ZUtil/Modulo/PullPush.vo 0m00.68s | 467216 ko | Util/ZUtil/Stabilization.vo 0m00.67s | 400300 ko | Util/Structures/Orders/Sum.vo 0m00.66s | 457296 ko | Util/Decidable/Decidable2Bool.vo 0m00.66s | 447236 ko | Util/ZUtil/Ltz.vo 0m00.65s | 445568 ko | Coqprime/PrimalityTest/Zp 0m00.64s | 489572 ko | Util/MSetPositive/Show.vo 0m00.63s | 467548 ko | Util/Strings/NamingConventions.vo 0m00.63s | 453656 ko | Util/Strings/ParseArithmetic.vo 0m00.60s | 475788 ko | Rewriter/Language/IdentifiersBasicGenerate.vo 0m00.59s | 450284 ko | Util/Strings/ParseArithmeticToTaps.vo 0m00.58s | 397472 ko | Util/Decidable.vo 0m00.58s | 457856 ko | Util/ZUtil/Log2.vo 0m00.57s | 469508 ko | Util/ZUtil/SignBit.vo 0m00.56s | 23468 ko | fiat-go/64/curve25519/curve25519.go 0m00.55s | 469636 ko | Arithmetic/ModularArithmeticPre.vo 0m00.54s | 454468 ko | Util/Level.vo 0m00.54s | 463188 ko | Util/Strings/Show.vo 0m00.54s | 369764 ko | Util/Wf.vo 0m00.54s | 457860 ko | Util/ZBounded.vo 0m00.53s | 458488 ko | Spec/CompleteEdwardsCurve.vo 0m00.53s | 443612 ko | Util/Strings/Sorting.vo 0m00.53s | 461624 ko | Util/ZUtil/Land.vo 0m00.52s | 397296 ko | Rewriter/Util/Decidable.vo 0m00.52s | 456444 ko | Util/HList.vo 0m00.51s | 471512 ko | Rewriter/TestRules.vo 0m00.51s | 449888 ko | Util/MSetPositive/Facts.vo 0m00.51s | 457192 ko | Util/ZRange.vo 0m00.50s | 462380 ko | Curves/Montgomery/XZ.vo 0m00.50s | 457772 ko | Curves/Weierstrass/Affine.vo 0m00.50s | 454808 ko | Util/Listable.vo 0m00.50s | 21024 ko | fiat-c/src/curve25519_64.c 0m00.50s | 21056 ko | fiat-rust/src/curve25519_64.rs 0m00.49s | 447844 ko | Rewriter/Util/Strings/ParseArithmetic.vo 0m00.49s | 442660 ko | Util/ZUtil/CPS.vo 0m00.48s | 471192 ko | Language/IdentifierParameters.vo 0m00.48s | 468940 ko | Rewriter/Language/UnderLets.vo 0m00.48s | 461224 ko | Util/ZUtil/EquivModulo.vo 0m00.48s | 464884 ko | Util/ZUtil/Tactics/SolveRange.vo 0m00.48s | 22504 ko | fiat-json/src/poly1305_32.json 0m00.48s | 21084 ko | fiat-zig/src/curve25519_64.zig 0m00.47s | 439784 ko | Coqprime/PrimalityTest/Euler 0m00.47s | 469980 ko | Rewriter/TestRulesProofs.vo 0m00.47s | 420476 ko | Util/Strings/String_as_OT_old.vo 0m00.47s | 399408 ko | Util/Sum.vo 0m00.47s | 458004 ko | Util/ZRange/Operations.vo 0m00.47s | 487360 ko | Util/ZUtil.vo 0m00.46s | 416128 ko | Coqprime/PrimalityTest/Lagrange 0m00.46s | 467664 ko | Language/PreExtra.vo 0m00.46s | 397100 ko | Rewriter/Util/Sum.vo 0m00.46s | 461316 ko | Util/ZUtil/Divide.vo 0m00.45s | 448808 ko | Rewriter/Util/MSetPositive/Facts.vo 0m00.45s | 467860 ko | Util/MSets/Show.vo 0m00.45s | 454696 ko | Util/ZUtil/Pow.vo 0m00.44s | 404732 ko | Coqprime/List/UList 0m00.44s | 430812 ko | Util/ZUtil/Tactics.vo 0m00.43s | 404204 ko | Coqprime/List/Permutation 0m00.43s | 457096 ko | Util/AdditionChainExponentiation.vo 0m00.43s | 465024 ko | Util/ErrorT/Show.vo 0m00.43s | 436720 ko | Util/Strings/String.vo 0m00.43s | 461948 ko | Util/ZUtil/Tactics/SolveTestbit.vo 0m00.42s | 414984 ko | Coqprime/PrimalityTest/IGroup 0m00.42s | 436804 ko | Rewriter/Util/Strings/String.vo 0m00.42s | 444348 ko | Util/ZUtil/Combine.vo 0m00.42s | 461608 ko | Util/ZUtil/Lor.vo 0m00.41s | 438632 ko | Coqprime/List/ZProgression 0m00.41s | 466416 ko | Util/ZRange/Show.vo 0m00.40s | 441464 ko | Spec/ModularArithmetic.vo 0m00.40s | 426740 ko | Util/MSetPositive/Equality.vo 0m00.40s | 437660 ko | Util/ZUtil/Peano.vo 0m00.39s | 418824 ko | Algebra/Nsatz.vo 0m00.39s | 441376 ko | Util/NUtil/WithoutReferenceToZ.vo 0m00.39s | 424264 ko | Util/ZUtil/Tactics/Ztestbit.vo 0m00.38s | 428832 ko | Arithmetic/MontgomeryReduction/Definition.vo 0m00.38s | 439536 ko | Util/ZUtil/Le.vo 0m00.38s | 438344 ko | Util/ZUtil/Tactics/LtbToLt.vo 0m00.37s | 402900 ko | Coqprime/List/ListAux 0m00.37s | 412112 ko | Util/IdfunWithAlt.vo 0m00.37s | 384060 ko | Util/SideConditions/ModInvPackage.vo 0m00.37s | 419300 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo 0m00.37s | 415832 ko | Util/ZUtil/Tactics/ZeroBounds.vo 0m00.36s | 426216 ko | Rewriter/Util/MSetPositive/Equality.vo 0m00.36s | 402532 ko | Util/ZUtil/Tactics/RewriteModSmall.vo 0m00.35s | 425712 ko | Util/Strings/StringMap.vo 0m00.34s | 394312 ko | Util/ZUtil/MulSplit.vo 0m00.33s | 367916 ko | Util/Strings/Parse/Common.vo 0m00.33s | 342284 ko | Util/ZUtil/Hints/Ztestbit.vo 0m00.33s | 378096 ko | Util/ZUtil/Sgn.vo 0m00.32s | 404204 ko | Coqprime/List/Iterator 0m00.32s | 312496 ko | Rewriter/Util/Option.vo 0m00.32s | 369692 ko | Util/Factorize.vo 0m00.32s | 357700 ko | Util/ZUtil/DistrIf.vo 0m00.32s | 345896 ko | Util/ZUtil/Hints.vo 0m00.32s | 343492 ko | Util/ZUtil/Hints/ZArith.vo 0m00.32s | 378708 ko | Util/ZUtil/N2Z.vo 0m00.32s | 382708 ko | Util/ZUtil/Nat2Z.vo 0m00.32s | 355432 ko | Util/ZUtil/Sorting.vo 0m00.32s | 399724 ko | Util/ZUtil/Z2Nat.vo 0m00.31s | 343916 ko | Util/ZUtil/Hints/Core.vo 0m00.31s | 348960 ko | Util/ZUtil/ModExp.vo 0m00.31s | 372036 ko | Util/ZUtil/Odd.vo 0m00.31s | 349424 ko | Util/ZUtil/Opp.vo 0m00.31s | 374168 ko | Util/ZUtil/Tactics/LinearSubstitute.vo 0m00.31s | 342236 ko | Util/ZUtil/Tactics/PeelLe.vo 0m00.31s | 348300 ko | Util/ZUtil/Tactics/PullPush/Modulo.vo 0m00.30s | 403932 ko | Rewriter/Language/PreLemmas.vo 0m00.30s | 347368 ko | Rewriter/Util/Strings/Parse/Common.vo 0m00.30s | 372252 ko | Util/FMapPositive/Equality.vo 0m00.30s | 343324 ko | Util/ZUtil/Div/Bootstrap.vo 0m00.30s | 347364 ko | Util/ZUtil/Lnot.vo 0m00.30s | 367256 ko | Util/ZUtil/Pow2.vo 0m00.30s | 345840 ko | Util/ZUtil/Tactics/ReplaceNegWithPos.vo 0m00.30s | 340484 ko | Util/ZUtil/Tactics/SplitMinMax.vo 0m00.30s | 411064 ko | Util/ZUtil/ZSimplify/Simple.vo 0m00.29s | 399684 ko | Algebra/Monoid.vo 0m00.29s | 373884 ko | Coqprime/PrimalityTest/FGroup 0m00.29s | 312716 ko | Util/Option.vo 0m00.29s | 359864 ko | Util/SideConditions/Autosolve.vo 0m00.29s | 351924 ko | Util/ZUtil/Hints/PullPush.vo 0m00.29s | 342396 ko | Util/ZUtil/Mul.vo 0m00.28s | 362040 ko | TAPSort.vo 0m00.28s | 356256 ko | Util/ZUtil/Modulo/Bootstrap.vo 0m00.28s | 343476 ko | Util/ZUtil/Tactics/DivModToQuotRem.vo 0m00.28s | 339108 ko | Util/ZUtil/Tactics/DivideExistsMul.vo 0m00.28s | 318228 ko | Util/ZUtil/ZSimplify.vo 0m00.27s | 299788 ko | Rewriter/Util/Strings/Decimal.vo 0m00.27s | 348184 ko | Util/ZUtil/ZSimplify/Core.vo 0m00.26s | 367084 ko | Rewriter/Util/FMapPositive/Equality.vo 0m00.26s | 331272 ko | Util/ZUtil/Definitions.vo 0m00.25s | 295228 ko | PushButtonSynthesis/InvertHighLow.vo 0m00.25s | 352652 ko | Util/ListUtil/FoldBool.vo 0m00.25s | 354448 ko | Util/ListUtil/SetoidList.vo 0m00.25s | 298356 ko | Util/SideConditions/RingPackage.vo 0m00.25s | 304756 ko | Util/Strings/Decimal.vo 0m00.25s | 312824 ko | Util/ZUtil/Tactics/PullPush.vo 0m00.25s | 319540 ko | Util/ZUtil/Zselect.vo 0m00.25s | 20068 ko | fiat-java/src/FiatPoly1305.java 0m00.25s | 20600 ko | fiat-json/src/poly1305_64.json 0m00.24s | 309752 ko | Algebra/Hierarchy.vo 0m00.24s | 311876 ko | Util/PointedProp.vo 0m00.24s | 290120 ko | Util/ZUtil/Tactics/CompareToSgn.vo 0m00.24s | 304528 ko | Util/ZUtil/Tactics/PrimeBound.vo 0m00.24s | 20504 ko | fiat-zig/src/poly1305_32.zig 0m00.23s | 279804 ko | Util/Strings/Ascii.vo 0m00.23s | 326420 ko | Util/Structures/Equalities/Sum.vo 0m00.23s | 309872 ko | Util/ZUtil/AddModulo.vo 0m00.23s | 19820 ko | fiat-c/src/poly1305_32.c 0m00.22s | 306528 ko | Coqprime/N/NatAux 0m00.22s | 311944 ko | Util/ZUtil/Ge.vo 0m00.22s | 20080 ko | fiat-rust/src/poly1305_32.rs 0m00.21s | 340408 ko | Rewriter/Util/OptionList.vo 0m00.21s | 273076 ko | Rewriter/Util/Strings/Ascii.vo 0m00.21s | 20068 ko | fiat-go/32/poly1305/poly1305.go 0m00.20s | 262900 ko | Util/Decidable/Bool2Prop.vo 0m00.20s | 302984 ko | Util/LetInMonad.vo 0m00.20s | 240680 ko | Util/ParseTaps.vo 0m00.20s | 309600 ko | Util/ZUtil/LnotModulo.vo 0m00.19s | 276016 ko | Spec/MxDH.vo 0m00.19s | 269772 ko | Util/ListUtil/NthExt.vo 0m00.18s | 229792 ko | Util/ZUtil/Notations.vo 0m00.17s | 248560 ko | Util/SideConditions/ReductionPackages.vo 0m00.17s | 240532 ko | Util/Sigma.vo 0m00.15s | 263912 ko | Util/Prod.vo 0m00.15s | 19816 ko | fiat-go/64/poly1305/poly1305.go 0m00.14s | 259760 ko | Rewriter/Util/Prod.vo 0m00.14s | 235636 ko | Rewriter/Util/Sigma.vo 0m00.14s | 273156 ko | Util/Telescope/Equality.vo 0m00.14s | 193176 ko | Util/Telescope/Instances.vo 0m00.13s | 172084 ko | Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo 0m00.13s | 219788 ko | Util/ListUtil/ForallIn.vo 0m00.13s | 19424 ko | fiat-c/src/poly1305_64.c 0m00.13s | 19236 ko | fiat-zig/src/poly1305_64.zig 0m00.12s | 165508 ko | Util/PrimitiveSigma.vo 0m00.12s | 19452 ko | fiat-rust/src/poly1305_64.rs 0m00.11s | 140384 ko | Rewriter/Util/Equality.vo 0m00.11s | 203680 ko | Rewriter/Util/ListUtil/SetoidList.vo 0m00.11s | 160276 ko | Rewriter/Util/PrimitiveSigma.vo 0m00.11s | 156976 ko | Util/PrimitiveHList.vo 0m00.10s | 160356 ko | Rewriter/Language/Pre.vo 0m00.10s | 154728 ko | Rewriter/Language/PreCommon.vo 0m00.10s | 192512 ko | Rewriter/Util/PrimitiveProd.vo 0m00.10s | 157660 ko | Util/Bool.vo 0m00.10s | 197864 ko | Util/PrimitiveProd.vo 0m00.10s | 146172 ko | Util/Tactics/AllSuccesses.vo 0m00.09s | 152024 ko | Rewriter/Util/PrimitiveHList.vo 0m00.09s | 145440 ko | Util/Equality.vo 0m00.09s | 189188 ko | Util/Relations.vo 0m00.09s | 118404 ko | Util/Structures/Equalities/Iso.vo 0m00.09s | 166272 ko | Util/Tactics.vo 0m00.09s | 147180 ko | Util/Tactics/AllInstances.vo 0m00.09s | 157184 ko | Util/TagList.vo 0m00.08s | 149268 ko | Util/DynList.vo 0m00.08s | 118132 ko | Util/Sigma/Related.vo 0m00.07s | 112776 ko | Rewriter/Util/Sigma/Related.vo 0m00.07s | 84972 ko | Rewriter/Util/Tactics/RewriteHyp.vo 0m00.07s | 91364 ko | Util/Structures/Orders.vo 0m00.07s | 105976 ko | Util/Structures/Orders/Iso.vo 0m00.07s | 102120 ko | Util/Telescope/Core.vo 0m00.06s | 134120 ko | Rewriter/Util/Bool.vo 0m00.06s | 77372 ko | Util/CPSNotations.vo 0m00.06s | 101192 ko | Util/Compose.vo 0m00.06s | 93952 ko | Util/HProp.vo 0m00.06s | 92956 ko | Util/LetIn.vo 0m00.06s | 102004 ko | Util/Logic/ExistsEqAnd.vo 0m00.05s | 88592 ko | Rewriter/Util/HProp.vo 0m00.05s | 78940 ko | Rewriter/Util/IffT.vo 0m00.05s | 78960 ko | Rewriter/Util/Logic/ProdForall.vo 0m00.05s | 69416 ko | Rewriter/Util/Tactics/BreakMatch.vo 0m00.05s | 65696 ko | Rewriter/Util/Tactics/DebugPrint.vo 0m00.05s | 67296 ko | Rewriter/Util/Tactics/DestructHyps.vo 0m00.05s | 65196 ko | Rewriter/Util/Tactics/Head.vo 0m00.05s | 65444 ko | Rewriter/Util/Tactics/RunTacticAsConstr.vo 0m00.05s | 82996 ko | Util/AutoRewrite.vo 0m00.05s | 76908 ko | Util/FixCoqMistakes.vo 0m00.05s | 62580 ko | Util/GlobalSettings.vo 0m00.05s | 84056 ko | Util/IffT.vo 0m00.05s | 86660 ko | Util/Logic.vo 0m00.05s | 70644 ko | Util/Logic/ImplAnd.vo 0m00.05s | 83244 ko | Util/Notations.vo 0m00.05s | 72428 ko | Util/SideConditions/CorePackages.vo 0m00.05s | 83076 ko | Util/Sigma/Lift.vo 0m00.05s | 65192 ko | Util/Sigma/MapProjections.vo 0m00.05s | 87752 ko | Util/Sumbool.vo 0m00.05s | 74852 ko | Util/Tactics/BreakMatch.vo 0m00.05s | 63224 ko | Util/Tactics/ClearAll.vo 0m00.05s | 70668 ko | Util/Tactics/DebugPrint.vo 0m00.05s | 79100 ko | Util/Tactics/DestructHead.vo 0m00.05s | 64488 ko | Util/Tactics/SetoidSubst.vo 0m00.05s | 71320 ko | Util/Tactics/SpecializeBy.vo 0m00.05s | 64560 ko | Util/Tactics/UnifyAbstractReflexivity.vo 0m00.05s | 83912 ko | Util/Tower.vo 0m00.05s | 71720 ko | Util/Unit.vo 0m00.04s | 68676 ko | Rewriter/Util/Bool/Equality.vo 0m00.04s | 72592 ko | Rewriter/Util/CPSNotations.vo 0m00.04s | 71736 ko | Rewriter/Util/Comparison.vo 0m00.04s | 71976 ko | Rewriter/Util/FixCoqMistakes.vo 0m00.04s | 96444 ko | Rewriter/Util/Logic/ExistsEqAnd.vo 0m00.04s | 78268 ko | Rewriter/Util/Notations.vo 0m00.04s | 82312 ko | Rewriter/Util/Pointed.vo 0m00.04s | 65168 ko | Rewriter/Util/Tactics/AssertSucceedsPreserveError.vo 0m00.04s | 61020 ko | Rewriter/Util/Tactics/CacheTerm.vo 0m00.04s | 73740 ko | Rewriter/Util/Tactics/DestructHead.vo 0m00.04s | 57892 ko | Rewriter/Util/Tactics/EvarNormalize.vo 0m00.04s | 58024 ko | Rewriter/Util/Tactics/Not.vo 0m00.04s | 65440 ko | Rewriter/Util/Tactics/SpecializeAllWays.vo 0m00.04s | 59852 ko | Rewriter/Util/TypeList.vo 0m00.04s | 73660 ko | Util/Bool/Equality.vo 0m00.04s | 65244 ko | Util/Bool/IsTrue.vo 0m00.04s | 77168 ko | Util/Comparison.vo 0m00.04s | 76776 ko | Util/ErrorT.vo 0m00.04s | 64452 ko | Util/Isomorphism.vo 0m00.04s | 73892 ko | Util/Logic/Exists.vo 0m00.04s | 76272 ko | Util/Logic/Forall.vo 0m00.04s | 74472 ko | Util/PER.vo 0m00.04s | 87468 ko | Util/Pointed.vo 0m00.04s | 64952 ko | Util/Pos.vo 0m00.04s | 70124 ko | Util/Tactics/AppendUnderscores.vo 0m00.04s | 65512 ko | Util/Tactics/CPSId.vo 0m00.04s | 63296 ko | Util/Tactics/ChangeInAll.vo 0m00.04s | 63380 ko | Util/Tactics/ClearDuplicates.vo 0m00.04s | 63168 ko | Util/Tactics/ConstrFail.vo 0m00.04s | 63204 ko | Util/Tactics/Contains.vo 0m00.04s | 70920 ko | Util/Tactics/CountBinders.vo 0m00.04s | 72256 ko | Util/Tactics/DestructHyps.vo 0m00.04s | 70680 ko | Util/Tactics/DoWithHyp.vo 0m00.04s | 63096 ko | Util/Tactics/ESpecialize.vo 0m00.04s | 62888 ko | Util/Tactics/EvarExists.vo 0m00.04s | 63720 ko | Util/Tactics/Forward.vo 0m00.04s | 62924 ko | Util/Tactics/GetGoal.vo 0m00.04s | 62820 ko | Util/Tactics/HasBody.vo 0m00.04s | 70608 ko | Util/Tactics/HeadUnderBinders.vo 0m00.04s | 75048 ko | Util/Tactics/MoveLetIn.vo 0m00.04s | 63496 ko | Util/Tactics/Not.vo 0m00.04s | 63408 ko | Util/Tactics/PrintGoal.vo 0m00.04s | 62988 ko | Util/Tactics/Revert.vo 0m00.04s | 90228 ko | Util/Tactics/RewriteHyp.vo 0m00.04s | 63108 ko | Util/Tactics/SetEvars.vo 0m00.04s | 64360 ko | Util/Tactics/SimplifyProjections.vo 0m00.04s | 70764 ko | Util/Tactics/SpecializeAllWays.vo 0m00.04s | 71628 ko | Util/Tactics/SplitInContext.vo 0m00.04s | 63036 ko | Util/Tactics/SubstLet.vo 0m00.04s | 63832 ko | Util/Tactics/TransparentAssert.vo 0m00.04s | 63488 ko | Util/Tactics/UnfoldArg.vo 0m00.03s | 58900 ko | Coqprime/Tactic/Tactic 0m00.03s | 61420 ko | Rewriter/Util/InductiveHList.vo 0m00.03s | 94276 ko | Rewriter/Util/LetIn.vo 0m00.03s | 60264 ko | Rewriter/Util/Tactics/CPSId.vo 0m00.03s | 58040 ko | Rewriter/Util/Tactics/ConstrFail.vo 0m00.03s | 58052 ko | Rewriter/Util/Tactics/Contains.vo 0m00.03s | 65544 ko | Rewriter/Util/Tactics/DoWithHyp.vo 0m00.03s | 57728 ko | Rewriter/Util/Tactics/GetGoal.vo 0m00.03s | 65400 ko | Rewriter/Util/Tactics/HeadUnderBinders.vo 0m00.03s | 57764 ko | Rewriter/Util/Tactics/SetEvars.vo 0m00.03s | 66520 ko | Rewriter/Util/Tactics/SplitInContext.vo 0m00.03s | 57820 ko | Rewriter/Util/Tactics/Test.vo 0m00.03s | 58620 ko | Rewriter/Util/Tactics/TransparentAssert.vo 0m00.03s | 65848 ko | Rewriter/Util/Tactics/UniquePose.vo 0m00.03s | 57988 ko | Rewriter/Util/Tactics/WarnIfGoalsRemain.vo 0m00.03s | 63164 ko | Util/ChangeInAll.vo 0m00.03s | 66928 ko | Util/Curry.vo 0m00.03s | 63356 ko | Util/DefaultedTypes.vo 0m00.03s | 63652 ko | Util/FueledLUB.vo 0m00.03s | 83900 ko | Util/Logic/ProdForall.vo 0m00.03s | 65640 ko | Util/Sigma/Associativity.vo 0m00.03s | 65992 ko | Util/Tactics/CacheTerm.vo 0m00.03s | 62964 ko | Util/Tactics/ClearbodyAll.vo 0m00.03s | 64008 ko | Util/Tactics/ConvoyDestruct.vo 0m00.03s | 63368 ko | Util/Tactics/DestructTrivial.vo 0m00.03s | 68848 ko | Util/Tactics/ETransitivity.vo 0m00.03s | 63300 ko | Util/Tactics/EvarNormalize.vo 0m00.03s | 70528 ko | Util/Tactics/Head.vo 0m00.03s | 63272 ko | Util/Tactics/NormalizeCommutativeIdentifier.vo 0m00.03s | 63056 ko | Util/Tactics/OnSubterms.vo 0m00.03s | 63108 ko | Util/Tactics/PoseTermWithName.vo 0m00.03s | 63364 ko | Util/Tactics/PrintContext.vo 0m00.03s | 70372 ko | Util/Tactics/RunTacticAsConstr.vo 0m00.03s | 63244 ko | Util/Tactics/SideConditionsBeforeToAfter.vo 0m00.03s | 63388 ko | Util/Tactics/SimplifyRepeatedIfs.vo 0m00.03s | 62820 ko | Util/Tactics/Test.vo 0m00.03s | 71188 ko | Util/Tactics/UniquePose.vo 0m00.03s | 64140 ko | Util/Tactics/VM.vo 0m00.02s | 58128 ko | Rewriter/Util/Tactics/PrintContext.vo 0m00.02s | 57996 ko | Rewriter/Util/Tactics/PrintGoal.vo 0m00.02s | 59268 ko | Rewriter/Util/Tactics/SetoidSubst.vo 0m00.02s | 66184 ko | Rewriter/Util/Tactics/SpecializeBy.vo 0m00.01s | 57028 ko | Rewriter/Util/GlobalSettings.vo 0m00.01s | 58944 ko | Rewriter/Util/Isomorphism.vo 0m00.01s | 57620 ko | Rewriter/Util/Tactics/SubstEvars.vo 0m00.01s | 57968 ko | Rewriter/Util/plugins/StrategyTactic.vo 0m00.01s | 63164 ko | Util/Tactics/SubstEvars.vo ``` </p> </details> | 15 July 2021, 00:28:56 UTC |
| 58622d4 | Jason Gross | 24 January 2021, 17:33:10 UTC | Don't exclude log files | 15 July 2021, 00:28:56 UTC |
| 38c52b7 | Jason Gross | 24 January 2021, 17:32:15 UTC | Enable testing | 15 July 2021, 00:28:56 UTC |
| 24f0791 | Jason Gross | 15 July 2021, 00:27:02 UTC | Clean up more in the Makefile | 15 July 2021, 00:28:47 UTC |
| 015fb71 | Jason Gross | 15 July 2021, 00:25:18 UTC | Be more permissive in reading rows This fixes errors, though I haven't dug into them carefully | 15 July 2021, 00:28:45 UTC |
| 35d1ff5 | Jason Gross | 14 July 2021, 22:55:20 UTC | Add show for sum | 14 July 2021, 22:55:44 UTC |
| f5e3ed4 | Jason Gross | 09 July 2021, 04:01:35 UTC | Merge pull request #1000 from herbelin/master+adapt-coq-pr14596-show-all-names-about Remove the Arguments line from the tested output of Print | 09 July 2021, 04:01:35 UTC |
| eab54d1 | Jason Gross | 09 July 2021, 04:01:09 UTC | Merge branch 'master' into master+adapt-coq-pr14596-show-all-names-about | 09 July 2021, 04:01:09 UTC |
| afcb17c | Jason Gross | 07 July 2021, 15:07:28 UTC | Improve output test display, hopefully Should help with https://github.com/coq/coq/pull/14596#issuecomment-875581896 | 07 July 2021, 15:07:28 UTC |
| 4aa6941 | Hugo Herbelin | 07 July 2021, 12:51:52 UTC | Remove the Arguments line from the tested output of Print | 07 July 2021, 12:52:37 UTC |
| d01ef61 | Jason Gross | 03 July 2021, 15:31:18 UTC | Better error messages about expected functions | 03 July 2021, 15:31:18 UTC |
| a92163f | Jason Gross | 03 July 2021, 15:23:49 UTC | Fix a missing negation We want to return the assembly functions not matched by anything requested, for the error messages. We were missing a negation in filtering before. Oops. | 03 July 2021, 15:23:49 UTC |
| bccc816 | Frank Denis | 28 June 2021, 23:29:17 UTC | inversion/zig: remove redundant comptime Fixes #997 | 01 July 2021, 01:26:46 UTC |
| 3d7c408 | Jason Gross | 28 June 2021, 20:45:50 UTC | Fix lingering xargs | 28 June 2021, 20:46:10 UTC |
| 612519f | Jason Gross | 28 June 2021, 17:28:29 UTC | Don't invoke to_csv.py multiple times | 28 June 2021, 17:29:27 UTC |
| c3d1b2c | Jason Gross | 28 June 2021, 14:33:55 UTC | Add lineterminator to csv generator | 28 June 2021, 14:33:55 UTC |
| 9ea76a9 | Jason Gross | 28 June 2021, 14:29:00 UTC | Add nlimbs column in perf.csv | 28 June 2021, 14:31:09 UTC |
| fad0119 | Jason Gross | 28 June 2021, 14:10:06 UTC | Update file writing to avoid error make: execvp: /bin/sh: Argument list too long | 28 June 2021, 14:10:06 UTC |
| f549083 | Frank Denis | 16 June 2021, 22:46:54 UTC | Zig: emulate unsafe casts Unsafe c-like casts have been removed from the language (or, rather, moved to a dark corner). So, include code to emulate them by upcasting or downcasting at compile time according to the source and target bit sizes. | 17 June 2021, 19:06:49 UTC |
| 279c6fe | Andres Erbsen | 07 June 2021, 14:50:21 UTC | Merge pull request #991 from mit-plv/bump-rupicola Bump rupicola | 07 June 2021, 14:50:21 UTC |
| 554888c | Andres Erbsen | 07 June 2021, 01:21:27 UTC | make accept-Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body | 07 June 2021, 01:21:27 UTC |
| b65f249 | Andres Erbsen | 06 June 2021, 12:07:05 UTC | accept-Crypto.Bedrock.Group.ScalarMult.LadderStep.ladderstep_body | 06 June 2021, 12:07:05 UTC |
| dd1a933 | Andres Erbsen | 06 June 2021, 01:43:53 UTC | port X25519 examples | 06 June 2021, 01:43:53 UTC |
| 48a4980 | Emil Bremer Orloff | 04 June 2021, 06:18:43 UTC | Run 'make java-files' | 04 June 2021, 23:48:07 UTC |
| 2d00e34 | Emil Bremer Orloff | 03 June 2021, 13:22:25 UTC | Remove --only-signed when generating java sources. Reintroduce use of Box and change the static cast to match | 04 June 2021, 23:48:07 UTC |
| 1aa4bf1 | Emil Bremer Orloff | 04 May 2021, 11:12:53 UTC | Removed usage of Box ín favor of int/long arrays. Changed how static casts are handled. | 04 June 2021, 23:48:07 UTC |
| 050b87a | Andres Erbsen | 04 June 2021, 20:13:19 UTC | port Signature.v and some UnsaturatedSolinas.v | 04 June 2021, 20:13:19 UTC |
| 49d5f01 | Andres Erbsen | 04 June 2021, 15:35:02 UTC | port binop fiat-crypto -> bedrock2 translation | 04 June 2021, 15:38:08 UTC |
| 42515b4 | Kris Kwiatkowski | 02 June 2021, 10:10:02 UTC | README: adds jq as dependency | 02 June 2021, 12:03:13 UTC |
| 44530ba | Kris Kwiatkowski | 02 June 2021, 09:48:15 UTC | README: adds ocalm-zarith as dependency | 02 June 2021, 12:03:13 UTC |
| b2d5e2a | Jason Gross | 24 May 2021, 12:42:05 UTC | Fix for Coq 8.9 | 27 May 2021, 12:18:24 UTC |
| 6b0368f | Jason Gross | 24 May 2021, 12:04:16 UTC | Fix for older versions of Coq | 27 May 2021, 12:18:24 UTC |
| 3068c33 | Jason Gross | 20 May 2021, 17:33:59 UTC | Add some proofs about `Z.modinv` | 27 May 2021, 12:18:24 UTC |
| d72f58c | Frank Denis | 26 May 2021, 18:34:13 UTC | Zig backend: favor "inline fn" over "fn ... callconv(.Inline)" Both are equivalent, but the former is now preferred. No functional changes. | 27 May 2021, 01:39:05 UTC |
| 94919dc | Jason Gross | 26 May 2021, 19:24:13 UTC | Get rid of dead code in gh-actions make _CoqProject is now generated | 26 May 2021, 19:24:13 UTC |
| 3e81b29 | Jason Gross | 26 April 2021, 16:49:31 UTC | Finish up PHOAS-interaction | 26 May 2021, 18:32:39 UTC |
| 235a3a9 | Jason Gross | 26 April 2021, 16:51:31 UTC | Better inferface for PHOAS equivalence interaction Co-authored-by: Andres Erbsen <andreser@mit.edu> | 26 May 2021, 18:32:39 UTC |
| 418eb6a | Jason Gross | 09 April 2021, 22:11:04 UTC | Infer the stack size from the code | 26 May 2021, 18:32:39 UTC |
| 41d5df5 | Jason Gross | 20 May 2021, 01:17:42 UTC | Regenerate files | 25 May 2021, 18:04:59 UTC |
| 2aa891b | Jason Gross | 19 May 2021, 14:26:25 UTC | Fix Zig casing | 25 May 2021, 18:04:59 UTC |
| 3302d83 | Jason Gross | 19 May 2021, 02:02:21 UTC | Improve Go code | 25 May 2021, 18:04:59 UTC |
| 468489d | Jason Gross | 18 May 2021, 20:38:23 UTC | Fix for Coq 8.9 | 25 May 2021, 18:04:59 UTC |
| d3638c4 | Jason Gross | 18 May 2021, 19:53:35 UTC | Add Zig typedefs | 25 May 2021, 18:04:59 UTC |
| 11af3c5 | Jason Gross | 18 May 2021, 15:52:20 UTC | Add synthesis of relax Now it makes sense, since we're using typedefs | 25 May 2021, 18:04:59 UTC |
| aafdb40 | Jason Gross | 14 May 2021, 00:21:04 UTC | Add named typedefs Questions: - [ ] Which divstep things belong in the montgomery domain? - [ ] What should we do about the various other kinds of bounds (saturated, bytes, etc)? - [x] Should we synthesize relax? (Current answer: Yes) - [ ] What should we do about selectznz? (should it take tight fe, loose fe, saturated fe; should we have a variant of saturated_relax that goes from loose to saturated?) | 25 May 2021, 18:04:59 UTC |
| e18dad9 | Andres Erbsen | 25 May 2021, 16:51:01 UTC | Merge remote-tracking branch 'jadep/update-rupicola' into bump-rupicola - disable rupicola derivation of Montgomery ladder and its uses, to be fixed after ladderstep uses stackalloc internally. that work is now unblocked. - break bedrock2-based CLI code generation, or at least I think that's what src/Bedrock/Field/Synthesis/New/Signature.v is for. I don't know what the plan for this is yet. | 25 May 2021, 16:51:01 UTC |
| e3060c1 | Andres Erbsen | 25 May 2021, 15:59:42 UTC | update for newer bedrock2 | 25 May 2021, 15:59:42 UTC |
| 59f5484 | Clément Pit-Claudel | 23 May 2021, 22:08:57 UTC | Bump Rupicola | 23 May 2021, 22:08:57 UTC |
| 7602507 | Jason Gross | 19 May 2021, 19:02:48 UTC | Work around Coq Haskell Extraction issue https://github.com/coq/coq/issues/14256 | 20 May 2021, 17:34:46 UTC |
| fb05f2b | Jason Gross | 04 May 2021, 15:29:27 UTC | Switch to latest version of Haskell and Cabal Mainly to silence warnings/annotations. Also switch from an unmaintained action to a maintained one. | 20 May 2021, 17:34:46 UTC |
| 098fd23 | Jason Gross | 20 May 2021, 14:32:40 UTC | Add more rewrite_mod_small tactics | 20 May 2021, 14:32:40 UTC |
| 7086309 | Jason Gross | 20 May 2021, 13:25:28 UTC | Add some Wf facts from Fiat | 20 May 2021, 13:25:28 UTC |
| 431b450 | Jason Gross | 20 May 2021, 00:04:46 UTC | Fix a typo and improve doc comment | 20 May 2021, 00:48:37 UTC |
| c4237de | Jason Gross | 20 May 2021, 00:13:44 UTC | Remove trailing whitespace | 20 May 2021, 00:13:44 UTC |
| f555159 | Jason Gross | 19 May 2021, 02:09:59 UTC | Test that gofmt is a no-op on Go code | 19 May 2021, 12:32:59 UTC |
| 9525e9d | Jason Gross | 18 May 2021, 18:47:36 UTC | Bump coqprime | 19 May 2021, 01:47:52 UTC |
| 4a0b8d1 | Automated Publisher | 18 May 2021, 18:44:42 UTC | Automated Rust Crate Version Bump: Tue May 18 18:44:42 UTC 2021 2d76718a2be2b05e22c57c2c0dd6dadd72134f05 | 18 May 2021, 18:44:42 UTC |
| 2d76718 | Jason Gross | 17 May 2021, 22:48:10 UTC | Update fancy machine to use the new curve_good requests | 17 May 2021, 22:48:10 UTC |
| e7c20b5 | Jason Gross | 17 May 2021, 21:34:59 UTC | Add map_ranges utility functions | 17 May 2021, 21:34:59 UTC |
| 21fa689 | Jason Gross | 06 May 2021, 21:21:10 UTC | Make `prime_bytes_bounds` not an `option` This makes things more uniform | 17 May 2021, 21:33:39 UTC |
| 13ac664 | Jason Gross | 17 May 2021, 21:23:09 UTC | Fix a missing argument | 17 May 2021, 21:23:09 UTC |
| f028939 | Jason Gross | 17 May 2021, 14:08:43 UTC | Add tactics for getting all instances of a class | 17 May 2021, 14:08:43 UTC |
| d50398f | Jason Gross | 15 May 2021, 15:55:06 UTC | Bump rewriter | 15 May 2021, 15:55:06 UTC |
| f6f2278 | Jason Gross | 15 May 2021, 01:48:46 UTC | Compatibility with bumped rewriter This is in preparation for having typedefs based on bounds info. If this passes CI, then we can merge https://github.com/mit-plv/rewriter/pull/28. | 15 May 2021, 15:47:42 UTC |
| 32f9f0b | Jason Gross | 15 May 2021, 01:46:25 UTC | Bump rewriter | 15 May 2021, 15:47:42 UTC |
| afbc55a | Jason Gross | 15 May 2021, 01:43:40 UTC | Bump rewriter for compat with Coq master | 15 May 2021, 01:43:40 UTC |
| 4dd8dba | Jason Gross | 13 May 2021, 18:28:53 UTC | Remove useless require | 13 May 2021, 18:28:53 UTC |
| cfa7106 | Jason Gross | 13 May 2021, 17:30:01 UTC | Add list_beq_hetero lemmas | 13 May 2021, 17:30:01 UTC |
| 78fff68 | Jason Gross | 13 May 2021, 17:19:38 UTC | Rename forall2b into list_beq_hetero | 13 May 2021, 17:19:38 UTC |
| 31d4637 | Jason Gross | 13 May 2021, 17:17:48 UTC | Add some utility functions | 13 May 2021, 17:17:58 UTC |
| 7235aa9 | Jason Gross | 12 May 2021, 20:25:48 UTC | Include newlines in -h output Fixes #979 | 12 May 2021, 20:25:48 UTC |
| f4fa385 | Jason Gross | 12 May 2021, 14:02:45 UTC | Revert "TEMP DO NOT MERGE Remove other CI files Also test opam package on PR" This reverts commit aee63da68811951357adb8e3ee66e816fce0160b. | 12 May 2021, 17:08:17 UTC |
| 9be7e28 | Jason Gross | 12 May 2021, 14:06:27 UTC | Update coq-opam-package.yml Now that https://github.com/avsm/setup-ocaml/pull/77 has been merged | 12 May 2021, 17:08:17 UTC |
| 66f003a | Jason Gross | 11 May 2021, 15:39:59 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| ecc3e5c | Jason Gross | 11 May 2021, 14:32:59 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 0ca45b5 | Jason Gross | 11 May 2021, 01:27:05 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| a9b3a3a | Jason Gross | 11 May 2021, 01:24:35 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 5e99331 | Jason Gross | 10 May 2021, 16:31:02 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 0d8630c | Jason Gross | 10 May 2021, 13:53:09 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| f79425c | Jason Gross | 10 May 2021, 12:52:16 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 94c1d9c | Jason Gross | 07 May 2021, 22:30:00 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| ccdd066 | Jason Gross | 07 May 2021, 18:27:50 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| bc3847a | Jason Gross | 06 May 2021, 20:46:09 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 841ac8f | Jason Gross | 06 May 2021, 20:32:18 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 47ac106 | Jason Gross | 06 May 2021, 03:13:27 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 80622d5 | Jason Gross | 06 May 2021, 00:38:29 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| b6e86e0 | Jason Gross | 06 May 2021, 00:28:01 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 4cb4c51 | Jason Gross | 06 May 2021, 00:17:42 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 7c9daf2 | Jason Gross | 05 May 2021, 21:33:12 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 711adfc | Jason Gross | 05 May 2021, 21:32:27 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| b2b288f | Jason Gross | 05 May 2021, 18:54:47 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 225b6c7 | Jason Gross | 05 May 2021, 17:11:07 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 617b23e | Jason Gross | 05 May 2021, 16:13:55 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| 50edef8 | Jason Gross | 04 May 2021, 20:10:12 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
| c080a0a | Jason Gross | 04 May 2021, 15:03:14 UTC | Update coq-opam-package.yml | 12 May 2021, 17:08:17 UTC |
