-
-
Save kckennylau/04917450f71db69f29150d64f360dd0f to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| git ls-files *.lean | xargs -I % sh -c '>&2 echo %; /c/lean/bin/lean --profile % >/dev/null;' > profile.txt 2>&1 | |
| algebra/archimedean.lean | |
| cumulative profiling times: | |
| compilation 22.4ms | |
| decl post-processing 37.5ms | |
| elaboration 2.23s | |
| elaboration: tactic compilation 203ms | |
| elaboration: tactic execution 651ms | |
| parsing 327ms | |
| type checking 48.9ms | |
| algebra/big_operators.lean | |
| cumulative profiling times: | |
| compilation 1.46ms | |
| decl post-processing 3.63s | |
| elaboration 4.83s | |
| elaboration: tactic compilation 413ms | |
| elaboration: tactic execution 2.15s | |
| parsing 677ms | |
| type checking 13.2ms | |
| algebra/char_zero.lean | |
| cumulative profiling times: | |
| compilation 0.115ms | |
| decl post-processing 5.52ms | |
| elaboration 316ms | |
| elaboration: tactic compilation 60.5ms | |
| elaboration: tactic execution 42ms | |
| parsing 44.8ms | |
| type checking 6.89ms | |
| algebra/default.lean | |
| algebra/euclidean_domain.lean | |
| cumulative profiling times: | |
| compilation 8.16ms | |
| decl post-processing 14.9ms | |
| elaboration 1.05s | |
| elaboration: tactic compilation 237ms | |
| elaboration: tactic execution 252ms | |
| parsing 294ms | |
| type checking 7.73ms | |
| algebra/field.lean | |
| cumulative profiling times: | |
| compilation 12.9ms | |
| decl post-processing 9.67ms | |
| elaboration 772ms | |
| elaboration: tactic compilation 203ms | |
| elaboration: tactic execution 123ms | |
| parsing 194ms | |
| type checking 14.7ms | |
| algebra/field_power.lean | |
| cumulative profiling times: | |
| compilation 0.577ms | |
| decl post-processing 2.45ms | |
| elaboration 1.21s | |
| elaboration: tactic compilation 72.8ms | |
| elaboration: tactic execution 522ms | |
| parsing 197ms | |
| type checking 2.72ms | |
| algebra/gcd_domain.lean | |
| cumulative profiling times: | |
| compilation 0.364ms | |
| decl post-processing 12.5ms | |
| elaboration 2.2s | |
| elaboration: tactic compilation 220ms | |
| elaboration: tactic execution 455ms | |
| parsing 287ms | |
| type checking 59.3ms | |
| algebra/group.lean | |
| cumulative profiling times: | |
| compilation 46.8ms | |
| decl post-processing 1.96s | |
| elaboration 1.68s | |
| elaboration: tactic compilation 287ms | |
| elaboration: tactic execution 314ms | |
| parsing 269ms | |
| type checking 31.8ms | |
| algebra/group_power.lean | |
| cumulative profiling times: | |
| compilation 2.49ms | |
| decl post-processing 119ms | |
| elaboration 2.59s | |
| elaboration: tactic compilation 387ms | |
| elaboration: tactic execution 661ms | |
| parsing 318ms | |
| type checking 15ms | |
| algebra/module.lean | |
| cumulative profiling times: | |
| compilation 16.3ms | |
| decl post-processing 76.1ms | |
| elaboration 21.4s | |
| elaboration: tactic compilation 312ms | |
| elaboration: tactic execution 15.7s | |
| parsing 323ms | |
| type checking 50.1ms | |
| algebra/order.lean | |
| cumulative profiling times: | |
| compilation 0.0827ms | |
| decl post-processing 1.56ms | |
| elaboration 121ms | |
| elaboration: tactic compilation 29.1ms | |
| elaboration: tactic execution 0ms | |
| parsing 14.2ms | |
| type checking 2.76ms | |
| algebra/order_functions.lean | |
| cumulative profiling times: | |
| compilation 0.9ms | |
| decl post-processing 3.03ms | |
| elaboration 2.87s | |
| elaboration: tactic compilation 181ms | |
| elaboration: tactic execution 1.64s | |
| parsing 220ms | |
| type checking 9.89ms | |
| algebra/ordered_field.lean | |
| cumulative profiling times: | |
| compilation 2.92ms | |
| decl post-processing 36.6ms | |
| elaboration 2.31s | |
| elaboration: tactic compilation 200ms | |
| elaboration: tactic execution 1.02s | |
| parsing 163ms | |
| type checking 55.1ms | |
| algebra/ordered_group.lean | |
| cumulative profiling times: | |
| compilation 76.7ms | |
| decl post-processing 84.1ms | |
| elaboration 7.07s | |
| elaboration: tactic compilation 518ms | |
| elaboration: tactic execution 3.03s | |
| parsing 556ms | |
| type checking 76ms | |
| algebra/ordered_ring.lean | |
| cumulative profiling times: | |
| compilation 98.3ms | |
| decl post-processing 106ms | |
| elaboration 6.03s | |
| elaboration: tactic compilation 362ms | |
| elaboration: tactic execution 3.32s | |
| parsing 430ms | |
| type checking 95.7ms | |
| algebra/pi_instances.lean | |
| cumulative profiling times: | |
| compilation 145ms | |
| decl post-processing 2.87s | |
| elaboration 4.17s | |
| elaboration: tactic compilation 74.8ms | |
| elaboration: tactic execution 1.82s | |
| parsing 22.8ms | |
| type checking 96.5ms | |
| algebra/ring.lean | |
| cumulative profiling times: | |
| compilation 19.4ms | |
| decl post-processing 53.1ms | |
| elaboration 5.4s | |
| elaboration: tactic compilation 357ms | |
| elaboration: tactic execution 3.1s | |
| parsing 413ms | |
| type checking 36.6ms | |
| analysis/bounded_linear_maps.lean | |
| cumulative profiling times: | |
| compilation 0.0227ms | |
| decl post-processing 0.239ms | |
| elaboration 6.96s | |
| elaboration: tactic compilation 119ms | |
| elaboration: tactic execution 5.99s | |
| parsing 164ms | |
| type checking 6.52ms | |
| analysis/complex.lean | |
| cumulative profiling times: | |
| compilation 0.214ms | |
| decl post-processing 5.87ms | |
| elaboration 2.19s | |
| elaboration: tactic compilation 43.3ms | |
| elaboration: tactic execution 1.18s | |
| parsing 61.7ms | |
| type checking 8.56ms | |
| analysis/ennreal.lean | |
| cumulative profiling times: | |
| compilation 1.22ms | |
| decl post-processing 35.9ms | |
| elaboration 17.5s | |
| elaboration: tactic compilation 352ms | |
| elaboration: tactic execution 16.2s | |
| parsing 499ms | |
| type checking 55.8ms | |
| analysis/limits.lean | |
| cumulative profiling times: | |
| compilation 0.0264ms | |
| decl post-processing 2.69ms | |
| elaboration 10.8s | |
| elaboration: tactic compilation 257ms | |
| elaboration: tactic execution 6.96s | |
| parsing 498ms | |
| type checking 11.5ms | |
| analysis/measure_theory/borel_space.lean | |
| cumulative profiling times: | |
| compilation 0.57ms | |
| decl post-processing 0.68ms | |
| elaboration 2.72s | |
| elaboration: tactic compilation 101ms | |
| elaboration: tactic execution 1.94s | |
| parsing 177ms | |
| type checking 3.37ms | |
| analysis/measure_theory/lebesgue_measure.lean | |
| cumulative profiling times: | |
| compilation 0.0476ms | |
| decl post-processing 3.38ms | |
| elaboration 26.4s | |
| elaboration: tactic compilation 333ms | |
| elaboration: tactic execution 27.3s | |
| parsing 708ms | |
| type checking 8.5ms | |
| analysis/measure_theory/measurable_space.lean | |
| cumulative profiling times: | |
| compilation 68.5ms | |
| decl post-processing 70.9ms | |
| elaboration 14.3s | |
| elaboration: tactic compilation 409ms | |
| elaboration: tactic execution 10.7s | |
| parsing 429ms | |
| type checking 26.4ms | |
| analysis/measure_theory/measure_space.lean | |
| cumulative profiling times: | |
| compilation 6.41ms | |
| decl post-processing 63.2ms | |
| elaboration 21.4s | |
| elaboration: tactic compilation 563ms | |
| elaboration: tactic execution 16.6s | |
| parsing 844ms | |
| type checking 62.5ms | |
| analysis/measure_theory/outer_measure.lean | |
| cumulative profiling times: | |
| compilation 5.37ms | |
| decl post-processing 60.8ms | |
| elaboration 34.6s | |
| elaboration: tactic compilation 392ms | |
| elaboration: tactic execution 27s | |
| parsing 702ms | |
| type checking 50.5ms | |
| analysis/metric_space.lean | |
| cumulative profiling times: | |
| compilation 15.4ms | |
| decl post-processing 47.3ms | |
| elaboration 27.1s | |
| elaboration: tactic compilation 525ms | |
| elaboration: tactic execution 21.5s | |
| parsing 653ms | |
| type checking 52.5ms | |
| analysis/nnreal.lean | |
| cumulative profiling times: | |
| compilation 0.133ms | |
| decl post-processing 16.7ms | |
| elaboration 2.68s | |
| elaboration: tactic compilation 44.2ms | |
| elaboration: tactic execution 1.35s | |
| parsing 90ms | |
| type checking 28.6ms | |
| analysis/normed_space.lean | |
| cumulative profiling times: | |
| compilation 25.2ms | |
| decl post-processing 73.6ms | |
| elaboration 43.7s | |
| elaboration: tactic compilation 377ms | |
| elaboration: tactic execution 30.5s | |
| parsing 586ms | |
| type checking 63.4ms | |
| analysis/probability_mass_function.lean | |
| cumulative profiling times: | |
| compilation 7ms | |
| decl post-processing 22.6ms | |
| elaboration 17s | |
| elaboration: tactic compilation 148ms | |
| elaboration: tactic execution 13.7s | |
| parsing 256ms | |
| type checking 16.6ms | |
| analysis/real.lean | |
| cumulative profiling times: | |
| compilation 0.606ms | |
| decl post-processing 87.8ms | |
| elaboration 17.5s | |
| elaboration: tactic compilation 277ms | |
| elaboration: tactic execution 10.3s | |
| parsing 883ms | |
| type checking 95.6ms | |
| analysis/topology/compact_open.lean | |
| cumulative profiling times: | |
| compilation 7.01ms | |
| decl post-processing 9.07ms | |
| elaboration 5.99s | |
| elaboration: tactic compilation 77.4ms | |
| elaboration: tactic execution 3.51s | |
| parsing 81.9ms | |
| type checking 4.62ms | |
| analysis/topology/continuity.lean | |
| cumulative profiling times: | |
| compilation 4.51ms | |
| decl post-processing 27ms | |
| elaboration 31.3s | |
| elaboration: tactic compilation 1.24s | |
| elaboration: tactic execution 20.7s | |
| parsing 1.92s | |
| type checking 43.7ms | |
| analysis/topology/infinite_sum.lean | |
| cumulative profiling times: | |
| compilation 0.604ms | |
| decl post-processing 5.16ms | |
| elaboration 43.6s | |
| elaboration: tactic compilation 482ms | |
| elaboration: tactic execution 31.8s | |
| parsing 575ms | |
| type checking 31.6ms | |
| analysis/topology/topological_space.lean | |
| cumulative profiling times: | |
| compilation 73.9ms | |
| decl post-processing 71.5ms | |
| elaboration 86.2s | |
| elaboration: tactic compilation 1.5s | |
| elaboration: tactic execution 71.7s | |
| parsing 2.28s | |
| type checking 46.6ms | |
| analysis/topology/topological_structures.lean | |
| cumulative profiling times: | |
| compilation 4.76ms | |
| decl post-processing 16.9ms | |
| elaboration 32.9s | |
| elaboration: tactic compilation 700ms | |
| elaboration: tactic execution 26.4s | |
| parsing 862ms | |
| type checking 40.4ms | |
| analysis/topology/uniform_space.lean | |
| cumulative profiling times: | |
| compilation 139ms | |
| decl post-processing 94.6ms | |
| elaboration 81s | |
| elaboration: tactic compilation 1.49s | |
| elaboration: tactic execution 58.2s | |
| parsing 2.17s | |
| type checking 90.9ms | |
| category/applicative.lean | |
| cumulative profiling times: | |
| compilation 9.03ms | |
| decl post-processing 37.9ms | |
| elaboration 1.5s | |
| elaboration: tactic compilation 81.2ms | |
| elaboration: tactic execution 795ms | |
| parsing 155ms | |
| type checking 24.9ms | |
| category/basic.lean | |
| cumulative profiling times: | |
| compilation 8.64ms | |
| decl post-processing 15.5ms | |
| elaboration 853ms | |
| elaboration: tactic compilation 54.6ms | |
| elaboration: tactic execution 488ms | |
| parsing 75.7ms | |
| type checking 3.09ms | |
| category/functor.lean | |
| cumulative profiling times: | |
| compilation 7.58ms | |
| decl post-processing 12.3ms | |
| elaboration 450ms | |
| elaboration: tactic compilation 43ms | |
| elaboration: tactic execution 213ms | |
| parsing 66.8ms | |
| type checking 6.6ms | |
| category/traversable/basic.lean | |
| cumulative profiling times: | |
| compilation 2.42ms | |
| decl post-processing 1.98ms | |
| elaboration 118ms | |
| elaboration: tactic compilation 6.01ms | |
| elaboration: tactic execution 59ms | |
| parsing 8.88ms | |
| type checking 1.42ms | |
| category/traversable/default.lean | |
| category/traversable/derive.lean | |
| cumulative profiling times: | |
| compilation 526ms | |
| decl post-processing 0.125ms | |
| elaboration 761ms | |
| parsing 31.1ms | |
| type checking 18.6ms | |
| category/traversable/equiv.lean | |
| cumulative profiling times: | |
| compilation 16.2ms | |
| decl post-processing 32.4ms | |
| elaboration 2.22s | |
| elaboration: tactic compilation 87ms | |
| elaboration: tactic execution 1.09s | |
| parsing 224ms | |
| type checking 18.1ms | |
| category/traversable/instances.lean | |
| cumulative profiling times: | |
| compilation 18.6ms | |
| decl post-processing 15.4ms | |
| elaboration 6.87s | |
| elaboration: tactic compilation 184ms | |
| elaboration: tactic execution 5.24s | |
| parsing 288ms | |
| type checking 14.2ms | |
| category/traversable/lemmas.lean | |
| cumulative profiling times: | |
| compilation 3.24ms | |
| decl post-processing 1.32ms | |
| elaboration 1.18s | |
| elaboration: tactic compilation 101ms | |
| elaboration: tactic execution 661ms | |
| parsing 171ms | |
| type checking 6.26ms | |
| category_theory/category.lean | |
| cumulative profiling times: | |
| compilation 14.8ms | |
| decl post-processing 19.6ms | |
| elaboration 1.33s | |
| elaboration: tactic compilation 20.3ms | |
| elaboration: tactic execution 765ms | |
| parsing 10.1ms | |
| type checking 7.49ms | |
| category_theory/embedding.lean | |
| cumulative profiling times: | |
| compilation 11.9ms | |
| decl post-processing 22.3ms | |
| elaboration 1.3s | |
| elaboration: tactic compilation 20.3ms | |
| elaboration: tactic execution 731ms | |
| parsing 4.66ms | |
| type checking 11.8ms | |
| category_theory/examples/measurable_space.lean | |
| cumulative profiling times: | |
| compilation 2.36ms | |
| decl post-processing 1.86ms | |
| elaboration 98.1ms | |
| parsing 0.302ms | |
| type checking 0.633ms | |
| category_theory/examples/monoids.lean | |
| cumulative profiling times: | |
| compilation 4.42ms | |
| decl post-processing 9.96ms | |
| elaboration 362ms | |
| elaboration: tactic compilation 25.2ms | |
| elaboration: tactic execution 153ms | |
| parsing 9.71ms | |
| type checking 6.33ms | |
| category_theory/examples/rings.lean | |
| cumulative profiling times: | |
| compilation 5.26ms | |
| decl post-processing 12.7ms | |
| elaboration 745ms | |
| elaboration: tactic compilation 31.8ms | |
| elaboration: tactic execution 391ms | |
| parsing 10.6ms | |
| type checking 9.24ms | |
| category_theory/examples/topological_spaces.lean | |
| cumulative profiling times: | |
| compilation 17.9ms | |
| decl post-processing 32.4ms | |
| elaboration 1.42s | |
| elaboration: tactic compilation 22ms | |
| elaboration: tactic execution 736ms | |
| parsing 6.48ms | |
| type checking 20.8ms | |
| category_theory/full_subcategory.lean | |
| cumulative profiling times: | |
| compilation 8.86ms | |
| decl post-processing 12.5ms | |
| elaboration 863ms | |
| elaboration: tactic compilation 14ms | |
| elaboration: tactic execution 508ms | |
| parsing 0.514ms | |
| type checking 5.68ms | |
| category_theory/functor.lean | |
| cumulative profiling times: | |
| compilation 15.3ms | |
| decl post-processing 20.7ms | |
| elaboration 580ms | |
| elaboration: tactic compilation 14.8ms | |
| elaboration: tactic execution 302ms | |
| parsing 8.89ms | |
| type checking 14.5ms | |
| category_theory/functor_category.lean | |
| cumulative profiling times: | |
| compilation 3.29ms | |
| decl post-processing 3.86ms | |
| elaboration 690ms | |
| elaboration: tactic compilation 0.558ms | |
| elaboration: tactic execution 397ms | |
| parsing 1.7ms | |
| type checking 10ms | |
| category_theory/isomorphism.lean | |
| cumulative profiling times: | |
| compilation 24ms | |
| decl post-processing 51.2ms | |
| elaboration 4.6s | |
| elaboration: tactic compilation 141ms | |
| elaboration: tactic execution 2.96s | |
| parsing 295ms | |
| type checking 24.3ms | |
| category_theory/natural_isomorphism.lean | |
| cumulative profiling times: | |
| compilation 39.5ms | |
| decl post-processing 111ms | |
| elaboration 7.51s | |
| elaboration: tactic compilation 57.4ms | |
| elaboration: tactic execution 4.33s | |
| parsing 58.9ms | |
| type checking 66.5ms | |
| category_theory/natural_transformation.lean | |
| cumulative profiling times: | |
| compilation 12.1ms | |
| decl post-processing 23.8ms | |
| elaboration 1.87s | |
| elaboration: tactic compilation 47.9ms | |
| elaboration: tactic execution 1.01s | |
| parsing 102ms | |
| type checking 14.3ms | |
| category_theory/opposites.lean | |
| cumulative profiling times: | |
| compilation 9.34ms | |
| decl post-processing 9.09ms | |
| elaboration 1s | |
| elaboration: tactic compilation 29.2ms | |
| elaboration: tactic execution 499ms | |
| parsing 48.3ms | |
| type checking 7.99ms | |
| category_theory/products.lean | |
| cumulative profiling times: | |
| compilation 39.2ms | |
| decl post-processing 56.6ms | |
| elaboration 5.08s | |
| elaboration: tactic compilation 35.6ms | |
| elaboration: tactic execution 2.91s | |
| parsing 58.7ms | |
| type checking 40ms | |
| category_theory/types.lean | |
| cumulative profiling times: | |
| compilation 5.57ms | |
| decl post-processing 13.5ms | |
| elaboration 1.53s | |
| elaboration: tactic compilation 10.2ms | |
| elaboration: tactic execution 971ms | |
| parsing 16.3ms | |
| type checking 13.2ms | |
| category_theory/yoneda.lean | |
| cumulative profiling times: | |
| compilation 62.7ms | |
| decl post-processing 160ms | |
| elaboration 13.4s | |
| elaboration: tactic compilation 81.3ms | |
| elaboration: tactic execution 7.8s | |
| parsing 102ms | |
| type checking 151ms | |
| computability/halting.lean | |
| cumulative profiling times: | |
| compilation 0.292ms | |
| decl post-processing 2.64ms | |
| elaboration 11.2s | |
| elaboration: tactic compilation 297ms | |
| elaboration: tactic execution 7.76s | |
| parsing 655ms | |
| type checking 9.51ms | |
| computability/partrec.lean | |
| cumulative profiling times: | |
| compilation 7.11ms | |
| decl post-processing 12.3ms | |
| elaboration 20.2s | |
| elaboration: tactic compilation 498ms | |
| elaboration: tactic execution 12.7s | |
| parsing 1.24s | |
| type checking 35.4ms | |
| computability/partrec_code.lean | |
| cumulative profiling times: | |
| compilation 39.5ms | |
| decl post-processing 19.5ms | |
| elaboration 37.4s | |
| elaboration: tactic compilation 824ms | |
| elaboration: tactic execution 24.9s | |
| parsing 4.05s | |
| type checking 9.06ms | |
| computability/primrec.lean | |
| cumulative profiling times: | |
| compilation 16.8ms | |
| decl post-processing 19.4ms | |
| elaboration 19.7s | |
| elaboration: tactic compilation 1.24s | |
| elaboration: tactic execution 11.5s | |
| parsing 2.8s | |
| type checking 46.4ms | |
| computability/turing_machine.lean | |
| cumulative profiling times: | |
| compilation 107ms | |
| decl post-processing 428ms | |
| elaboration 73.9s | |
| elaboration: tactic compilation 1.5s | |
| elaboration: tactic execution 59.4s | |
| parsing 4.28s | |
| type checking 76.6ms | |
| core/data/list.lean | |
| cumulative profiling times: | |
| compilation 1.14ms | |
| decl post-processing 2.18ms | |
| elaboration 14.2ms | |
| parsing 0.446ms | |
| type checking 0.129ms | |
| core/default.lean | |
| data/analysis/filter.lean | |
| cumulative profiling times: | |
| compilation 75.3ms | |
| decl post-processing 44.1ms | |
| elaboration 8.93s | |
| elaboration: tactic compilation 114ms | |
| elaboration: tactic execution 5.34s | |
| parsing 154ms | |
| type checking 23.7ms | |
| data/analysis/topology.lean | |
| cumulative profiling times: | |
| compilation 23.5ms | |
| decl post-processing 26.4ms | |
| elaboration 10.7s | |
| elaboration: tactic compilation 73.1ms | |
| elaboration: tactic execution 6.6s | |
| parsing 175ms | |
| type checking 16.3ms | |
| data/array/lemmas.lean | |
| cumulative profiling times: | |
| compilation 9.58ms | |
| decl post-processing 12.1ms | |
| elaboration 5.21s | |
| elaboration: tactic compilation 189ms | |
| elaboration: tactic execution 3.27s | |
| parsing 277ms | |
| type checking 8.86ms | |
| data/bool.lean | |
| cumulative profiling times: | |
| compilation 2.4ms | |
| decl post-processing 5.28ms | |
| elaboration 1.6s | |
| elaboration: tactic compilation 196ms | |
| elaboration: tactic execution 712ms | |
| parsing 101ms | |
| type checking 2.47ms | |
| data/buffer/basic.lean | |
| cumulative profiling times: | |
| compilation 10ms | |
| decl post-processing 11ms | |
| elaboration 2.16s | |
| elaboration: tactic compilation 57.8ms | |
| elaboration: tactic execution 1.44s | |
| parsing 161ms | |
| type checking 2.1ms | |
| data/char.lean | |
| cumulative profiling times: | |
| compilation 1.69ms | |
| decl post-processing 1.72ms | |
| elaboration 8.66ms | |
| parsing 0.267ms | |
| type checking 1.45ms | |
| data/complex/basic.lean | |
| cumulative profiling times: | |
| compilation 68.3ms | |
| decl post-processing 31.8ms | |
| elaboration 56.2s | |
| elaboration: tactic compilation 475ms | |
| elaboration: tactic execution 47.9s | |
| parsing 608ms | |
| type checking 52.6ms | |
| data/dlist/basic.lean | |
| cumulative profiling times: | |
| compilation 0.208ms | |
| decl post-processing 0.968ms | |
| elaboration 7.85ms | |
| parsing 0.21ms | |
| type checking 0.0245ms | |
| data/dlist/instances.lean | |
| cumulative profiling times: | |
| compilation 1.18ms | |
| decl post-processing 1.1ms | |
| elaboration 302ms | |
| elaboration: tactic compilation 5.04ms | |
| elaboration: tactic execution 177ms | |
| parsing 6.78ms | |
| type checking 0.306ms | |
| data/equiv/basic.lean | |
| cumulative profiling times: | |
| compilation 132ms | |
| decl post-processing 135ms | |
| elaboration 5.49s | |
| elaboration: tactic compilation 442ms | |
| elaboration: tactic execution 2.51s | |
| parsing 460ms | |
| type checking 48.1ms | |
| data/equiv/denumerable.lean | |
| cumulative profiling times: | |
| compilation 11.4ms | |
| decl post-processing 12ms | |
| elaboration 2.67s | |
| elaboration: tactic compilation 53.1ms | |
| elaboration: tactic execution 1.55s | |
| parsing 84.6ms | |
| type checking 3.9ms | |
| data/equiv/encodable.lean | |
| cumulative profiling times: | |
| compilation 36.1ms | |
| decl post-processing 30.9ms | |
| elaboration 3.28s | |
| elaboration: tactic compilation 82.5ms | |
| elaboration: tactic execution 1.77s | |
| parsing 139ms | |
| type checking 9.49ms | |
| data/equiv/list.lean | |
| cumulative profiling times: | |
| compilation 38.3ms | |
| decl post-processing 33ms | |
| elaboration 9.07s | |
| elaboration: tactic compilation 111ms | |
| elaboration: tactic execution 5.9s | |
| parsing 180ms | |
| type checking 10.8ms | |
| data/equiv/nat.lean | |
| cumulative profiling times: | |
| compilation 2.62ms | |
| decl post-processing 1.84ms | |
| elaboration 311ms | |
| elaboration: tactic compilation 13.5ms | |
| elaboration: tactic execution 165ms | |
| parsing 13.3ms | |
| type checking 0.526ms | |
| data/erased.lean | |
| cumulative profiling times: | |
| compilation 18.5ms | |
| decl post-processing 49.7ms | |
| elaboration 472ms | |
| elaboration: tactic compilation 24.4ms | |
| elaboration: tactic execution 237ms | |
| parsing 46.1ms | |
| type checking 35.9ms | |
| data/fin.lean | |
| cumulative profiling times: | |
| compilation 9.5ms | |
| decl post-processing 16.7ms | |
| elaboration 382ms | |
| elaboration: tactic compilation 37.3ms | |
| elaboration: tactic execution 177ms | |
| parsing 36.5ms | |
| type checking 8.01ms | |
| data/finset.lean | |
| cumulative profiling times: | |
| compilation 138ms | |
| decl post-processing 178ms | |
| elaboration 173s | |
| elaboration: tactic compilation 1.83s | |
| elaboration: tactic execution 182s | |
| parsing 2.32s | |
| type checking 125ms | |
| data/finsupp.lean | |
| cumulative profiling times: | |
| compilation 178ms | |
| decl post-processing 2.53s | |
| elaboration 68.2s | |
| elaboration: tactic compilation 923ms | |
| elaboration: tactic execution 49.3s | |
| parsing 1.17s | |
| type checking 129ms | |
| data/fintype.lean | |
| cumulative profiling times: | |
| compilation 84.1ms | |
| decl post-processing 92.2ms | |
| elaboration 31.8s | |
| elaboration: tactic compilation 635ms | |
| elaboration: tactic execution 21s | |
| parsing 848ms | |
| type checking 30.4ms | |
| data/fp/basic.lean | |
| cumulative profiling times: | |
| compilation 108ms | |
| decl post-processing 13.5ms | |
| elaboration 1.5s | |
| elaboration: tactic compilation 42.3ms | |
| elaboration: tactic execution 580ms | |
| parsing 130ms | |
| type checking 13.2ms | |
| data/hash_map.lean | |
| cumulative profiling times: | |
| compilation 69.5ms | |
| decl post-processing 60.4ms | |
| elaboration 14s | |
| elaboration: tactic compilation 656ms | |
| elaboration: tactic execution 9.06s | |
| parsing 1.99s | |
| type checking 25.9ms | |
| data/int/basic.lean | |
| cumulative profiling times: | |
| compilation 38.2ms | |
| decl post-processing 30.2ms | |
| elaboration 28.4s | |
| elaboration: tactic compilation 1.73s | |
| elaboration: tactic execution 18.5s | |
| parsing 2.1s | |
| type checking 40.7ms | |
| data/int/gcd.lean | |
| cumulative profiling times: | |
| compilation 23.2ms | |
| decl post-processing 27.6ms | |
| elaboration 10.7s | |
| elaboration: tactic compilation 380ms | |
| elaboration: tactic execution 8.24s | |
| parsing 358ms | |
| type checking 31.6ms | |
| data/int/modeq.lean | |
| cumulative profiling times: | |
| compilation 1.56ms | |
| decl post-processing 1.31ms | |
| elaboration 2.63s | |
| elaboration: tactic compilation 114ms | |
| elaboration: tactic execution 2.09s | |
| parsing 111ms | |
| type checking 1.19ms | |
| data/lazy_list2.lean | |
| cumulative profiling times: | |
| compilation 6.2ms | |
| decl post-processing 4.01ms | |
| elaboration 1.48s | |
| elaboration: tactic compilation 30.4ms | |
| elaboration: tactic execution 753ms | |
| parsing 114ms | |
| type checking 0.841ms | |
| data/list/basic.lean | |
| cumulative profiling times: | |
| compilation 85.7ms | |
| decl post-processing 1.17s | |
| elaboration 126s | |
| elaboration: tactic compilation 4.88s | |
| elaboration: tactic execution 90.9s | |
| parsing 7.79s | |
| type checking 145ms | |
| data/list/default.lean | |
| data/list/perm.lean | |
| cumulative profiling times: | |
| compilation 1.52ms | |
| decl post-processing 255ms | |
| elaboration 14.8s | |
| elaboration: tactic compilation 1.09s | |
| elaboration: tactic execution 9.27s | |
| parsing 2.28s | |
| type checking 19.4ms | |
| data/list/sort.lean | |
| cumulative profiling times: | |
| compilation 2.56ms | |
| decl post-processing 13.8ms | |
| elaboration 4.72s | |
| elaboration: tactic compilation 219ms | |
| elaboration: tactic execution 3s | |
| parsing 509ms | |
| type checking 2.77ms | |
| data/multiset.lean | |
| cumulative profiling times: | |
| compilation 164ms | |
| decl post-processing 1.72s | |
| elaboration 99.3s | |
| elaboration: tactic compilation 2.91s | |
| elaboration: tactic execution 77.9s | |
| parsing 4.31s | |
| type checking 191ms | |
| data/nat/basic.lean | |
| cumulative profiling times: | |
| compilation 10.4ms | |
| decl post-processing 14.9ms | |
| elaboration 6.3s | |
| elaboration: tactic compilation 772ms | |
| elaboration: tactic execution 3.1s | |
| parsing 1.04s | |
| type checking 13.6ms | |
| data/nat/binomial.lean | |
| cumulative profiling times: | |
| compilation 0.00113ms | |
| decl post-processing 0.00378ms | |
| elaboration 1.31s | |
| elaboration: tactic compilation 28.5ms | |
| elaboration: tactic execution 661ms | |
| parsing 39.8ms | |
| type checking 0.375ms | |
| data/nat/cast.lean | |
| cumulative profiling times: | |
| compilation 1.05ms | |
| decl post-processing 6.42ms | |
| elaboration 1.85s | |
| elaboration: tactic compilation 82.1ms | |
| elaboration: tactic execution 1.08s | |
| parsing 102ms | |
| type checking 5.47ms | |
| data/nat/choose.lean | |
| cumulative profiling times: | |
| compilation 0.118ms | |
| decl post-processing 1.25ms | |
| elaboration 1.31s | |
| elaboration: tactic compilation 151ms | |
| elaboration: tactic execution 686ms | |
| parsing 278ms | |
| type checking 0.819ms | |
| data/nat/dist.lean | |
| cumulative profiling times: | |
| compilation 0.438ms | |
| decl post-processing 0.562ms | |
| elaboration 911ms | |
| elaboration: tactic compilation 162ms | |
| elaboration: tactic execution 385ms | |
| parsing 90.7ms | |
| type checking 1.06ms | |
| data/nat/gcd.lean | |
| cumulative profiling times: | |
| compilation 0.816ms | |
| decl post-processing 0.857ms | |
| elaboration 778ms | |
| elaboration: tactic compilation 246ms | |
| elaboration: tactic execution 97ms | |
| parsing 209ms | |
| type checking 5.27ms | |
| data/nat/modeq.lean | |
| cumulative profiling times: | |
| compilation 1.1ms | |
| decl post-processing 1.11ms | |
| elaboration 3.29s | |
| elaboration: tactic compilation 112ms | |
| elaboration: tactic execution 2.56s | |
| parsing 226ms | |
| type checking 1.33ms | |
| data/nat/pairing.lean | |
| cumulative profiling times: | |
| compilation 2.8ms | |
| decl post-processing 1.27ms | |
| elaboration 4.13s | |
| elaboration: tactic compilation 138ms | |
| elaboration: tactic execution 3.1s | |
| parsing 403ms | |
| type checking 0.916ms | |
| data/nat/prime.lean | |
| cumulative profiling times: | |
| compilation 5.45ms | |
| decl post-processing 6.32ms | |
| elaboration 4.92s | |
| elaboration: tactic compilation 423ms | |
| elaboration: tactic execution 2.26s | |
| parsing 457ms | |
| type checking 8.79ms | |
| data/nat/sqrt.lean | |
| cumulative profiling times: | |
| compilation 1.08ms | |
| decl post-processing 1.56ms | |
| elaboration 3.48s | |
| elaboration: tactic compilation 232ms | |
| elaboration: tactic execution 2.25s | |
| parsing 391ms | |
| type checking 2.07ms | |
| data/num/basic.lean | |
| cumulative profiling times: | |
| compilation 37.9ms | |
| decl post-processing 94.3ms | |
| elaboration 808ms | |
| elaboration: tactic compilation 56.7ms | |
| elaboration: tactic execution 126ms | |
| parsing 57.8ms | |
| type checking 3.07ms | |
| data/num/bitwise.lean | |
| cumulative profiling times: | |
| compilation 1.32ms | |
| decl post-processing 18.1ms | |
| elaboration 122ms | |
| parsing 4.25ms | |
| type checking 0.116ms | |
| data/num/lemmas.lean | |
| cumulative profiling times: | |
| compilation 101ms | |
| decl post-processing 44ms | |
| elaboration 34.3s | |
| elaboration: tactic compilation 2.51s | |
| elaboration: tactic execution 19.5s | |
| parsing 3.08s | |
| type checking 71.7ms | |
| data/option.lean | |
| cumulative profiling times: | |
| compilation 5.87ms | |
| decl post-processing 43.1ms | |
| elaboration 2.22s | |
| elaboration: tactic compilation 144ms | |
| elaboration: tactic execution 1.35s | |
| parsing 202ms | |
| type checking 14.1ms | |
| data/padics/padic_integers.lean | |
| cumulative profiling times: | |
| compilation 0.178ms | |
| decl post-processing 16ms | |
| elaboration 1.27s | |
| elaboration: tactic compilation 24.9ms | |
| elaboration: tactic execution 682ms | |
| parsing 30.1ms | |
| type checking 2.61ms | |
| data/padics/padic_norm.lean | |
| cumulative profiling times: | |
| compilation 9.25ms | |
| decl post-processing 14.2ms | |
| elaboration 33.2s | |
| elaboration: tactic compilation 773ms | |
| elaboration: tactic execution 26.6s | |
| parsing 1.27s | |
| type checking 14.7ms | |
| data/padics/padic_rationals.lean | |
| cumulative profiling times: | |
| compilation 3.05ms | |
| decl post-processing 64.7ms | |
| elaboration 38.1s | |
| elaboration: tactic compilation 639ms | |
| elaboration: tactic execution 28.2s | |
| parsing 1.37s | |
| type checking 204ms | |
| data/pfun.lean | |
| cumulative profiling times: | |
| compilation 34.8ms | |
| decl post-processing 132ms | |
| elaboration 4.73s | |
| elaboration: tactic compilation 222ms | |
| elaboration: tactic execution 2.84s | |
| parsing 339ms | |
| type checking 87.1ms | |
| data/pnat.lean | |
| cumulative profiling times: | |
| compilation 4.49ms | |
| decl post-processing 5.61ms | |
| elaboration 38.4ms | |
| parsing 2.03ms | |
| type checking 3.77ms | |
| data/polynomial.lean | |
| cumulative profiling times: | |
| compilation 168ms | |
| decl post-processing 317ms | |
| elaboration 115s | |
| elaboration: tactic compilation 2.03s | |
| elaboration: tactic execution 94.1s | |
| parsing 2.77s | |
| type checking 233ms | |
| data/prod.lean | |
| cumulative profiling times: | |
| compilation 4.43ms | |
| decl post-processing 12.6ms | |
| elaboration 485ms | |
| elaboration: tactic compilation 43.3ms | |
| elaboration: tactic execution 260ms | |
| parsing 48.6ms | |
| type checking 2.75ms | |
| data/quot.lean | |
| cumulative profiling times: | |
| compilation 19.9ms | |
| decl post-processing 47.1ms | |
| elaboration 203ms | |
| elaboration: tactic compilation 12.2ms | |
| elaboration: tactic execution 37ms | |
| parsing 16ms | |
| type checking 30.6ms | |
| data/rat.lean | |
| cumulative profiling times: | |
| compilation 67.2ms | |
| decl post-processing 116ms | |
| elaboration 55.4s | |
| elaboration: tactic compilation 1.64s | |
| elaboration: tactic execution 43.4s | |
| parsing 2.98s | |
| type checking 77.2ms | |
| data/real/basic.lean | |
| cumulative profiling times: | |
| compilation 30.5ms | |
| decl post-processing 147ms | |
| elaboration 36.6s | |
| elaboration: tactic compilation 836ms | |
| elaboration: tactic execution 25.7s | |
| parsing 1.42s | |
| type checking 623ms | |
| data/real/cau_seq.lean | |
| cumulative profiling times: | |
| compilation 63.8ms | |
| decl post-processing 89.7ms | |
| elaboration 19s | |
| elaboration: tactic compilation 545ms | |
| elaboration: tactic execution 12.5s | |
| parsing 1.19s | |
| type checking 86.7ms | |
| data/real/cau_seq_completion.lean | |
| cumulative profiling times: | |
| compilation 41.8ms | |
| decl post-processing 72.4ms | |
| elaboration 8s | |
| elaboration: tactic compilation 89.6ms | |
| elaboration: tactic execution 4.57s | |
| parsing 189ms | |
| type checking 97ms | |
| data/real/ennreal.lean | |
| cumulative profiling times: | |
| compilation 0.66ms | |
| decl post-processing 17.7ms | |
| elaboration 44.4s | |
| elaboration: tactic compilation 488ms | |
| elaboration: tactic execution 37.2s | |
| parsing 692ms | |
| type checking 26.4ms | |
| data/real/irrational.lean | |
| cumulative profiling times: | |
| compilation 0.0846ms | |
| decl post-processing 0.495ms | |
| elaboration 1.04s | |
| elaboration: tactic compilation 18.1ms | |
| elaboration: tactic execution 718ms | |
| parsing 120ms | |
| type checking 0.169ms | |
| data/real/nnreal.lean | |
| cumulative profiling times: | |
| compilation 96.9ms | |
| decl post-processing 74.5ms | |
| elaboration 26.4s | |
| elaboration: tactic compilation 320ms | |
| elaboration: tactic execution 19.9s | |
| parsing 378ms | |
| type checking 68ms | |
| data/semiquot.lean | |
| cumulative profiling times: | |
| compilation 33.9ms | |
| decl post-processing 124ms | |
| elaboration 2.68s | |
| elaboration: tactic compilation 63.8ms | |
| elaboration: tactic execution 1.66s | |
| parsing 69.9ms | |
| type checking 95.7ms | |
| data/seq/computation.lean | |
| cumulative profiling times: | |
| compilation 53.4ms | |
| decl post-processing 122ms | |
| elaboration 8.1s | |
| elaboration: tactic compilation 805ms | |
| elaboration: tactic execution 4.69s | |
| parsing 1.19s | |
| type checking 67.1ms | |
| data/seq/parallel.lean | |
| cumulative profiling times: | |
| compilation 12.4ms | |
| decl post-processing 23.5ms | |
| elaboration 5.76s | |
| elaboration: tactic compilation 306ms | |
| elaboration: tactic execution 4.42s | |
| parsing 1.24s | |
| type checking 5.66ms | |
| data/seq/seq.lean | |
| cumulative profiling times: | |
| compilation 54.5ms | |
| decl post-processing 106ms | |
| elaboration 12.8s | |
| elaboration: tactic compilation 804ms | |
| elaboration: tactic execution 10.1s | |
| parsing 1.33s | |
| type checking 51ms | |
| data/seq/wseq.lean | |
| cumulative profiling times: | |
| compilation 164ms | |
| decl post-processing 90.8ms | |
| elaboration 44.1s | |
| elaboration: tactic compilation 1.72s | |
| elaboration: tactic execution 38.1s | |
| parsing 2.88s | |
| type checking 36.1ms | |
| data/set/basic.lean | |
| cumulative profiling times: | |
| compilation 3.56ms | |
| decl post-processing 40.3ms | |
| elaboration 47.5s | |
| elaboration: tactic compilation 1.14s | |
| elaboration: tactic execution 37.1s | |
| parsing 1.01s | |
| type checking 53.4ms | |
| data/set/countable.lean | |
| cumulative profiling times: | |
| compilation 0.196ms | |
| decl post-processing 1.82ms | |
| elaboration 5.59s | |
| elaboration: tactic compilation 126ms | |
| elaboration: tactic execution 6.36s | |
| parsing 166ms | |
| type checking 5.37ms | |
| data/set/default.lean | |
| data/set/disjointed.lean | |
| cumulative profiling times: | |
| compilation 0.272ms | |
| decl post-processing 1.48ms | |
| elaboration 3.13s | |
| elaboration: tactic compilation 96.3ms | |
| elaboration: tactic execution 2.16s | |
| parsing 165ms | |
| type checking 1.86ms | |
| data/set/enumerate.lean | |
| cumulative profiling times: | |
| compilation 0.399ms | |
| decl post-processing 1.89ms | |
| elaboration 5.46s | |
| elaboration: tactic compilation 92.2ms | |
| elaboration: tactic execution 4.24s | |
| parsing 306ms | |
| type checking 0.609ms | |
| data/set/finite.lean | |
| cumulative profiling times: | |
| compilation 30.5ms | |
| decl post-processing 35.3ms | |
| elaboration 15.3s | |
| elaboration: tactic compilation 268ms | |
| elaboration: tactic execution 14.3s | |
| parsing 461ms | |
| type checking 16.7ms | |
| data/set/function.lean | |
| cumulative profiling times: | |
| compilation 0.773ms | |
| decl post-processing 6.72ms | |
| elaboration 365ms | |
| elaboration: tactic compilation 55.7ms | |
| elaboration: tactic execution 76ms | |
| parsing 38.7ms | |
| type checking 5.63ms | |
| data/set/intervals.lean | |
| cumulative profiling times: | |
| compilation 0.356ms | |
| decl post-processing 4.92ms | |
| elaboration 4.94s | |
| elaboration: tactic compilation 82.8ms | |
| elaboration: tactic execution 3.39s | |
| parsing 167ms | |
| type checking 4.98ms | |
| data/set/lattice.lean | |
| cumulative profiling times: | |
| compilation 33.8ms | |
| decl post-processing 214ms | |
| elaboration 18.4s | |
| elaboration: tactic compilation 505ms | |
| elaboration: tactic execution 13.3s | |
| parsing 632ms | |
| type checking 202ms | |
| data/sigma/basic.lean | |
| cumulative profiling times: | |
| compilation 5.07ms | |
| decl post-processing 8.31ms | |
| elaboration 118ms | |
| elaboration: tactic compilation 5.19ms | |
| elaboration: tactic execution 8ms | |
| parsing 3.21ms | |
| type checking 0.996ms | |
| data/sigma/default.lean | |
| data/stream/basic.lean | |
| data/string.lean | |
| cumulative profiling times: | |
| compilation 5.8ms | |
| decl post-processing 4.94ms | |
| elaboration 1.13s | |
| elaboration: tactic compilation 51.3ms | |
| elaboration: tactic execution 667ms | |
| parsing 50.7ms | |
| type checking 2.01ms | |
| data/subtype.lean | |
| cumulative profiling times: | |
| compilation 2.44ms | |
| decl post-processing 3.63ms | |
| elaboration 72.7ms | |
| elaboration: tactic compilation 14.2ms | |
| elaboration: tactic execution 7ms | |
| parsing 6.9ms | |
| type checking 2.78ms | |
| data/sum.lean | |
| cumulative profiling times: | |
| compilation 0.938ms | |
| decl post-processing 6.69ms | |
| elaboration 148ms | |
| elaboration: tactic compilation 35.5ms | |
| elaboration: tactic execution 7ms | |
| parsing 48.3ms | |
| type checking 1.72ms | |
| data/vector2.lean | |
| cumulative profiling times: | |
| compilation 12.4ms | |
| decl post-processing 35.3ms | |
| elaboration 6.42s | |
| elaboration: tactic compilation 176ms | |
| elaboration: tactic execution 4.46s | |
| parsing 239ms | |
| type checking 9.26ms | |
| data/zmod.lean | |
| cumulative profiling times: | |
| compilation 25.4ms | |
| decl post-processing 22.6ms | |
| elaboration 9.12s | |
| elaboration: tactic compilation 253ms | |
| elaboration: tactic execution 6.17s | |
| parsing 410ms | |
| type checking 22.5ms | |
| field_theory/subfield.lean | |
| cumulative profiling times: | |
| compilation 9.17ms | |
| decl post-processing 14ms | |
| elaboration 988ms | |
| elaboration: tactic compilation 3.25ms | |
| elaboration: tactic execution 592ms | |
| parsing 0.19ms | |
| type checking 9.42ms | |
| group_theory/abelianization.lean | |
| cumulative profiling times: | |
| compilation 24.8ms | |
| decl post-processing 11.7ms | |
| elaboration 1.45s | |
| elaboration: tactic compilation 68.7ms | |
| elaboration: tactic execution 683ms | |
| parsing 76.7ms | |
| type checking 6.44ms | |
| group_theory/coset.lean | |
| cumulative profiling times: | |
| compilation 9.62ms | |
| decl post-processing 5.61s | |
| elaboration 4.79s | |
| elaboration: tactic compilation 130ms | |
| elaboration: tactic execution 2.6s | |
| parsing 160ms | |
| type checking 11.5ms | |
| group_theory/free_abelian_group.lean | |
| cumulative profiling times: | |
| compilation 5.57ms | |
| decl post-processing 9ms | |
| elaboration 1.74s | |
| elaboration: tactic compilation 18.2ms | |
| elaboration: tactic execution 1.02s | |
| parsing 39.9ms | |
| type checking 4.92ms | |
| group_theory/free_group.lean | |
| cumulative profiling times: | |
| compilation 51.5ms | |
| decl post-processing 87.6ms | |
| elaboration 26.5s | |
| elaboration: tactic compilation 722ms | |
| elaboration: tactic execution 22s | |
| parsing 1.17s | |
| type checking 39.3ms | |
| group_theory/group_action.lean | |
| cumulative profiling times: | |
| compilation 3.99ms | |
| decl post-processing 18.9ms | |
| elaboration 1.95s | |
| elaboration: tactic compilation 51ms | |
| elaboration: tactic execution 949ms | |
| parsing 53.2ms | |
| type checking 9.41ms | |
| group_theory/order_of_element.lean | |
| cumulative profiling times: | |
| compilation 8.81ms | |
| decl post-processing 6.58ms | |
| elaboration 6.43s | |
| elaboration: tactic compilation 151ms | |
| elaboration: tactic execution 6.5s | |
| parsing 144ms | |
| type checking 9.23ms | |
| group_theory/perm.lean | |
| cumulative profiling times: | |
| compilation 40.5ms | |
| decl post-processing 104ms | |
| elaboration 55.7s | |
| elaboration: tactic compilation 1.15s | |
| elaboration: tactic execution 42.7s | |
| parsing 1.78s | |
| type checking 66.8ms | |
| group_theory/quotient_group.lean | |
| cumulative profiling times: | |
| compilation 14.9ms | |
| decl post-processing 341ms | |
| elaboration 1.11s | |
| elaboration: tactic compilation 35ms | |
| elaboration: tactic execution 289ms | |
| parsing 28.1ms | |
| type checking 22.7ms | |
| group_theory/subgroup.lean | |
| cumulative profiling times: | |
| compilation 9.92ms | |
| decl post-processing 1.85s | |
| elaboration 5.73s | |
| elaboration: tactic compilation 258ms | |
| elaboration: tactic execution 2.49s | |
| parsing 297ms | |
| type checking 41.6ms | |
| group_theory/submonoid.lean | |
| cumulative profiling times: | |
| compilation 3.74ms | |
| decl post-processing 159ms | |
| elaboration 1.68s | |
| elaboration: tactic compilation 45ms | |
| elaboration: tactic execution 906ms | |
| parsing 97.6ms | |
| type checking 7.61ms | |
| linear_algebra/basic.lean | |
| cumulative profiling times: | |
| compilation 8.41ms | |
| decl post-processing 55.3ms | |
| elaboration 67.3s | |
| elaboration: tactic compilation 1.23s | |
| elaboration: tactic execution 53.1s | |
| parsing 1.41s | |
| type checking 66.7ms | |
| linear_algebra/default.lean | |
| linear_algebra/dimension.lean | |
| cumulative profiling times: | |
| compilation 0.0117ms | |
| decl post-processing 1.23ms | |
| elaboration 549ms | |
| elaboration: tactic compilation 50.2ms | |
| elaboration: tactic execution 129ms | |
| parsing 92ms | |
| type checking 4.33ms | |
| linear_algebra/linear_map_module.lean | |
| cumulative profiling times: | |
| compilation 35.6ms | |
| decl post-processing 122ms | |
| elaboration 8.87s | |
| elaboration: tactic compilation 126ms | |
| elaboration: tactic execution 4.53s | |
| parsing 269ms | |
| type checking 84.5ms | |
| linear_algebra/multivariate_polynomial.lean | |
| cumulative profiling times: | |
| compilation 71.3ms | |
| decl post-processing 240ms | |
| elaboration 32.5s | |
| elaboration: tactic compilation 277ms | |
| elaboration: tactic execution 26.8s | |
| parsing 477ms | |
| type checking 207ms | |
| linear_algebra/prod_module.lean | |
| cumulative profiling times: | |
| compilation 0.242ms | |
| decl post-processing 3.23ms | |
| elaboration 2.75s | |
| elaboration: tactic compilation 29.9ms | |
| elaboration: tactic execution 2.18s | |
| parsing 25.1ms | |
| type checking 5.76ms | |
| linear_algebra/quotient_module.lean | |
| cumulative profiling times: | |
| compilation 33.3ms | |
| decl post-processing 41.4ms | |
| elaboration 3.89s | |
| elaboration: tactic compilation 126ms | |
| elaboration: tactic execution 1.91s | |
| parsing 151ms | |
| type checking 27.4ms | |
| linear_algebra/submodule.lean | |
| cumulative profiling times: | |
| compilation 50.4ms | |
| decl post-processing 80ms | |
| elaboration 13.4s | |
| elaboration: tactic compilation 436ms | |
| elaboration: tactic execution 10.2s | |
| parsing 322ms | |
| type checking 41.5ms | |
| linear_algebra/subtype_module.lean | |
| cumulative profiling times: | |
| compilation 27.9ms | |
| decl post-processing 34.5ms | |
| elaboration 4.35s | |
| elaboration: tactic compilation 32.3ms | |
| elaboration: tactic execution 2.73s | |
| parsing 40.8ms | |
| type checking 23.1ms | |
| linear_algebra/tensor_product.lean | |
| cumulative profiling times: | |
| compilation 117ms | |
| decl post-processing 304ms | |
| elaboration 21.6s | |
| elaboration: tactic compilation 271ms | |
| elaboration: tactic execution 14.6s | |
| parsing 426ms | |
| type checking 291ms | |
| logic/basic.lean | |
| cumulative profiling times: | |
| compilation 2.69ms | |
| decl post-processing 13.2ms | |
| elaboration 1.78s | |
| elaboration: tactic compilation 172ms | |
| elaboration: tactic execution 783ms | |
| parsing 178ms | |
| type checking 9.92ms | |
| logic/embedding.lean | |
| cumulative profiling times: | |
| compilation 18.5ms | |
| decl post-processing 20.8ms | |
| elaboration 1.02s | |
| elaboration: tactic compilation 40.4ms | |
| elaboration: tactic execution 775ms | |
| parsing 67.5ms | |
| type checking 7.37ms | |
| logic/function.lean | |
| cumulative profiling times: | |
| compilation 3.64ms | |
| decl post-processing 10.8ms | |
| elaboration 235ms | |
| elaboration: tactic compilation 54.2ms | |
| elaboration: tactic execution 15ms | |
| parsing 69.3ms | |
| type checking 5.03ms | |
| logic/relation.lean | |
| cumulative profiling times: | |
| compilation 0.358ms | |
| decl post-processing 3.06ms | |
| elaboration 1.21s | |
| elaboration: tactic compilation 308ms | |
| elaboration: tactic execution 269ms | |
| parsing 679ms | |
| type checking 4.88ms | |
| logic/relator.lean | |
| cumulative profiling times: | |
| compilation 0.0665ms | |
| decl post-processing 0.417ms | |
| elaboration 26.4ms | |
| elaboration: tactic compilation 9.69ms | |
| elaboration: tactic execution 0ms | |
| parsing 7.32ms | |
| type checking 0.437ms | |
| logic/schroeder_bernstein.lean | |
| cumulative profiling times: | |
| compilation 2.77ms | |
| decl post-processing 3.5ms | |
| elaboration 1.76s | |
| elaboration: tactic compilation 154ms | |
| elaboration: tactic execution 744ms | |
| parsing 92.3ms | |
| type checking 2.11ms | |
| meta/rb_map.lean | |
| cumulative profiling times: | |
| compilation 24.8ms | |
| decl post-processing 0.105ms | |
| elaboration 40ms | |
| parsing 2.15ms | |
| type checking 2.11ms | |
| number_theory/dioph.lean | |
| cumulative profiling times: | |
| compilation 38.5ms | |
| decl post-processing 88.1ms | |
| elaboration 25.2s | |
| elaboration: tactic compilation 871ms | |
| elaboration: tactic execution 21s | |
| parsing 914ms | |
| type checking 29.8ms | |
| number_theory/pell.lean | |
| cumulative profiling times: | |
| compilation 71ms | |
| decl post-processing 83.4ms | |
| elaboration 39.1s | |
| elaboration: tactic compilation 2.49s | |
| elaboration: tactic execution 28.6s | |
| parsing 3s | |
| type checking 58.9ms | |
| order/basic.lean | |
| cumulative profiling times: | |
| compilation 31.5ms | |
| decl post-processing 91.6ms | |
| elaboration 1.86s | |
| elaboration: tactic compilation 139ms | |
| elaboration: tactic execution 675ms | |
| parsing 218ms | |
| type checking 43.6ms | |
| order/boolean_algebra.lean | |
| cumulative profiling times: | |
| compilation 0.0351ms | |
| decl post-processing 2.57ms | |
| elaboration 2.78s | |
| elaboration: tactic compilation 174ms | |
| elaboration: tactic execution 1.87s | |
| parsing 168ms | |
| type checking 3.86ms | |
| order/bounded_lattice.lean | |
| cumulative profiling times: | |
| compilation 156ms | |
| decl post-processing 129ms | |
| elaboration 4.65s | |
| elaboration: tactic compilation 352ms | |
| elaboration: tactic execution 1.8s | |
| parsing 553ms | |
| type checking 99.6ms | |
| order/bounds.lean | |
| cumulative profiling times: | |
| compilation 0.477ms | |
| decl post-processing 3.69ms | |
| elaboration 1.21s | |
| elaboration: tactic compilation 68ms | |
| elaboration: tactic execution 685ms | |
| parsing 58ms | |
| type checking 5.06ms | |
| order/complete_boolean_algebra.lean | |
| cumulative profiling times: | |
| compilation 11ms | |
| decl post-processing 7.08ms | |
| elaboration 954ms | |
| elaboration: tactic compilation 34.8ms | |
| elaboration: tactic execution 523ms | |
| parsing 39.3ms | |
| type checking 7.44ms | |
| order/complete_lattice.lean | |
| cumulative profiling times: | |
| compilation 46.2ms | |
| decl post-processing 87.3ms | |
| elaboration 14.8s | |
| elaboration: tactic compilation 323ms | |
| elaboration: tactic execution 10.1s | |
| parsing 244ms | |
| type checking 87ms | |
| order/conditionally_complete_lattice.lean | |
| cumulative profiling times: | |
| compilation 40.5ms | |
| decl post-processing 73.4ms | |
| elaboration 80.4s | |
| elaboration: tactic compilation 1.48s | |
| elaboration: tactic execution 70.9s | |
| parsing 934ms | |
| type checking 74.3ms | |
| order/default.lean | |
| order/filter.lean | |
| cumulative profiling times: | |
| compilation 103ms | |
| decl post-processing 892ms | |
| elaboration 94.3s | |
| elaboration: tactic compilation 1.72s | |
| elaboration: tactic execution 76.4s | |
| parsing 2.39s | |
| type checking 893ms | |
| order/fixed_points.lean | |
| cumulative profiling times: | |
| compilation 40.1ms | |
| decl post-processing 34.9ms | |
| elaboration 590ms | |
| elaboration: tactic compilation 20.5ms | |
| elaboration: tactic execution 9ms | |
| parsing 19ms | |
| type checking 21.8ms | |
| order/galois_connection.lean | |
| cumulative profiling times: | |
| compilation 36.8ms | |
| decl post-processing 43.5ms | |
| elaboration 1.67s | |
| elaboration: tactic compilation 146ms | |
| elaboration: tactic execution 843ms | |
| parsing 100ms | |
| type checking 36.7ms | |
| order/lattice.lean | |
| cumulative profiling times: | |
| compilation 22.6ms | |
| decl post-processing 34.7ms | |
| elaboration 14.6s | |
| elaboration: tactic compilation 352ms | |
| elaboration: tactic execution 10.8s | |
| parsing 505ms | |
| type checking 25.9ms | |
| order/liminf_limsup.lean | |
| cumulative profiling times: | |
| compilation 15.4ms | |
| decl post-processing 11.8ms | |
| elaboration 10.3s | |
| elaboration: tactic compilation 142ms | |
| elaboration: tactic execution 7.98s | |
| parsing 159ms | |
| type checking 13.1ms | |
| order/order_iso.lean | |
| cumulative profiling times: | |
| compilation 30.6ms | |
| decl post-processing 44.4ms | |
| elaboration 3.75s | |
| elaboration: tactic compilation 213ms | |
| elaboration: tactic execution 1.96s | |
| parsing 303ms | |
| type checking 29.5ms | |
| order/zorn.lean | |
| cumulative profiling times: | |
| compilation 0.457ms | |
| decl post-processing 4.42ms | |
| elaboration 3.19s | |
| elaboration: tactic compilation 135ms | |
| elaboration: tactic execution 2.07s | |
| parsing 539ms | |
| type checking 3.69ms | |
| pending/default.lean | |
| ring_theory/associated.lean | |
| cumulative profiling times: | |
| compilation 53ms | |
| decl post-processing 39.1ms | |
| elaboration 21.6s | |
| elaboration: tactic compilation 596ms | |
| elaboration: tactic execution 15.8s | |
| parsing 992ms | |
| type checking 64.8ms | |
| ring_theory/ideals.lean | |
| cumulative profiling times: | |
| compilation 42.2ms | |
| decl post-processing 84.7ms | |
| elaboration 5.35s | |
| elaboration: tactic compilation 122ms | |
| elaboration: tactic execution 2.61s | |
| parsing 111ms | |
| type checking 60.2ms | |
| ring_theory/localization.lean | |
| cumulative profiling times: | |
| compilation 55ms | |
| decl post-processing 62.9ms | |
| elaboration 16.4s | |
| elaboration: tactic compilation 178ms | |
| elaboration: tactic execution 9.82s | |
| parsing 241ms | |
| type checking 34.8ms | |
| ring_theory/matrix.lean | |
| cumulative profiling times: | |
| compilation 60.4ms | |
| decl post-processing 70.7ms | |
| elaboration 15.3s | |
| elaboration: tactic compilation 137ms | |
| elaboration: tactic execution 13.3s | |
| parsing 282ms | |
| type checking 33.4ms | |
| ring_theory/noetherian.lean | |
| cumulative profiling times: | |
| compilation 0.34ms | |
| decl post-processing 2.77ms | |
| elaboration 1.91s | |
| elaboration: tactic compilation 82.2ms | |
| elaboration: tactic execution 1.08s | |
| parsing 242ms | |
| type checking 1.66ms | |
| ring_theory/principal_ideal_domain.lean | |
| cumulative profiling times: | |
| compilation 0.902ms | |
| decl post-processing 7.57ms | |
| elaboration 2.22s | |
| elaboration: tactic compilation 79.8ms | |
| elaboration: tactic execution 1.74s | |
| parsing 141ms | |
| type checking 5.03ms | |
| ring_theory/subring.lean | |
| cumulative profiling times: | |
| compilation 26ms | |
| decl post-processing 21.7ms | |
| elaboration 1.26s | |
| elaboration: tactic compilation 17.8ms | |
| elaboration: tactic execution 751ms | |
| parsing 2.12ms | |
| type checking 13.8ms | |
| ring_theory/unique_factorization_domain.lean | |
| cumulative profiling times: | |
| compilation 106ms | |
| decl post-processing 70.4ms | |
| elaboration 11.9s | |
| elaboration: tactic compilation 280ms | |
| elaboration: tactic execution 8.2s | |
| parsing 358ms | |
| type checking 94.4ms | |
| set_theory/cardinal.lean | |
| cumulative profiling times: | |
| compilation 20.7ms | |
| decl post-processing 26.7ms | |
| elaboration 30.9s | |
| elaboration: tactic compilation 744ms | |
| elaboration: tactic execution 29.1s | |
| parsing 1.16s | |
| type checking 29.1ms | |
| set_theory/cofinality.lean | |
| cumulative profiling times: | |
| compilation 0.359ms | |
| decl post-processing 5.86ms | |
| elaboration 30.4s | |
| elaboration: tactic compilation 661ms | |
| elaboration: tactic execution 29.1s | |
| parsing 1.35s | |
| type checking 6.38ms | |
| set_theory/lists.lean | |
| cumulative profiling times: | |
| compilation 73.5ms | |
| decl post-processing 39.3ms | |
| elaboration 5.44s | |
| elaboration: tactic compilation 360ms | |
| elaboration: tactic execution 4.59s | |
| parsing 490ms | |
| type checking 10ms | |
| set_theory/ordinal.lean | |
| cumulative profiling times: | |
| compilation 75.5ms | |
| decl post-processing 255ms | |
| elaboration 208s | |
| elaboration: tactic compilation 3.75s | |
| elaboration: tactic execution 179s | |
| parsing 6.85s | |
| type checking 155ms | |
| set_theory/ordinal_notation.lean | |
| cumulative profiling times: | |
| compilation 62.8ms | |
| decl post-processing 89.1ms | |
| elaboration 49.4s | |
| elaboration: tactic compilation 969ms | |
| elaboration: tactic execution 38.4s | |
| parsing 3.3s | |
| type checking 23.6ms | |
| set_theory/zfc.lean | |
| cumulative profiling times: | |
| compilation 29.6ms | |
| decl post-processing 77.3ms | |
| elaboration 7.72s | |
| elaboration: tactic compilation 425ms | |
| elaboration: tactic execution 3.72s | |
| parsing 587ms | |
| type checking 25.8ms | |
| tactic/abel.lean | |
| cumulative profiling times: | |
| compilation 117ms | |
| decl post-processing 3.02ms | |
| elaboration 5.9s | |
| elaboration: tactic compilation 115ms | |
| elaboration: tactic execution 4.3s | |
| parsing 154ms | |
| type checking 10ms | |
| tactic/algebra.lean | |
| cumulative profiling times: | |
| compilation 7.39ms | |
| decl post-processing 0.116ms | |
| elaboration 35.9ms | |
| elaboration: tactic compilation 0.182ms | |
| elaboration: tactic execution 0ms | |
| parsing 0.704ms | |
| type checking 0.644ms | |
| tactic/alias.lean | |
| cumulative profiling times: | |
| compilation 63.9ms | |
| decl post-processing 0.194ms | |
| elaboration 212ms | |
| elaboration: tactic compilation 0.32ms | |
| elaboration: tactic execution 0ms | |
| parsing 4.23ms | |
| type checking 4.79ms | |
| tactic/auto_cases.lean | |
| cumulative profiling times: | |
| compilation 64.3ms | |
| decl post-processing 0.00566ms | |
| elaboration 71.9ms | |
| parsing 10.2ms | |
| type checking 2.99ms | |
| tactic/basic.lean | |
| cumulative profiling times: | |
| compilation 346ms | |
| decl post-processing 0.143ms | |
| elaboration 696ms | |
| elaboration: tactic compilation 5.21ms | |
| elaboration: tactic execution 0ms | |
| parsing 25.6ms | |
| type checking 21.4ms | |
| tactic/cache.lean | |
| cumulative profiling times: | |
| compilation 14.4ms | |
| decl post-processing 0.0147ms | |
| elaboration 36.3ms | |
| parsing 1.37ms | |
| type checking 8.27ms | |
| tactic/chain.lean | |
| cumulative profiling times: | |
| compilation 56.9ms | |
| decl post-processing 0.106ms | |
| elaboration 137ms | |
| parsing 7.3ms | |
| type checking 2.78ms | |
| tactic/converter/binders.lean | |
| cumulative profiling times: | |
| compilation 133ms | |
| decl post-processing 0.31ms | |
| elaboration 711ms | |
| elaboration: tactic compilation 11.9ms | |
| elaboration: tactic execution 243ms | |
| parsing 19.1ms | |
| type checking 9.77ms | |
| tactic/converter/interactive.lean | |
| cumulative profiling times: | |
| compilation 29ms | |
| decl post-processing 0.0223ms | |
| elaboration 62.3ms | |
| parsing 2.83ms | |
| type checking 2.22ms | |
| tactic/converter/old_conv.lean | |
| cumulative profiling times: | |
| compilation 180ms | |
| decl post-processing 0.156ms | |
| elaboration 296ms | |
| parsing 14.8ms | |
| type checking 11.4ms | |
| tactic/default.lean | |
| tactic/explode.lean | |
| cumulative profiling times: | |
| compilation 40ms | |
| decl post-processing 1.13ms | |
| elaboration 82.3ms | |
| parsing 2.93ms | |
| type checking 3.25ms | |
| tactic/ext.lean | |
| cumulative profiling times: | |
| compilation 41.6ms | |
| decl post-processing 6.04ms | |
| elaboration 390ms | |
| elaboration: tactic compilation 7.99ms | |
| elaboration: tactic execution 45ms | |
| parsing 31.1ms | |
| type checking 4.98ms | |
| tactic/find.lean | |
| cumulative profiling times: | |
| compilation 34.9ms | |
| decl post-processing 0.0491ms | |
| elaboration 146ms | |
| parsing 4.72ms | |
| type checking 2.41ms | |
| tactic/finish.lean | |
| cumulative profiling times: | |
| compilation 187ms | |
| decl post-processing 0.62ms | |
| elaboration 451ms | |
| parsing 14.6ms | |
| type checking 12.4ms | |
| tactic/generalize_proofs.lean | |
| cumulative profiling times: | |
| compilation 4.45ms | |
| decl post-processing 0.00529ms | |
| elaboration 88.3ms | |
| parsing 2.54ms | |
| type checking 0.296ms | |
| tactic/interactive.lean | |
| cumulative profiling times: | |
| compilation 421ms | |
| decl post-processing 0.0834ms | |
| elaboration 755ms | |
| parsing 19.8ms | |
| type checking 76.5ms | |
| tactic/linarith.lean | |
| cumulative profiling times: | |
| compilation 1.57s | |
| decl post-processing 5.64ms | |
| elaboration 10.2s | |
| elaboration: tactic compilation 122ms | |
| elaboration: tactic execution 3.75s | |
| parsing 231ms | |
| type checking 54.2ms | |
| tactic/mk_iff_of_inductive_prop.lean | |
| cumulative profiling times: | |
| compilation 119ms | |
| decl post-processing 3.47ms | |
| elaboration 185ms | |
| parsing 8.1ms | |
| type checking 5.93ms | |
| tactic/norm_num.lean | |
| cumulative profiling times: | |
| compilation 1.51s | |
| decl post-processing 0.46ms | |
| elaboration 9.96s | |
| elaboration: tactic compilation 167ms | |
| elaboration: tactic execution 5.45s | |
| parsing 242ms | |
| type checking 36.2ms | |
| tactic/pi_instances.lean | |
| cumulative profiling times: | |
| compilation 32.6ms | |
| decl post-processing 0.00528ms | |
| elaboration 78.3ms | |
| elaboration: tactic compilation 2.57ms | |
| elaboration: tactic execution 0ms | |
| parsing 1.65ms | |
| type checking 1.44ms | |
| tactic/rcases.lean | |
| cumulative profiling times: | |
| compilation 71.4ms | |
| decl post-processing 5.05ms | |
| elaboration 255ms | |
| elaboration: tactic compilation 6.98ms | |
| elaboration: tactic execution 2ms | |
| parsing 31.3ms | |
| type checking 4.43ms | |
| tactic/replacer.lean | |
| cumulative profiling times: | |
| compilation 38ms | |
| decl post-processing 0.0581ms | |
| elaboration 246ms | |
| elaboration: tactic compilation 0.231ms | |
| elaboration: tactic execution 0ms | |
| parsing 5.73ms | |
| type checking 2.25ms | |
| tactic/restate_axiom.lean | |
| cumulative profiling times: | |
| compilation 23.3ms | |
| decl post-processing 0.0412ms | |
| elaboration 45.9ms | |
| parsing 1.51ms | |
| type checking 1.64ms | |
| tactic/rewrite.lean | |
| cumulative profiling times: | |
| compilation 93.5ms | |
| decl post-processing 0.0502ms | |
| elaboration 347ms | |
| parsing 12.6ms | |
| type checking 6.41ms | |
| tactic/ring.lean | |
| cumulative profiling times: | |
| compilation 125ms | |
| decl post-processing 1.33ms | |
| elaboration 7.8s | |
| elaboration: tactic compilation 123ms | |
| elaboration: tactic execution 4.72s | |
| parsing 178ms | |
| type checking 12.1ms | |
| tactic/ring2.lean | |
| cumulative profiling times: | |
| compilation 98.7ms | |
| decl post-processing 25ms | |
| elaboration 13.5s | |
| elaboration: tactic compilation 308ms | |
| elaboration: tactic execution 9.89s | |
| parsing 922ms | |
| type checking 6.28ms | |
| tactic/split_ifs.lean | |
| cumulative profiling times: | |
| compilation 21.1ms | |
| decl post-processing 0.0177ms | |
| elaboration 143ms | |
| elaboration: tactic compilation 2.27ms | |
| elaboration: tactic execution 3ms | |
| parsing 11.6ms | |
| type checking 2.25ms | |
| tactic/subtype_instance.lean | |
| cumulative profiling times: | |
| compilation 76.9ms | |
| decl post-processing 1.06ms | |
| elaboration 89.8ms | |
| parsing 14.5ms | |
| type checking 3.08ms | |
| tactic/tauto.lean | |
| cumulative profiling times: | |
| compilation 101ms | |
| decl post-processing 0.0272ms | |
| elaboration 1.02s | |
| parsing 20.8ms | |
| type checking 5.5ms | |
| tactic/tidy.lean | |
| cumulative profiling times: | |
| compilation 40.3ms | |
| decl post-processing 0.112ms | |
| elaboration 133ms | |
| elaboration: tactic compilation 2.47ms | |
| elaboration: tactic execution 0ms | |
| parsing 9.17ms | |
| type checking 2.43ms | |
| tactic/wlog.lean | |
| cumulative profiling times: | |
| compilation 234ms | |
| decl post-processing 0.0193ms | |
| elaboration 456ms | |
| parsing 12.7ms | |
| type checking 8.79ms | |
| tests/examples.lean | |
| cumulative profiling times: | |
| compilation 0.287ms | |
| decl post-processing 0.926ms | |
| elaboration 1.55s | |
| elaboration: tactic compilation 113ms | |
| elaboration: tactic execution 3.54s | |
| parsing 241ms | |
| type checking 0.968ms | |
| tests/finish1.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 278ms | |
| elaboration: tactic execution 2s | |
| parsing 67.5ms | |
| tests/finish2.lean | |
| cumulative profiling times: | |
| compilation 0.00189ms | |
| decl post-processing 0.00302ms | |
| elaboration 305ms | |
| elaboration: tactic compilation 722ms | |
| elaboration: tactic execution 13.4s | |
| parsing 196ms | |
| type checking 0.0649ms | |
| tests/finish3.lean | |
| cumulative profiling times: | |
| compilation 0.00151ms | |
| decl post-processing 0.0068ms | |
| elaboration 568ms | |
| elaboration: tactic compilation 233ms | |
| elaboration: tactic execution 3.41s | |
| parsing 60.2ms | |
| type checking 0.0804ms | |
| tests/linarith.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 163ms | |
| elaboration: tactic execution 2.34s | |
| parsing 281ms | |
| tests/mk_iff_of_inductive.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 26.3ms | |
| elaboration: tactic execution 42ms | |
| tests/norm_num.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 136ms | |
| elaboration: tactic execution 5.43s | |
| parsing 75.9ms | |
| tests/replacer.lean | |
| cumulative profiling times: | |
| compilation 16ms | |
| decl post-processing 3.26ms | |
| elaboration 16.7ms | |
| elaboration: tactic compilation 40ms | |
| elaboration: tactic execution 0ms | |
| parsing 1.95ms | |
| type checking 1.03ms | |
| tests/restate_axiom.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 14.1ms | |
| elaboration: tactic execution 0ms | |
| parsing 6ms | |
| tests/ring.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 37.5ms | |
| elaboration: tactic execution 4.83s | |
| parsing 13.3ms | |
| tests/split_ifs.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 32.5ms | |
| elaboration: tactic execution 48ms | |
| parsing 18.2ms | |
| tests/tactics.lean | |
| cumulative profiling times: | |
| compilation 5.1ms | |
| decl post-processing 10.4ms | |
| elaboration 522ms | |
| elaboration: tactic compilation 757ms | |
| elaboration: tactic execution 5.31s | |
| parsing 1.83s | |
| type checking 0.809ms | |
| tests/tidy.lean | |
| cumulative profiling times: | |
| compilation 4.01ms | |
| decl post-processing 1.07ms | |
| elaboration 519ms | |
| elaboration: tactic compilation 21.2ms | |
| elaboration: tactic execution 268ms | |
| parsing 15.5ms | |
| type checking 0.651ms |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment