diff options
Diffstat (limited to 'test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected')
| -rw-r--r-- | test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected | 307 |
1 files changed, 307 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected new file mode 100644 index 0000000000..05c1687002 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/time-of-build-pretty.log.expected @@ -0,0 +1,307 @@ +Time | File Name +----------------------------------------------------------------------- +39m02.51s | Total +----------------------------------------------------------------------- +3m26.96s | Kami/Ex/Multiplier64 +3m22.44s | bedrock2/compiler/src/FlatToRiscv +2m19.56s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI +2m11.59s | Kami/Ex/Divider64 +1m44.22s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeCSR +1m44.11s | Kami/Ex/Multiplier32 +1m41.50s | bedrock2/bedrock2/src/Examples/bsearch +1m08.57s | Kami/Ex/ProcFDInl +1m07.92s | bedrock2/deps/riscv-coq/src/Platform/MinimalMMIO +1m01.07s | Kami/Ex/FifoCorrect +1m00.73s | Kami/Ex/Divider32 +0m50.15s | bedrock2/deps/riscv-coq/src/Proofs/EncodeBound +0m40.64s | bedrock2/bedrock2/src/Examples/FE310CompilerDemo +0m40.29s | Kami/InlineFacts +0m39.12s | Kami/Renaming +0m37.44s | Kami/Ex/SimpleFifoCorrect +0m37.08s | Kami/SemFacts +0m36.08s | ─preprbedrock2/deps/coqutil/src/Map/TestGoals +0m32.76s | Kami/ModularFacts +0m28.68s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA +0m26.60s | Kami/Lib/Word +0m26.55s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_SB +0m26.45s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA64 +0m25.80s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI64 +0m25.47s | bedrock2/processor/src/KamiRiscv +0m23.66s | bedrock2/compiler/src/EmitsValid +0m22.68s | Kami/Ex/InDepthTutorial +0m22.60s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM +0m21.68s | Kami/Specialize +0m21.59s | bedrock2/bedrock2/src/Examples/lightbulb +0m19.20s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_66 +0m19.19s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_UJ +0m17.33s | Kami/Ex/ProcDecInl +0m15.63s | bedrock2/compiler/src/examples/MMIO +0m14.78s | Kami/ParametricSyntax +0m12.11s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_S +0m11.74s | bedrock2/deps/riscv-coq/src/Platform/MetricMinimal +0m09.95s | bedrock2/deps/coqutil/src/Word/Properties +0m09.77s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM64 +0m09.56s | Kami/Lib/FMap +0m09.35s | bedrock2/bedrock2/src/Examples/ipow +0m09.26s | Kami/StepDet +0m09.19s | bedrock2/bedrock2/src/WeakestPreconditionProperties +0m09.16s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_Fence +0m08.98s | Kami/RefinementFacts +0m08.68s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R_atomic +0m08.26s | bedrock2/compiler/src/FlatToRiscv32 +0m07.55s | Kami/Ex/Fifo +0m07.54s | ─ensbedrock2/deps/coqutil/src/Map/SlowGoals +0m06.99s | bedrock2/deps/riscv-coq/src/Platform/Minimal +0m06.89s | bedrock2/compiler/src/GoFlatToRiscv +0m06.82s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I +0m06.72s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_FenceI +0m06.50s | Kami/Semantics +0m06.36s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_57 +0m06.32s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R +0m06.24s | Kami/PartialInlineFacts +0m06.02s | bedrock2/deps/coqutil/src/Map/Properties +0m05.62s | Kami/Ex/ProcThreeStage +0m05.56s | Kami/Decomposition +0m05.12s | Kami/Amortization +0m05.07s | Kami/Ex/SCMMInl +0m04.71s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_system +0m04.46s | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_U +0m04.19s | Kami/ParametricInline +0m04.13s | Kami/Ex/ProcDec +0m03.88s | bedrock2/bedrock2/src/Examples/swap +0m03.81s | Kami/Ex/SC +0m03.64s | bedrock2/bedrock2/src/FE310CSemantics +0m03.39s | Kami/Tutorial +0m03.30s | bedrock2/compiler/src/examples/Fibonacci +0m03.17s | Kami/Label +0m03.17s | Kami/ModuleBoundEx +0m03.10s | Kami/ParametricEquiv +0m03.06s | Kami/Wf +0m02.50s | bedrock2/compiler/src/Pipeline +0m02.42s | Kami/Ex/ProcFDInv +0m02.42s | Kami/ParamDup +0m02.39s | Kami/Duplicate +0m02.19s | Kami/ParametricWf +0m02.11s | Kami/Ex/ProcFetchDecode +0m02.06s | bedrock2/bedrock2/src/Examples/ARPResponder +0m01.94s | Kami/MapReifyEx +0m01.89s | Kami/Syntax +0m01.88s | Kami/Ex/IsaRv32/PgmGcd +0m01.87s | Kami/Ex/IsaRv32/PgmBankerWorker1 +0m01.87s | Kami/Ex/IsaRv32/PgmMatMulReport +0m01.85s | Kami/Ex/IsaRv32/PgmBankerWorker3 +0m01.83s | Kami/Ex/IsaRv32/PgmDekker2 +0m01.83s | Kami/Ex/IsaRv32/PgmFact +0m01.83s | Kami/Ex/IsaRv32/PgmMatMulNormal1 +0m01.81s | Kami/Ex/IsaRv32/PgmBankerInit +0m01.81s | Kami/Ex/IsaRv32/PgmMatMulInit +0m01.81s | Kami/Ex/IsaRv32/PgmMatMulNormal2 +0m01.81s | Kami/Ex/RegFile +0m01.80s | Kami/Ex/IsaRv32/PgmBankerWorker2 +0m01.80s | Kami/Ex/IsaRv32/PgmPeterson1 +0m01.80s | Kami/Ex/IsaRv32/PgmPeterson2 +0m01.80s | bedrock2/bedrock2/src/ptsto_bytes +0m01.78s | Kami/Ex/IsaRv32/PgmDekker1 +0m01.78s | Kami/Ex/ProcDecInv +0m01.76s | bedrock2/bedrock2/src/Map/SeparationLogic +0m01.75s | Kami/Ex/IsaRv32/PgmBsort +0m01.74s | Kami/Ex/IsaRv32/PgmHanoi +0m01.70s | Kami/Ex/NativeFifo +0m01.52s | Kami/Lib/NatLib +0m01.51s | bedrock2/processor/src/Test +0m01.48s | Kami/SymEval +0m01.47s | Kami/Ex/MemAtomic +0m01.44s | Kami/Ex/ProcThreeStInv +0m01.35s | bedrock2/bedrock2/src/Array +0m01.34s | bedrock2/bedrock2/src/TailRecursion +0m01.30s | Kami/Ex/IsaRv32 +0m01.29s | Kami/ModuleBound +0m01.29s | bedrock2/bedrock2/src/Byte +0m01.25s | bedrock2/bedrock2/src/Examples/chacha20 +0m01.19s | Kami/Ex/ProcThreeStDec +0m01.18s | bedrock2/bedrock2/src/Scalars +0m01.17s | bedrock2/deps/riscv-coq/src/Utility/ListLib +0m01.15s | Kami/Ex/OneEltFifo +0m01.14s | bedrock2/bedrock2/src/Examples/Trace +0m01.13s | bedrock2/bedrock2/src/TODO_absint +0m01.10s | bedrock2/compiler/lib/LibTactics +0m01.08s | Kami/Lib/StringAsList +0m01.00s | bedrock2/deps/coqutil/src/Z/ZLib +0m00.99s | Kami/Lib/Struct +0m00.98s | bedrock2/compiler/src/examples/toposort +0m00.95s | bedrock2/deps/riscv-coq/src/Utility/prove_Zeq_bitwise +0m00.94s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeProver +0m00.94s | bedrock2/deps/riscv-coq/src/Spec/ExecuteI +0m00.93s | Kami/Ex/ProcDecSC +0m00.92s | Kami/Ex/IsaRv32PgmExt +0m00.90s | Kami/Lib/Indexer +0m00.89s | Kami/Tactics +0m00.88s | bedrock2/compiler/src/util/ListLib +0m00.87s | Kami/Notations +0m00.84s | bedrock2/bedrock2/src/Memory +0m00.83s | Kami/Ex/ProcFDCorrect +0m00.83s | bedrock2/deps/riscv-coq/src/Utility/ZBitOps +0m00.82s | Kami/Ex/IsaRv32Pgm +0m00.82s | Kami/Lib/ilist +0m00.81s | Kami/Ex/ProcDecSCN +0m00.81s | bedrock2/deps/coqutil/src/Z/BitOps +0m00.80s | Kami/Ex/ProcFourStDec +0m00.80s | bedrock2/compiler/src/examples/EditDistExample +0m00.79s | Kami/Ext/BSyntax +0m00.79s | Kami/Ext/Extraction +0m00.77s | Kami/ParametricInlineLtac +0m00.76s | bedrock2/deps/riscv-coq/src/Platform/Example64Literal +0m00.76s | bedrock2/deps/riscv-coq/src/Spec/MetricPrimitives +0m00.75s | Kami/Ex/ProcThreeStInl +0m00.74s | Kami/Kami +0m00.74s | bedrock2/compiler/src/examples/CompileExamples +0m00.74s | bedrock2/compiler/src/examples/swap_bytes_over_uart_hexdump +0m00.74s | bedrock2/deps/riscv-coq/src/Platform/MinimalLogging +0m00.72s | Kami/Substitute +0m00.72s | bedrock2/compiler/src/examples/TestExprImp +0m00.72s | bedrock2/deps/riscv-coq/src/Spec/Primitives +0m00.71s | Kami/Ex/MemTypes +0m00.71s | bedrock2/compiler/src/examples/InlineAssemblyMacro +0m00.71s | bedrock2/compiler/src/examples/TestFlatImp +0m00.71s | bedrock2/deps/riscv-coq/src/Platform/Memory +0m00.71s | bedrock2/deps/riscv-coq/src/Spec/Decode +0m00.70s | Kami/Inline +0m00.70s | Kami/Lib/StringAsOT +0m00.69s | bedrock2/compiler/src/FlatToRiscvDef +0m00.68s | bedrock2/compiler/src/Rem4 +0m00.67s | Kami/SymEvalTac +0m00.67s | bedrock2/compiler/src/SimplWordExpr +0m00.67s | bedrock2/deps/riscv-coq/src/Utility/Encode +0m00.66s | bedrock2/bedrock2/src/Semantics +0m00.63s | Kami/Lib/StringStringAsOT +0m00.63s | bedrock2/deps/coqutil/src/Datatypes/PropSet +0m00.61s | bedrock2/compiler/src/UnmappedMemForExtSpec +0m00.61s | bedrock2/deps/riscv-coq/src/Utility/Monads +0m00.60s | bedrock2/deps/coqutil/src/Map/SortedList +0m00.59s | Kami/Synthesize +0m00.59s | bedrock2/compiler/src/util/Common +0m00.59s | bedrock2/deps/coqutil/src/Map/SortedListWord +0m00.58s | bedrock2/deps/coqutil/src/Word/Naive +0m00.58s | bedrock2/deps/riscv-coq/src/Utility/runsToNonDet_Run +0m00.57s | bedrock2/bedrock2/src/BasicC64Semantics +0m00.57s | bedrock2/deps/riscv-coq/src/Utility/Utility +0m00.56s | Kami/Lib/WordSupport +0m00.56s | bedrock2/bedrock2/src/WeakestPrecondition +0m00.55s | Kami/Lib/StringEq +0m00.55s | bedrock2/bedrock2/src/BasicC32Semantics +0m00.55s | bedrock2/compiler/src/examples/highlevel/FuncMut +0m00.55s | bedrock2/deps/riscv-coq/src/Spec/ExecuteI64 +0m00.55s | bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl32 +0m00.54s | bedrock2/bedrock2/src/Examples/MultipleReturnValues +0m00.53s | bedrock2/compiler/src/RegAlloc2 +0m00.53s | bedrock2/deps/riscv-coq/src/Spec/ExecuteM +0m00.52s | bedrock2/bedrock2/src/ProgramLogic +0m00.52s | bedrock2/deps/riscv-coq/src/Platform/Run +0m00.52s | bedrock2/deps/riscv-coq/src/Spec/ExecuteM64 +0m00.52s | bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl64 +0m00.52s | bedrock2/deps/riscv-coq/src/Utility/Words32Naive +0m00.50s | bedrock2/bedrock2/src/BasicCSyntax +0m00.50s | bedrock2/compiler/src/Basic32Semantics +0m00.50s | bedrock2/compiler/src/RegAlloc3 +0m00.49s | bedrock2/bedrock2/src/BytedumpTest +0m00.49s | bedrock2/bedrock2/src/BytedumpTestα +0m00.49s | bedrock2/deps/coqutil/src/Map/Z_keyed_SortedListMap +0m00.49s | bedrock2/deps/riscv-coq/src/Spec/Machine +0m00.49s | bedrock2/deps/riscv-coq/src/Utility/MkMachineWidth +0m00.49s | bedrock2/deps/riscv-coq/src/Utility/Words64Naive +0m00.48s | bedrock2/bedrock2/src/ToCString +0m00.48s | bedrock2/compiler/src/SeparationLogic +0m00.48s | bedrock2/deps/coqutil/src/Decidable +0m00.48s | bedrock2/deps/riscv-coq/src/Platform/MetricRiscvMachine +0m00.48s | bedrock2/deps/riscv-coq/src/Platform/RiscvMachine +0m00.47s | bedrock2/bedrock2/src/BasicC64Syntax +0m00.47s | bedrock2/deps/riscv-coq/src/Spec/PseudoInstructions +0m00.46s | bedrock2/compiler/src/ZNameGen +0m00.46s | bedrock2/deps/riscv-coq/src/Platform/MetricLogging +0m00.45s | bedrock2/compiler/src/RegAllocAnnotatedNotations +0m00.45s | bedrock2/processor/src/KamiWord +0m00.44s | bedrock2/deps/coqutil/src/Map/SortedListString_test +0m00.44s | bedrock2/deps/coqutil/src/Tactics/Tactics +0m00.44s | bedrock2/deps/riscv-coq/src/Spec/Execute +0m00.44s | bedrock2/deps/riscv-coq/src/Utility/InstructionNotations +0m00.43s | bedrock2/bedrock2/src/Map/Separation +0m00.43s | bedrock2/compiler/src/RiscvWordProperties +0m00.43s | bedrock2/deps/riscv-coq/src/Spec/VirtualMemory +0m00.43s | bedrock2/deps/riscv-coq/src/Utility/InstructionCoercions +0m00.42s | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncode +0m00.40s | bedrock2/compiler/src/util/Tactics +0m00.40s | bedrock2/deps/coqutil/src/Map/Interface +0m00.39s | bedrock2/deps/coqutil/src/Z/HexNotation +0m00.38s | Kami/Lib/CommonTactics +0m00.38s | Kami/Lib/Nomega +0m00.38s | bedrock2/bedrock2/src/ZNamesSyntax +0m00.37s | bedrock2/deps/coqutil/src/Map/Funext +0m00.37s | bedrock2/deps/riscv-coq/src/Utility/div_mod_to_quot_rem +0m00.36s | Kami/Ex/Names +0m00.36s | Kami/Lib/Concat +0m00.36s | bedrock2/bedrock2/src/string2ident +0m00.36s | bedrock2/compiler/src/Simp +0m00.36s | bedrock2/deps/coqutil/src/Map/Solver +0m00.36s | bedrock2/deps/riscv-coq/src/Utility/nat_div_mod_to_quot_rem +0m00.35s | Kami/Lib/Misc +0m00.35s | bedrock2/bedrock2/src/Examples/StructAccess +0m00.35s | bedrock2/bedrock2/src/StructNotations +0m00.35s | bedrock2/deps/coqutil/src/Map/Empty_set_keyed_map +0m00.35s | bedrock2/deps/coqutil/src/Map/SortedListString +0m00.34s | Kami/Lib/Reflection +0m00.34s | bedrock2/bedrock2/src/Bytedump +0m00.34s | bedrock2/deps/riscv-coq/src/Utility/Tactics +0m00.33s | bedrock2/bedrock2/src/NotationsCustomEntry +0m00.33s | bedrock2/compiler/src/util/MyOmega +0m00.32s | bedrock2/bedrock2/src/Hexdump +0m00.32s | bedrock2/compiler/src/NameGen +0m00.31s | bedrock2/compiler/lib/LibTacticsMin +0m00.30s | bedrock2/bedrock2/src/StringNamesSyntax +0m00.30s | bedrock2/compiler/src/util/Set +0m00.30s | bedrock2/compiler/src/util/SetSolverTests +0m00.29s | bedrock2/deps/coqutil/src/Datatypes/String +0m00.27s | bedrock2/deps/coqutil/src/Word/LittleEndian +0m00.27s | bedrock2/deps/riscv-coq/src/Utility/MonadTests +0m00.26s | bedrock2/deps/coqutil/src/Z/div_mod_to_equations +0m00.23s | bedrock2/deps/riscv-coq/src/Utility/MonadT +0m00.19s | bedrock2/bedrock2/src/NotationsInConstr +0m00.19s | bedrock2/deps/coqutil/src/Datatypes/HList +0m00.17s | Kami/Lib/VectorFacts +0m00.17s | bedrock2/deps/riscv-coq/src/Utility/JMonad +0m00.14s | Kami/Lib/DepEq +0m00.13s | Kami/Lib/FinNotations +0m00.13s | bedrock2/bedrock2/src/ListPred +0m00.13s | bedrock2/bedrock2/src/Variables +0m00.13s | bedrock2/deps/coqutil/src/Datatypes/List +0m00.12s | bedrock2/deps/riscv-coq/src/Utility/MonadNotations +0m00.09s | bedrock2/bedrock2/src/Lift1Prop +0m00.09s | bedrock2/deps/coqutil/src/Datatypes/Option +0m00.09s | bedrock2/deps/coqutil/src/Datatypes/Prod +0m00.07s | Kami/Lib/BasicLogic +0m00.07s | bedrock2/bedrock2/src/Syntax +0m00.06s | Kami/Lib/DepEqNat +0m00.06s | bedrock2/deps/coqutil/src/Macros/symmetry +0m00.05s | bedrock2/compiler/lib/fiat_crypto_tactics/Not +0m00.05s | bedrock2/compiler/src/util/Misc +0m00.05s | bedrock2/deps/riscv-coq/src/Utility/PowerFunc +0m00.05s | bedrock2/deps/riscv-coq/src/Utility/runsToNonDet +0m00.04s | bedrock2/bedrock2/src/Markers +0m00.04s | bedrock2/bedrock2/src/Notations +0m00.04s | bedrock2/compiler/lib/fiat_crypto_tactics/Test +0m00.04s | bedrock2/compiler/lib/fiat_crypto_tactics/UniquePose +0m00.04s | bedrock2/compiler/src/NoActionSyntaxParams +0m00.04s | bedrock2/compiler/src/eqexact +0m00.04s | bedrock2/compiler/src/examples/highlevel/For +0m00.04s | bedrock2/compiler/src/on_hyp_containing +0m00.04s | bedrock2/compiler/src/util/Learning +0m00.04s | bedrock2/deps/coqutil/src/Datatypes/PrimitivePair +0m00.04s | bedrock2/deps/coqutil/src/Macros/subst +0m00.04s | bedrock2/deps/coqutil/src/Macros/unique +0m00.04s | bedrock2/deps/coqutil/src/Tactics/eabstract +0m00.04s | bedrock2/deps/coqutil/src/Tactics/letexists +0m00.04s | bedrock2/deps/coqutil/src/Tactics/rdelta +0m00.04s | bedrock2/deps/coqutil/src/Tactics/syntactic_unify +0m00.04s | bedrock2/deps/coqutil/src/dlet +0m00.04s | bedrock2/deps/coqutil/src/sanity +0m00.04s | bedrock2/deps/riscv-coq/src/Utility/MMIOTrace +0m00.03s | bedrock2/compiler/src/util/LogGoal
\ No newline at end of file |
