-
-
Save kckennylau/afecc516f8f35d886815086b85923590 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 15.9ms | |
| decl post-processing 25.9ms | |
| elaboration 3.18s | |
| elaboration: tactic compilation 232ms | |
| elaboration: tactic execution 2s | |
| parsing 268ms | |
| type checking 36.4ms | |
| algebra/big_operators.lean | |
| cumulative profiling times: | |
| compilation 1.09ms | |
| decl post-processing 3.75s | |
| elaboration 10.7s | |
| elaboration: tactic compilation 529ms | |
| elaboration: tactic execution 12.8s | |
| parsing 937ms | |
| type checking 13.7ms | |
| algebra/char_zero.lean | |
| cumulative profiling times: | |
| compilation 0.142ms | |
| decl post-processing 3.47ms | |
| elaboration 404ms | |
| elaboration: tactic compilation 62.3ms | |
| elaboration: tactic execution 104ms | |
| parsing 42.3ms | |
| type checking 4.48ms | |
| algebra/default.lean | |
| algebra/euclidean_domain.lean | |
| cumulative profiling times: | |
| compilation 9.39ms | |
| decl post-processing 12.7ms | |
| elaboration 964ms | |
| elaboration: tactic compilation 199ms | |
| elaboration: tactic execution 408ms | |
| parsing 241ms | |
| type checking 5.64ms | |
| algebra/field.lean | |
| cumulative profiling times: | |
| compilation 9.02ms | |
| decl post-processing 6.93ms | |
| elaboration 785ms | |
| elaboration: tactic compilation 202ms | |
| elaboration: tactic execution 249ms | |
| parsing 168ms | |
| type checking 10.1ms | |
| algebra/field_power.lean | |
| cumulative profiling times: | |
| compilation 0.423ms | |
| decl post-processing 1.55ms | |
| elaboration 3.15s | |
| elaboration: tactic compilation 142ms | |
| elaboration: tactic execution 2.33s | |
| parsing 233ms | |
| type checking 3.88ms | |
| algebra/gcd_domain.lean | |
| cumulative profiling times: | |
| compilation 0.534ms | |
| decl post-processing 10.4ms | |
| elaboration 1.57s | |
| elaboration: tactic compilation 164ms | |
| elaboration: tactic execution 549ms | |
| parsing 214ms | |
| type checking 30.8ms | |
| algebra/group.lean | |
| cumulative profiling times: | |
| compilation 50.8ms | |
| decl post-processing 2.35s | |
| elaboration 2.16s | |
| elaboration: tactic compilation 388ms | |
| elaboration: tactic execution 608ms | |
| parsing 355ms | |
| type checking 31.3ms | |
| algebra/group_power.lean | |
| cumulative profiling times: | |
| compilation 3.39ms | |
| decl post-processing 101ms | |
| elaboration 5.66s | |
| elaboration: tactic compilation 561ms | |
| elaboration: tactic execution 3.41s | |
| parsing 572ms | |
| type checking 16.5ms | |
| algebra/module.lean | |
| cumulative profiling times: | |
| compilation 15.2ms | |
| decl post-processing 54.7ms | |
| elaboration 69s | |
| elaboration: tactic compilation 574ms | |
| elaboration: tactic execution 62.6s | |
| parsing 436ms | |
| type checking 50.6ms | |
| algebra/order.lean | |
| cumulative profiling times: | |
| compilation 0.29ms | |
| decl post-processing 2.17ms | |
| elaboration 279ms | |
| elaboration: tactic compilation 23.8ms | |
| elaboration: tactic execution 0ms | |
| parsing 34.7ms | |
| type checking 6.13ms | |
| algebra/order_functions.lean | |
| cumulative profiling times: | |
| compilation 1.76ms | |
| decl post-processing 4.77ms | |
| elaboration 9.37s | |
| elaboration: tactic compilation 335ms | |
| elaboration: tactic execution 7.73s | |
| parsing 268ms | |
| type checking 18.3ms | |
| algebra/ordered_field.lean | |
| cumulative profiling times: | |
| compilation 2.22ms | |
| decl post-processing 24.1ms | |
| elaboration 3.39s | |
| elaboration: tactic compilation 177ms | |
| elaboration: tactic execution 3.03s | |
| parsing 147ms | |
| type checking 37.8ms | |
| algebra/ordered_group.lean | |
| cumulative profiling times: | |
| compilation 64.8ms | |
| decl post-processing 60ms | |
| elaboration 6.76s | |
| elaboration: tactic compilation 498ms | |
| elaboration: tactic execution 3.76s | |
| parsing 506ms | |
| type checking 51.6ms | |
| algebra/ordered_ring.lean | |
| cumulative profiling times: | |
| compilation 76.6ms | |
| decl post-processing 72.4ms | |
| elaboration 6.56s | |
| elaboration: tactic compilation 262ms | |
| elaboration: tactic execution 4.8s | |
| parsing 334ms | |
| type checking 68.2ms | |
| algebra/pi_instances.lean | |
| cumulative profiling times: | |
| compilation 111ms | |
| decl post-processing 2.66s | |
| elaboration 4.68s | |
| elaboration: tactic compilation 75ms | |
| elaboration: tactic execution 4.21s | |
| parsing 42.3ms | |
| type checking 58.5ms | |
| algebra/ring.lean | |
| cumulative profiling times: | |
| compilation 14ms | |
| decl post-processing 39.6ms | |
| elaboration 7.12s | |
| elaboration: tactic compilation 437ms | |
| elaboration: tactic execution 5.47s | |
| parsing 422ms | |
| type checking 28.5ms | |
| analysis/bounded_linear_maps.lean | |
| cumulative profiling times: | |
| compilation 0.0393ms | |
| decl post-processing 0.255ms | |
| elaboration 13.2s | |
| elaboration: tactic compilation 127ms | |
| elaboration: tactic execution 13.5s | |
| parsing 149ms | |
| type checking 6.38ms | |
| analysis/complex.lean | |
| cumulative profiling times: | |
| compilation 0.323ms | |
| decl post-processing 7.27ms | |
| elaboration 1.64s | |
| elaboration: tactic compilation 39.9ms | |
| elaboration: tactic execution 1.16s | |
| parsing 79.1ms | |
| type checking 9.79ms | |
| analysis/ennreal.lean | |
| cumulative profiling times: | |
| compilation 1.5ms | |
| decl post-processing 22.8ms | |
| elaboration 36.7s | |
| elaboration: tactic compilation 469ms | |
| elaboration: tactic execution 38.5s | |
| parsing 659ms | |
| type checking 56.3ms | |
| analysis/limits.lean | |
| cumulative profiling times: | |
| compilation 0.0569ms | |
| decl post-processing 1.89ms | |
| elaboration 45.5s | |
| elaboration: tactic compilation 385ms | |
| elaboration: tactic execution 38.7s | |
| parsing 513ms | |
| type checking 10.2ms | |
| analysis/measure_theory/borel_space.lean | |
| cumulative profiling times: | |
| compilation 0.775ms | |
| decl post-processing 0.651ms | |
| elaboration 9.56s | |
| elaboration: tactic compilation 200ms | |
| elaboration: tactic execution 9.07s | |
| parsing 405ms | |
| type checking 5.85ms | |
| analysis/measure_theory/integration.lean | |
| cumulative profiling times: | |
| compilation 56.3ms | |
| decl post-processing 75.4ms | |
| elaboration 34.3s | |
| elaboration: tactic compilation 629ms | |
| elaboration: tactic execution 32.6s | |
| parsing 1.36s | |
| type checking 50.7ms | |
| analysis/measure_theory/lebesgue_measure.lean | |
| cumulative profiling times: | |
| compilation 0.1ms | |
| decl post-processing 4.38ms | |
| elaboration 41.5s | |
| elaboration: tactic compilation 413ms | |
| elaboration: tactic execution 50.2s | |
| parsing 657ms | |
| type checking 7.53ms | |
| analysis/measure_theory/measurable_space.lean | |
| cumulative profiling times: | |
| compilation 61.9ms | |
| decl post-processing 61.7ms | |
| elaboration 38.7s | |
| elaboration: tactic compilation 465ms | |
| elaboration: tactic execution 37.8s | |
| parsing 408ms | |
| type checking 28.3ms | |
| analysis/measure_theory/measure_space.lean | |
| cumulative profiling times: | |
| compilation 11.9ms | |
| decl post-processing 66.3ms | |
| elaboration 36.8s | |
| elaboration: tactic compilation 677ms | |
| elaboration: tactic execution 34.8s | |
| parsing 801ms | |
| type checking 79.2ms | |
| analysis/measure_theory/outer_measure.lean | |
| cumulative profiling times: | |
| compilation 5.56ms | |
| decl post-processing 48.6ms | |
| elaboration 56.8s | |
| elaboration: tactic compilation 456ms | |
| elaboration: tactic execution 51.8s | |
| parsing 607ms | |
| type checking 41.4ms | |
| analysis/metric_space.lean | |
| cumulative profiling times: | |
| compilation 15.2ms | |
| decl post-processing 64.9ms | |
| elaboration 65s | |
| elaboration: tactic compilation 664ms | |
| elaboration: tactic execution 59.2s | |
| parsing 654ms | |
| type checking 62.2ms | |
| analysis/nnreal.lean | |
| cumulative profiling times: | |
| compilation 0.147ms | |
| decl post-processing 9.3ms | |
| elaboration 2.01s | |
| elaboration: tactic compilation 39.6ms | |
| elaboration: tactic execution 1.4s | |
| parsing 82.2ms | |
| type checking 14.9ms | |
| analysis/normed_space.lean | |
| cumulative profiling times: | |
| compilation 24.3ms | |
| decl post-processing 65.8ms | |
| elaboration 48.1s | |
| elaboration: tactic compilation 435ms | |
| elaboration: tactic execution 44.9s | |
| parsing 572ms | |
| type checking 60.9ms | |
| analysis/polynomial.lean | |
| cumulative profiling times: | |
| compilation 0.00283ms | |
| decl post-processing 0.00746ms | |
| elaboration 1.04s | |
| elaboration: tactic compilation 23.7ms | |
| elaboration: tactic execution 1.49s | |
| parsing 62ms | |
| type checking 0.167ms | |
| analysis/probability_mass_function.lean | |
| cumulative profiling times: | |
| compilation 6.48ms | |
| decl post-processing 23.3ms | |
| elaboration 23.3s | |
| elaboration: tactic compilation 161ms | |
| elaboration: tactic execution 21.2s | |
| parsing 209ms | |
| type checking 12.6ms | |
| analysis/real.lean | |
| cumulative profiling times: | |
| compilation 0.912ms | |
| decl post-processing 52.1ms | |
| elaboration 19.9s | |
| elaboration: tactic compilation 271ms | |
| elaboration: tactic execution 16.5s | |
| parsing 705ms | |
| type checking 67ms | |
| analysis/topology/continuity.lean | |
| cumulative profiling times: | |
| compilation 3.56ms | |
| decl post-processing 21.7ms | |
| elaboration 109s | |
| elaboration: tactic compilation 1.81s | |
| elaboration: tactic execution 98.6s | |
| parsing 1.64s | |
| type checking 55ms | |
| analysis/topology/continuous_map.lean | |
| cumulative profiling times: | |
| compilation 9.67ms | |
| decl post-processing 10.2ms | |
| elaboration 4.61s | |
| elaboration: tactic compilation 61.4ms | |
| elaboration: tactic execution 4.08s | |
| parsing 83.6ms | |
| type checking 3.77ms | |
| analysis/topology/infinite_sum.lean | |
| cumulative profiling times: | |
| compilation 0.526ms | |
| decl post-processing 4.44ms | |
| elaboration 52.2s | |
| elaboration: tactic compilation 495ms | |
| elaboration: tactic execution 47.8s | |
| parsing 475ms | |
| type checking 31.4ms | |
| analysis/topology/topological_space.lean | |
| cumulative profiling times: | |
| compilation 56.6ms | |
| decl post-processing 48.9ms | |
| elaboration 7.51s | |
| elaboration: tactic compilation 898ms | |
| elaboration: tactic execution 3.21s | |
| parsing 1.02s | |
| type checking 31.5ms | |
| analysis/topology/topological_structures.lean | |
| cumulative profiling times: | |
| compilation 6.34ms | |
| decl post-processing 21.2ms | |
| elaboration 84.7s | |
| elaboration: tactic compilation 963ms | |
| elaboration: tactic execution 76.5s | |
| parsing 1.31s | |
| type checking 69.8ms | |
| analysis/topology/uniform_space.lean | |
| cumulative profiling times: | |
| compilation 63.8ms | |
| decl post-processing 50.4ms | |
| elaboration 8.53s | |
| elaboration: tactic compilation 848ms | |
| elaboration: tactic execution 3.36s | |
| parsing 1.01s | |
| type checking 47.6ms | |
| category/applicative.lean | |
| cumulative profiling times: | |
| compilation 9.03ms | |
| decl post-processing 23ms | |
| elaboration 1.59s | |
| elaboration: tactic compilation 79.1ms | |
| elaboration: tactic execution 1.11s | |
| parsing 124ms | |
| type checking 17.4ms | |
| category/basic.lean | |
| cumulative profiling times: | |
| compilation 17.8ms | |
| decl post-processing 45.7ms | |
| elaboration 1.21s | |
| elaboration: tactic compilation 85.1ms | |
| elaboration: tactic execution 767ms | |
| parsing 94.2ms | |
| type checking 20.2ms | |
| category/functor.lean | |
| cumulative profiling times: | |
| compilation 6ms | |
| decl post-processing 7.29ms | |
| elaboration 397ms | |
| elaboration: tactic compilation 40.3ms | |
| elaboration: tactic execution 242ms | |
| parsing 72.1ms | |
| type checking 3.39ms | |
| category/traversable/basic.lean | |
| cumulative profiling times: | |
| compilation 2.23ms | |
| decl post-processing 1.63ms | |
| elaboration 139ms | |
| elaboration: tactic compilation 10.8ms | |
| elaboration: tactic execution 104ms | |
| parsing 16.1ms | |
| type checking 0.997ms | |
| category/traversable/default.lean | |
| category/traversable/derive.lean | |
| cumulative profiling times: | |
| compilation 379ms | |
| decl post-processing 0.138ms | |
| elaboration 697ms | |
| parsing 28.4ms | |
| type checking 11.5ms | |
| category/traversable/equiv.lean | |
| cumulative profiling times: | |
| compilation 11.6ms | |
| decl post-processing 19.9ms | |
| elaboration 2.31s | |
| elaboration: tactic compilation 72.5ms | |
| elaboration: tactic execution 1.61s | |
| parsing 191ms | |
| type checking 10.5ms | |
| category/traversable/instances.lean | |
| cumulative profiling times: | |
| compilation 23.8ms | |
| decl post-processing 14.3ms | |
| elaboration 16.7s | |
| elaboration: tactic compilation 251ms | |
| elaboration: tactic execution 14.8s | |
| parsing 274ms | |
| type checking 18.5ms | |
| category/traversable/lemmas.lean | |
| cumulative profiling times: | |
| compilation 2.96ms | |
| decl post-processing 1.02ms | |
| elaboration 1.76s | |
| elaboration: tactic compilation 115ms | |
| elaboration: tactic execution 1.41s | |
| parsing 133ms | |
| type checking 4.77ms | |
| category_theory/category.lean | |
| cumulative profiling times: | |
| compilation 12.4ms | |
| decl post-processing 12.1ms | |
| elaboration 1.69s | |
| elaboration: tactic compilation 18.7ms | |
| elaboration: tactic execution 1.48s | |
| parsing 11.4ms | |
| type checking 5.52ms | |
| category_theory/embedding.lean | |
| cumulative profiling times: | |
| compilation 11.7ms | |
| decl post-processing 18.1ms | |
| elaboration 1.54s | |
| elaboration: tactic compilation 24.4ms | |
| elaboration: tactic execution 1.29s | |
| parsing 6.68ms | |
| type checking 9.73ms | |
| category_theory/examples/measurable_space.lean | |
| cumulative profiling times: | |
| compilation 2.38ms | |
| decl post-processing 1.48ms | |
| elaboration 86.6ms | |
| parsing 0.342ms | |
| type checking 0.472ms | |
| category_theory/examples/monoids.lean | |
| cumulative profiling times: | |
| compilation 4.13ms | |
| decl post-processing 7.48ms | |
| elaboration 626ms | |
| elaboration: tactic compilation 20.2ms | |
| elaboration: tactic execution 423ms | |
| parsing 9.75ms | |
| type checking 4.04ms | |
| category_theory/examples/rings.lean | |
| cumulative profiling times: | |
| compilation 6.4ms | |
| decl post-processing 13ms | |
| elaboration 1.3s | |
| elaboration: tactic compilation 36.2ms | |
| elaboration: tactic execution 980ms | |
| parsing 18.7ms | |
| type checking 7.51ms | |
| category_theory/examples/topological_spaces.lean | |
| cumulative profiling times: | |
| compilation 17.2ms | |
| decl post-processing 26.6ms | |
| elaboration 1.32s | |
| elaboration: tactic compilation 28.2ms | |
| elaboration: tactic execution 960ms | |
| parsing 10.5ms | |
| type checking 15.5ms | |
| category_theory/full_subcategory.lean | |
| cumulative profiling times: | |
| compilation 7.59ms | |
| decl post-processing 9.37ms | |
| elaboration 904ms | |
| elaboration: tactic compilation 14.7ms | |
| elaboration: tactic execution 770ms | |
| parsing 0.906ms | |
| type checking 3.86ms | |
| category_theory/functor.lean | |
| cumulative profiling times: | |
| compilation 13.1ms | |
| decl post-processing 14.5ms | |
| elaboration 635ms | |
| elaboration: tactic compilation 18ms | |
| elaboration: tactic execution 410ms | |
| parsing 17.3ms | |
| type checking 10.3ms | |
| category_theory/functor_category.lean | |
| cumulative profiling times: | |
| compilation 2.22ms | |
| decl post-processing 2.52ms | |
| elaboration 706ms | |
| elaboration: tactic compilation 0.887ms | |
| elaboration: tactic execution 589ms | |
| parsing 1.29ms | |
| type checking 3.98ms | |
| category_theory/groupoid.lean | |
| cumulative profiling times: | |
| compilation 1.5ms | |
| decl post-processing 1.18ms | |
| elaboration 320ms | |
| elaboration: tactic compilation 0.604ms | |
| elaboration: tactic execution 281ms | |
| parsing 0.199ms | |
| type checking 0.328ms | |
| category_theory/isomorphism.lean | |
| cumulative profiling times: | |
| compilation 17.6ms | |
| decl post-processing 35.4ms | |
| elaboration 4.15s | |
| elaboration: tactic compilation 102ms | |
| elaboration: tactic execution 3.37s | |
| parsing 287ms | |
| type checking 15.1ms | |
| category_theory/natural_isomorphism.lean | |
| cumulative profiling times: | |
| compilation 32.5ms | |
| decl post-processing 67.2ms | |
| elaboration 7s | |
| elaboration: tactic compilation 59.1ms | |
| elaboration: tactic execution 5.9s | |
| parsing 61.7ms | |
| type checking 52ms | |
| category_theory/natural_transformation.lean | |
| cumulative profiling times: | |
| compilation 10.7ms | |
| decl post-processing 16.7ms | |
| elaboration 1.92s | |
| elaboration: tactic compilation 65.1ms | |
| elaboration: tactic execution 1.55s | |
| parsing 96.2ms | |
| type checking 10.6ms | |
| category_theory/opposites.lean | |
| cumulative profiling times: | |
| compilation 7.52ms | |
| decl post-processing 6.45ms | |
| elaboration 1.04s | |
| elaboration: tactic compilation 27.4ms | |
| elaboration: tactic execution 709ms | |
| parsing 80.6ms | |
| type checking 5.07ms | |
| category_theory/products.lean | |
| cumulative profiling times: | |
| compilation 33.1ms | |
| decl post-processing 40ms | |
| elaboration 5.31s | |
| elaboration: tactic compilation 32.4ms | |
| elaboration: tactic execution 4.45s | |
| parsing 58.3ms | |
| type checking 28.1ms | |
| category_theory/types.lean | |
| cumulative profiling times: | |
| compilation 5.47ms | |
| decl post-processing 9.92ms | |
| elaboration 1.86s | |
| elaboration: tactic compilation 18.5ms | |
| elaboration: tactic execution 1.64s | |
| parsing 11.3ms | |
| type checking 9.13ms | |
| category_theory/whiskering.lean | |
| cumulative profiling times: | |
| compilation 172ms | |
| decl post-processing 1.62s | |
| elaboration 12s | |
| elaboration: tactic compilation 37.6ms | |
| elaboration: tactic execution 9.93s | |
| parsing 43.9ms | |
| type checking 1.68s | |
| category_theory/yoneda.lean | |
| cumulative profiling times: | |
| compilation 44ms | |
| decl post-processing 99.4ms | |
| elaboration 11.3s | |
| elaboration: tactic compilation 80.5ms | |
| elaboration: tactic execution 9.48s | |
| parsing 108ms | |
| type checking 112ms | |
| computability/halting.lean | |
| cumulative profiling times: | |
| compilation 0.4ms | |
| decl post-processing 4.29ms | |
| elaboration 36.5s | |
| elaboration: tactic compilation 403ms | |
| elaboration: tactic execution 35.1s | |
| parsing 588ms | |
| type checking 9.24ms | |
| computability/partrec.lean | |
| cumulative profiling times: | |
| compilation 21.1ms | |
| decl post-processing 10.5ms | |
| elaboration 149s | |
| elaboration: tactic compilation 1.19s | |
| elaboration: tactic execution 127s | |
| parsing 1.93s | |
| type checking 56.9ms | |
| computability/partrec_code.lean | |
| cumulative profiling times: | |
| compilation 19.6ms | |
| decl post-processing 17.1ms | |
| elaboration 42s | |
| elaboration: tactic compilation 566ms | |
| elaboration: tactic execution 36.5s | |
| parsing 2.96s | |
| type checking 8.23ms | |
| computability/primrec.lean | |
| cumulative profiling times: | |
| compilation 18.4ms | |
| decl post-processing 23.2ms | |
| elaboration 192s | |
| elaboration: tactic compilation 2.34s | |
| elaboration: tactic execution 175s | |
| parsing 4.28s | |
| type checking 94.3ms | |
| computability/turing_machine.lean | |
| cumulative profiling times: | |
| compilation 71.4ms | |
| decl post-processing 223ms | |
| elaboration 15.9s | |
| elaboration: tactic compilation 856ms | |
| elaboration: tactic execution 11.2s | |
| parsing 2.23s | |
| type checking 40.6ms | |
| core/data/list.lean | |
| cumulative profiling times: | |
| compilation 1.85ms | |
| decl post-processing 3.06ms | |
| elaboration 29.4ms | |
| parsing 1.7ms | |
| type checking 0.183ms | |
| core/default.lean | |
| data/analysis/filter.lean | |
| cumulative profiling times: | |
| compilation 67.1ms | |
| decl post-processing 41.2ms | |
| elaboration 7.63s | |
| elaboration: tactic compilation 105ms | |
| elaboration: tactic execution 6.76s | |
| parsing 216ms | |
| type checking 18.9ms | |
| data/analysis/topology.lean | |
| cumulative profiling times: | |
| compilation 17.7ms | |
| decl post-processing 20.1ms | |
| elaboration 8.44s | |
| elaboration: tactic compilation 70ms | |
| elaboration: tactic execution 7.4s | |
| parsing 204ms | |
| type checking 9.51ms | |
| data/array/lemmas.lean | |
| cumulative profiling times: | |
| compilation 9.1ms | |
| decl post-processing 11ms | |
| elaboration 6.14s | |
| elaboration: tactic compilation 199ms | |
| elaboration: tactic execution 5.1s | |
| parsing 259ms | |
| type checking 7.48ms | |
| data/bool.lean | |
| cumulative profiling times: | |
| compilation 2.2ms | |
| decl post-processing 8.15ms | |
| elaboration 3.81s | |
| elaboration: tactic compilation 424ms | |
| elaboration: tactic execution 1.95s | |
| parsing 135ms | |
| type checking 4ms | |
| data/buffer/basic.lean | |
| cumulative profiling times: | |
| compilation 9.5ms | |
| decl post-processing 11.2ms | |
| elaboration 2.13s | |
| elaboration: tactic compilation 55.6ms | |
| elaboration: tactic execution 1.74s | |
| parsing 114ms | |
| type checking 1.53ms | |
| data/char.lean | |
| cumulative profiling times: | |
| compilation 2.43ms | |
| decl post-processing 2.65ms | |
| elaboration 10.6ms | |
| parsing 0.347ms | |
| type checking 2.59ms | |
| data/complex/basic.lean | |
| cumulative profiling times: | |
| compilation 59.2ms | |
| decl post-processing 51.1ms | |
| elaboration 135s | |
| elaboration: tactic compilation 849ms | |
| elaboration: tactic execution 122s | |
| parsing 750ms | |
| type checking 118ms | |
| data/dlist/basic.lean | |
| cumulative profiling times: | |
| compilation 0.241ms | |
| decl post-processing 1.69ms | |
| elaboration 9.14ms | |
| parsing 0.272ms | |
| type checking 0.0289ms | |
| data/dlist/instances.lean | |
| cumulative profiling times: | |
| compilation 2.67ms | |
| decl post-processing 2.85ms | |
| elaboration 252ms | |
| elaboration: tactic compilation 3.96ms | |
| elaboration: tactic execution 216ms | |
| parsing 15.6ms | |
| type checking 0.243ms | |
| data/equiv/basic.lean | |
| cumulative profiling times: | |
| compilation 115ms | |
| decl post-processing 110ms | |
| elaboration 5.63s | |
| elaboration: tactic compilation 451ms | |
| elaboration: tactic execution 3.47s | |
| parsing 476ms | |
| type checking 39ms | |
| data/equiv/denumerable.lean | |
| cumulative profiling times: | |
| compilation 11.7ms | |
| decl post-processing 11.8ms | |
| elaboration 2.59s | |
| elaboration: tactic compilation 60.5ms | |
| elaboration: tactic execution 2.22s | |
| parsing 87.7ms | |
| type checking 3.02ms | |
| data/equiv/encodable.lean | |
| cumulative profiling times: | |
| compilation 39.7ms | |
| decl post-processing 30ms | |
| elaboration 3.29s | |
| elaboration: tactic compilation 102ms | |
| elaboration: tactic execution 2.61s | |
| parsing 169ms | |
| type checking 8.04ms | |
| data/equiv/list.lean | |
| cumulative profiling times: | |
| compilation 37.9ms | |
| decl post-processing 28.9ms | |
| elaboration 9.24s | |
| elaboration: tactic compilation 113ms | |
| elaboration: tactic execution 7.36s | |
| parsing 205ms | |
| type checking 8.33ms | |
| data/equiv/nat.lean | |
| cumulative profiling times: | |
| compilation 4.14ms | |
| decl post-processing 2.73ms | |
| elaboration 259ms | |
| elaboration: tactic compilation 10.8ms | |
| elaboration: tactic execution 190ms | |
| parsing 21.4ms | |
| type checking 0.494ms | |
| data/erased.lean | |
| cumulative profiling times: | |
| compilation 17.9ms | |
| decl post-processing 37.1ms | |
| elaboration 517ms | |
| elaboration: tactic compilation 24.3ms | |
| elaboration: tactic execution 369ms | |
| parsing 62.8ms | |
| type checking 26ms | |
| data/fin.lean | |
| cumulative profiling times: | |
| compilation 12.6ms | |
| decl post-processing 16.6ms | |
| elaboration 684ms | |
| elaboration: tactic compilation 40.2ms | |
| elaboration: tactic execution 494ms | |
| parsing 48.3ms | |
| type checking 6.49ms | |
| data/finset.lean | |
| cumulative profiling times: | |
| compilation 89.1ms | |
| decl post-processing 129ms | |
| elaboration 14.4s | |
| elaboration: tactic compilation 1.23s | |
| elaboration: tactic execution 12.1s | |
| parsing 1.59s | |
| type checking 97.9ms | |
| data/finsupp.lean | |
| cumulative profiling times: | |
| compilation 123ms | |
| decl post-processing 1.66s | |
| elaboration 7.67s | |
| elaboration: tactic compilation 536ms | |
| elaboration: tactic execution 2.85s | |
| parsing 614ms | |
| type checking 77.7ms | |
| data/fintype.lean | |
| cumulative profiling times: | |
| compilation 79.7ms | |
| decl post-processing 244ms | |
| elaboration 33.9s | |
| elaboration: tactic compilation 571ms | |
| elaboration: tactic execution 29.4s | |
| parsing 733ms | |
| type checking 24.1ms | |
| data/fp/basic.lean | |
| cumulative profiling times: | |
| compilation 84.3ms | |
| decl post-processing 13.7ms | |
| elaboration 1.53s | |
| elaboration: tactic compilation 48.7ms | |
| elaboration: tactic execution 859ms | |
| parsing 116ms | |
| type checking 8.3ms | |
| data/hash_map.lean | |
| cumulative profiling times: | |
| compilation 56.9ms | |
| decl post-processing 62.2ms | |
| elaboration 22s | |
| elaboration: tactic compilation 513ms | |
| elaboration: tactic execution 21.3s | |
| parsing 1.57s | |
| type checking 22.9ms | |
| data/holor.lean | |
| cumulative profiling times: | |
| compilation 33.1ms | |
| decl post-processing 35.9ms | |
| elaboration 22.5s | |
| elaboration: tactic compilation 323ms | |
| elaboration: tactic execution 21.4s | |
| parsing 426ms | |
| type checking 21.2ms | |
| data/int/basic.lean | |
| cumulative profiling times: | |
| compilation 42.9ms | |
| decl post-processing 54.3ms | |
| elaboration 55.8s | |
| elaboration: tactic compilation 3.18s | |
| elaboration: tactic execution 43.7s | |
| parsing 1.95s | |
| type checking 65.2ms | |
| data/int/gcd.lean | |
| cumulative profiling times: | |
| compilation 17.6ms | |
| decl post-processing 18.1ms | |
| elaboration 23.1s | |
| elaboration: tactic compilation 502ms | |
| elaboration: tactic execution 20.8s | |
| parsing 349ms | |
| type checking 22.1ms | |
| data/int/modeq.lean | |
| cumulative profiling times: | |
| compilation 1.08ms | |
| decl post-processing 1.54ms | |
| elaboration 7s | |
| elaboration: tactic compilation 300ms | |
| elaboration: tactic execution 5.92s | |
| parsing 135ms | |
| type checking 2.74ms | |
| data/lazy_list2.lean | |
| cumulative profiling times: | |
| compilation 8.41ms | |
| decl post-processing 5.49ms | |
| elaboration 1.09s | |
| elaboration: tactic compilation 26.7ms | |
| elaboration: tactic execution 715ms | |
| parsing 112ms | |
| type checking 0.691ms | |
| data/list/basic.lean | |
| cumulative profiling times: | |
| compilation 61.8ms | |
| decl post-processing 699ms | |
| elaboration 24.5s | |
| elaboration: tactic compilation 3.7s | |
| elaboration: tactic execution 10s | |
| parsing 4.89s | |
| type checking 98.9ms | |
| data/list/default.lean | |
| data/list/perm.lean | |
| cumulative profiling times: | |
| compilation 2.96ms | |
| decl post-processing 236ms | |
| elaboration 58.1s | |
| elaboration: tactic compilation 1.94s | |
| elaboration: tactic execution 53.2s | |
| parsing 2.67s | |
| type checking 36.9ms | |
| data/list/sort.lean | |
| cumulative profiling times: | |
| compilation 2.96ms | |
| decl post-processing 12.4ms | |
| elaboration 4.26s | |
| elaboration: tactic compilation 183ms | |
| elaboration: tactic execution 3.29s | |
| parsing 435ms | |
| type checking 2.57ms | |
| data/multiset.lean | |
| cumulative profiling times: | |
| compilation 291ms | |
| decl post-processing 1.99s | |
| elaboration 556s | |
| elaboration: tactic compilation 6.56s | |
| elaboration: tactic execution 504s | |
| parsing 6.76s | |
| type checking 421ms | |
| data/nat/basic.lean | |
| cumulative profiling times: | |
| compilation 14.4ms | |
| decl post-processing 21.6ms | |
| elaboration 30.8s | |
| elaboration: tactic compilation 1.58s | |
| elaboration: tactic execution 24.7s | |
| parsing 1.23s | |
| type checking 21.3ms | |
| data/nat/binomial.lean | |
| cumulative profiling times: | |
| compilation 0.00267ms | |
| decl post-processing 0.00771ms | |
| elaboration 1.42s | |
| elaboration: tactic compilation 30.6ms | |
| elaboration: tactic execution 1.1s | |
| parsing 39.3ms | |
| type checking 0.238ms | |
| data/nat/cast.lean | |
| cumulative profiling times: | |
| compilation 1.07ms | |
| decl post-processing 5.51ms | |
| elaboration 1.81s | |
| elaboration: tactic compilation 92.3ms | |
| elaboration: tactic execution 1.32s | |
| parsing 113ms | |
| type checking 5.43ms | |
| data/nat/choose.lean | |
| cumulative profiling times: | |
| compilation 0.114ms | |
| decl post-processing 1.5ms | |
| elaboration 1.9s | |
| elaboration: tactic compilation 139ms | |
| elaboration: tactic execution 1.55s | |
| parsing 202ms | |
| type checking 0.912ms | |
| data/nat/dist.lean | |
| cumulative profiling times: | |
| compilation 0.532ms | |
| decl post-processing 0.505ms | |
| elaboration 1.5s | |
| elaboration: tactic compilation 195ms | |
| elaboration: tactic execution 1.04s | |
| parsing 70.3ms | |
| type checking 1ms | |
| data/nat/gcd.lean | |
| cumulative profiling times: | |
| compilation 0.933ms | |
| decl post-processing 0.929ms | |
| elaboration 986ms | |
| elaboration: tactic compilation 245ms | |
| elaboration: tactic execution 300ms | |
| parsing 184ms | |
| type checking 4.64ms | |
| data/nat/modeq.lean | |
| cumulative profiling times: | |
| compilation 3.85ms | |
| decl post-processing 1.99ms | |
| elaboration 2.98s | |
| elaboration: tactic compilation 139ms | |
| elaboration: tactic execution 2.51s | |
| parsing 196ms | |
| type checking 1.64ms | |
| data/nat/pairing.lean | |
| cumulative profiling times: | |
| compilation 2.11ms | |
| decl post-processing 0.916ms | |
| elaboration 7.16s | |
| elaboration: tactic compilation 137ms | |
| elaboration: tactic execution 6.37s | |
| parsing 276ms | |
| type checking 0.621ms | |
| data/nat/prime.lean | |
| cumulative profiling times: | |
| compilation 3.2ms | |
| decl post-processing 6.7ms | |
| elaboration 6.58s | |
| elaboration: tactic compilation 446ms | |
| elaboration: tactic execution 3.91s | |
| parsing 431ms | |
| type checking 8.31ms | |
| data/nat/sqrt.lean | |
| cumulative profiling times: | |
| compilation 1.05ms | |
| decl post-processing 1.18ms | |
| elaboration 2.76s | |
| elaboration: tactic compilation 187ms | |
| elaboration: tactic execution 2.11s | |
| parsing 291ms | |
| type checking 1.77ms | |
| data/nat/totient.lean | |
| cumulative profiling times: | |
| compilation 0.648ms | |
| decl post-processing 0.314ms | |
| elaboration 3.12s | |
| elaboration: tactic compilation 72.5ms | |
| elaboration: tactic execution 2.58s | |
| parsing 93.1ms | |
| type checking 0.741ms | |
| data/num/basic.lean | |
| cumulative profiling times: | |
| compilation 49ms | |
| decl post-processing 106ms | |
| elaboration 811ms | |
| elaboration: tactic compilation 45.5ms | |
| elaboration: tactic execution 188ms | |
| parsing 60.3ms | |
| type checking 3.84ms | |
| data/num/bitwise.lean | |
| cumulative profiling times: | |
| compilation 2.11ms | |
| decl post-processing 25.1ms | |
| elaboration 167ms | |
| parsing 5.56ms | |
| type checking 0.243ms | |
| data/num/lemmas.lean | |
| cumulative profiling times: | |
| compilation 58.3ms | |
| decl post-processing 31.5ms | |
| elaboration 25.2s | |
| elaboration: tactic compilation 1.81s | |
| elaboration: tactic execution 18s | |
| parsing 1.92s | |
| type checking 37.6ms | |
| data/option.lean | |
| cumulative profiling times: | |
| compilation 5.64ms | |
| decl post-processing 27.1ms | |
| elaboration 2.52s | |
| elaboration: tactic compilation 157ms | |
| elaboration: tactic execution 1.9s | |
| parsing 210ms | |
| type checking 9.81ms | |
| data/padics/default.lean | |
| data/padics/hensel.lean | |
| cumulative profiling times: | |
| compilation 1.35ms | |
| decl post-processing 54.8ms | |
| elaboration 54s | |
| elaboration: tactic compilation 554ms | |
| elaboration: tactic execution 45.7s | |
| parsing 589ms | |
| type checking 81.1ms | |
| data/padics/padic_integers.lean | |
| cumulative profiling times: | |
| compilation 5.96ms | |
| decl post-processing 48.8ms | |
| elaboration 41.9s | |
| elaboration: tactic compilation 340ms | |
| elaboration: tactic execution 39.7s | |
| parsing 415ms | |
| type checking 32.7ms | |
| data/padics/padic_norm.lean | |
| cumulative profiling times: | |
| compilation 9.78ms | |
| decl post-processing 17.3ms | |
| elaboration 163s | |
| elaboration: tactic compilation 1.72s | |
| elaboration: tactic execution 148s | |
| parsing 3.2s | |
| type checking 28.1ms | |
| data/padics/padic_numbers.lean | |
| cumulative profiling times: | |
| compilation 56.8ms | |
| decl post-processing 90ms | |
| elaboration 120s | |
| elaboration: tactic compilation 1.15s | |
| elaboration: tactic execution 109s | |
| parsing 1.92s | |
| type checking 127ms | |
| data/pfun.lean | |
| cumulative profiling times: | |
| compilation 33.2ms | |
| decl post-processing 108ms | |
| elaboration 4.89s | |
| elaboration: tactic compilation 229ms | |
| elaboration: tactic execution 3.9s | |
| parsing 312ms | |
| type checking 71ms | |
| data/pnat.lean | |
| cumulative profiling times: | |
| compilation 6.96ms | |
| decl post-processing 8.28ms | |
| elaboration 43.8ms | |
| parsing 3.29ms | |
| type checking 3.92ms | |
| data/polynomial.lean | |
| cumulative profiling times: | |
| compilation 118ms | |
| decl post-processing 247ms | |
| elaboration 38.2s | |
| elaboration: tactic compilation 1.53s | |
| elaboration: tactic execution 25.1s | |
| parsing 1.69s | |
| type checking 147ms | |
| data/prod.lean | |
| cumulative profiling times: | |
| compilation 3.65ms | |
| decl post-processing 10.3ms | |
| elaboration 482ms | |
| elaboration: tactic compilation 50.8ms | |
| elaboration: tactic execution 309ms | |
| parsing 55.9ms | |
| type checking 2.73ms | |
| data/quot.lean | |
| cumulative profiling times: | |
| compilation 22.9ms | |
| decl post-processing 36.7ms | |
| elaboration 223ms | |
| elaboration: tactic compilation 12.4ms | |
| elaboration: tactic execution 47ms | |
| parsing 21.5ms | |
| type checking 22.1ms | |
| data/rat.lean | |
| cumulative profiling times: | |
| compilation 67.4ms | |
| decl post-processing 118ms | |
| elaboration 169s | |
| elaboration: tactic compilation 2.7s | |
| elaboration: tactic execution 153s | |
| parsing 3.18s | |
| type checking 102ms | |
| data/real/basic.lean | |
| cumulative profiling times: | |
| compilation 27.1ms | |
| decl post-processing 156ms | |
| elaboration 50.5s | |
| elaboration: tactic compilation 836ms | |
| elaboration: tactic execution 49.6s | |
| parsing 1.15s | |
| type checking 732ms | |
| data/real/cau_seq.lean | |
| cumulative profiling times: | |
| compilation 63.2ms | |
| decl post-processing 79ms | |
| elaboration 43.4s | |
| elaboration: tactic compilation 719ms | |
| elaboration: tactic execution 37.6s | |
| parsing 1.14s | |
| type checking 90.1ms | |
| data/real/cau_seq_completion.lean | |
| cumulative profiling times: | |
| compilation 33.4ms | |
| decl post-processing 44.8ms | |
| elaboration 6.51s | |
| elaboration: tactic compilation 83.4ms | |
| elaboration: tactic execution 5.14s | |
| parsing 166ms | |
| type checking 52.3ms | |
| data/real/cau_seq_filter.lean | |
| cumulative profiling times: | |
| compilation 0.506ms | |
| decl post-processing 20.5ms | |
| elaboration 15.3s | |
| elaboration: tactic compilation 139ms | |
| elaboration: tactic execution 13.6s | |
| parsing 580ms | |
| type checking 20.6ms | |
| data/real/ennreal.lean | |
| cumulative profiling times: | |
| compilation 0.924ms | |
| decl post-processing 16.6ms | |
| elaboration 136s | |
| elaboration: tactic compilation 1.28s | |
| elaboration: tactic execution 121s | |
| parsing 1.2s | |
| type checking 43ms | |
| data/real/irrational.lean | |
| cumulative profiling times: | |
| compilation 0.11ms | |
| decl post-processing 0.4ms | |
| elaboration 889ms | |
| elaboration: tactic compilation 24.4ms | |
| elaboration: tactic execution 835ms | |
| parsing 161ms | |
| type checking 0.136ms | |
| data/real/nnreal.lean | |
| cumulative profiling times: | |
| compilation 70.5ms | |
| decl post-processing 63.9ms | |
| elaboration 43.6s | |
| elaboration: tactic compilation 602ms | |
| elaboration: tactic execution 37.9s | |
| parsing 406ms | |
| type checking 48.9ms | |
| data/semiquot.lean | |
| cumulative profiling times: | |
| compilation 35.9ms | |
| decl post-processing 111ms | |
| elaboration 2.88s | |
| elaboration: tactic compilation 83.3ms | |
| elaboration: tactic execution 2.21s | |
| parsing 90.1ms | |
| type checking 103ms | |
| data/seq/computation.lean | |
| cumulative profiling times: | |
| compilation 52.6ms | |
| decl post-processing 118ms | |
| elaboration 13.4s | |
| elaboration: tactic compilation 947ms | |
| elaboration: tactic execution 11s | |
| parsing 1.14s | |
| type checking 59.7ms | |
| data/seq/parallel.lean | |
| cumulative profiling times: | |
| compilation 7.59ms | |
| decl post-processing 15.9ms | |
| elaboration 4.59s | |
| elaboration: tactic compilation 213ms | |
| elaboration: tactic execution 3.81s | |
| parsing 911ms | |
| type checking 2.35ms | |
| data/seq/seq.lean | |
| cumulative profiling times: | |
| compilation 65.9ms | |
| decl post-processing 166ms | |
| elaboration 34.1s | |
| elaboration: tactic compilation 1.34s | |
| elaboration: tactic execution 34.5s | |
| parsing 1.78s | |
| type checking 99.2ms | |
| data/seq/wseq.lean | |
| cumulative profiling times: | |
| compilation 151ms | |
| decl post-processing 121ms | |
| elaboration 151s | |
| elaboration: tactic compilation 3.34s | |
| elaboration: tactic execution 142s | |
| parsing 4.31s | |
| type checking 59.2ms | |
| data/set/basic.lean | |
| cumulative profiling times: | |
| compilation 8.2ms | |
| decl post-processing 117ms | |
| elaboration 175s | |
| elaboration: tactic compilation 3.73s | |
| elaboration: tactic execution 152s | |
| parsing 2.59s | |
| type checking 176ms | |
| data/set/countable.lean | |
| cumulative profiling times: | |
| compilation 0.167ms | |
| decl post-processing 1.51ms | |
| elaboration 5.58s | |
| elaboration: tactic compilation 131ms | |
| elaboration: tactic execution 6.79s | |
| parsing 173ms | |
| type checking 2.21ms | |
| data/set/default.lean | |
| data/set/disjointed.lean | |
| cumulative profiling times: | |
| compilation 0.18ms | |
| decl post-processing 1.09ms | |
| elaboration 7.38s | |
| elaboration: tactic compilation 96.3ms | |
| elaboration: tactic execution 6.63s | |
| parsing 132ms | |
| type checking 1.85ms | |
| data/set/enumerate.lean | |
| cumulative profiling times: | |
| compilation 0.329ms | |
| decl post-processing 1.27ms | |
| elaboration 4.03s | |
| elaboration: tactic compilation 70.5ms | |
| elaboration: tactic execution 3.55s | |
| parsing 243ms | |
| type checking 0.464ms | |
| data/set/finite.lean | |
| cumulative profiling times: | |
| compilation 47.6ms | |
| decl post-processing 50.5ms | |
| elaboration 17.6s | |
| elaboration: tactic compilation 339ms | |
| elaboration: tactic execution 19.3s | |
| parsing 508ms | |
| type checking 21.1ms | |
| data/set/function.lean | |
| cumulative profiling times: | |
| compilation 1.15ms | |
| decl post-processing 6.3ms | |
| elaboration 383ms | |
| elaboration: tactic compilation 53.7ms | |
| elaboration: tactic execution 124ms | |
| parsing 52.2ms | |
| type checking 5.06ms | |
| data/set/intervals.lean | |
| cumulative profiling times: | |
| compilation 0.455ms | |
| decl post-processing 4.12ms | |
| elaboration 4.78s | |
| elaboration: tactic compilation 70.3ms | |
| elaboration: tactic execution 4.12s | |
| parsing 132ms | |
| type checking 4.2ms | |
| data/set/lattice.lean | |
| cumulative profiling times: | |
| compilation 28.6ms | |
| decl post-processing 208ms | |
| elaboration 102s | |
| elaboration: tactic compilation 1.38s | |
| elaboration: tactic execution 90.7s | |
| parsing 1.21s | |
| type checking 206ms | |
| data/sigma/basic.lean | |
| cumulative profiling times: | |
| compilation 6.26ms | |
| decl post-processing 8.99ms | |
| elaboration 162ms | |
| elaboration: tactic compilation 5.45ms | |
| elaboration: tactic execution 13ms | |
| parsing 4.03ms | |
| type checking 1.18ms | |
| data/sigma/default.lean | |
| data/stream/basic.lean | |
| data/string.lean | |
| cumulative profiling times: | |
| compilation 4.99ms | |
| decl post-processing 4.28ms | |
| elaboration 1.32s | |
| elaboration: tactic compilation 54.4ms | |
| elaboration: tactic execution 1.21s | |
| parsing 63.2ms | |
| type checking 1.36ms | |
| data/subtype.lean | |
| cumulative profiling times: | |
| compilation 3.1ms | |
| decl post-processing 4.47ms | |
| elaboration 126ms | |
| elaboration: tactic compilation 18ms | |
| elaboration: tactic execution 10ms | |
| parsing 22.8ms | |
| type checking 3.02ms | |
| data/sum.lean | |
| cumulative profiling times: | |
| compilation 1.87ms | |
| decl post-processing 7.77ms | |
| elaboration 191ms | |
| elaboration: tactic compilation 45.2ms | |
| elaboration: tactic execution 26ms | |
| parsing 51.7ms | |
| type checking 2.06ms | |
| data/vector2.lean | |
| cumulative profiling times: | |
| compilation 8.86ms | |
| decl post-processing 22.5ms | |
| elaboration 6.65s | |
| elaboration: tactic compilation 153ms | |
| elaboration: tactic execution 5.45s | |
| parsing 180ms | |
| type checking 5.92ms | |
| data/zmod/basic.lean | |
| cumulative profiling times: | |
| compilation 29.4ms | |
| decl post-processing 27.1ms | |
| elaboration 12s | |
| elaboration: tactic compilation 388ms | |
| elaboration: tactic execution 10.7s | |
| parsing 471ms | |
| type checking 22.2ms | |
| data/zmod/quadratic_reciprocity.lean | |
| cumulative profiling times: | |
| compilation 19.5ms | |
| decl post-processing 8.15ms | |
| elaboration 101s | |
| elaboration: tactic compilation 1.46s | |
| elaboration: tactic execution 101s | |
| parsing 1.65s | |
| type checking 34.8ms | |
| field_theory/finite.lean | |
| cumulative profiling times: | |
| compilation 11.3ms | |
| decl post-processing 10.4ms | |
| elaboration 8.94s | |
| elaboration: tactic compilation 167ms | |
| elaboration: tactic execution 7.21s | |
| parsing 297ms | |
| type checking 11.6ms | |
| field_theory/subfield.lean | |
| cumulative profiling times: | |
| compilation 9.73ms | |
| decl post-processing 10.3ms | |
| elaboration 818ms | |
| elaboration: tactic compilation 3.63ms | |
| elaboration: tactic execution 719ms | |
| parsing 0.393ms | |
| type checking 7.69ms | |
| group_theory/abelianization.lean | |
| cumulative profiling times: | |
| compilation 16.8ms | |
| decl post-processing 8.66ms | |
| elaboration 1.59s | |
| elaboration: tactic compilation 55.9ms | |
| elaboration: tactic execution 1.19s | |
| parsing 97ms | |
| type checking 4.71ms | |
| group_theory/coset.lean | |
| cumulative profiling times: | |
| compilation 7.16ms | |
| decl post-processing 5.23s | |
| elaboration 4.55s | |
| elaboration: tactic compilation 122ms | |
| elaboration: tactic execution 3.51s | |
| parsing 164ms | |
| type checking 6.77ms | |
| group_theory/free_abelian_group.lean | |
| cumulative profiling times: | |
| compilation 6.21ms | |
| decl post-processing 7.54ms | |
| elaboration 1.45s | |
| elaboration: tactic compilation 18.3ms | |
| elaboration: tactic execution 1.17s | |
| parsing 41.6ms | |
| type checking 3.84ms | |
| group_theory/free_group.lean | |
| cumulative profiling times: | |
| compilation 52.7ms | |
| decl post-processing 85.5ms | |
| elaboration 57.9s | |
| elaboration: tactic compilation 763ms | |
| elaboration: tactic execution 53.8s | |
| parsing 1.22s | |
| type checking 39ms | |
| group_theory/group_action.lean | |
| cumulative profiling times: | |
| compilation 3.45ms | |
| decl post-processing 15.1ms | |
| elaboration 1.49s | |
| elaboration: tactic compilation 47.7ms | |
| elaboration: tactic execution 1.01s | |
| parsing 63.2ms | |
| type checking 7.07ms | |
| group_theory/order_of_element.lean | |
| cumulative profiling times: | |
| compilation 13.2ms | |
| decl post-processing 8.49ms | |
| elaboration 22s | |
| elaboration: tactic compilation 254ms | |
| elaboration: tactic execution 21.9s | |
| parsing 221ms | |
| type checking 9.04ms | |
| group_theory/perm.lean | |
| cumulative profiling times: | |
| compilation 28ms | |
| decl post-processing 59.8ms | |
| elaboration 72.2s | |
| elaboration: tactic compilation 1.09s | |
| elaboration: tactic execution 67.8s | |
| parsing 1.41s | |
| type checking 64.8ms | |
| group_theory/quotient_group.lean | |
| cumulative profiling times: | |
| compilation 12.3ms | |
| decl post-processing 278ms | |
| elaboration 1.06s | |
| elaboration: tactic compilation 33ms | |
| elaboration: tactic execution 361ms | |
| parsing 42.5ms | |
| type checking 15.6ms | |
| group_theory/subgroup.lean | |
| cumulative profiling times: | |
| compilation 13.6ms | |
| decl post-processing 1.52s | |
| elaboration 7s | |
| elaboration: tactic compilation 270ms | |
| elaboration: tactic execution 4.9s | |
| parsing 280ms | |
| type checking 29.8ms | |
| group_theory/submonoid.lean | |
| cumulative profiling times: | |
| compilation 3.57ms | |
| decl post-processing 149ms | |
| elaboration 2.2s | |
| elaboration: tactic compilation 56.4ms | |
| elaboration: tactic execution 1.81s | |
| parsing 108ms | |
| type checking 5.64ms | |
| linear_algebra/basic.lean | |
| cumulative profiling times: | |
| compilation 14.3ms | |
| decl post-processing 72.7ms | |
| elaboration 196s | |
| elaboration: tactic compilation 1.75s | |
| elaboration: tactic execution 175s | |
| parsing 2.08s | |
| type checking 136ms | |
| linear_algebra/default.lean | |
| linear_algebra/dimension.lean | |
| cumulative profiling times: | |
| compilation 0.0279ms | |
| decl post-processing 0.911ms | |
| elaboration 529ms | |
| elaboration: tactic compilation 42.9ms | |
| elaboration: tactic execution 171ms | |
| parsing 85.1ms | |
| type checking 2.93ms | |
| linear_algebra/linear_map_module.lean | |
| cumulative profiling times: | |
| compilation 33.7ms | |
| decl post-processing 89.8ms | |
| elaboration 7.18s | |
| elaboration: tactic compilation 118ms | |
| elaboration: tactic execution 5.15s | |
| parsing 263ms | |
| type checking 66.8ms | |
| linear_algebra/multivariate_polynomial.lean | |
| cumulative profiling times: | |
| compilation 92.5ms | |
| decl post-processing 337ms | |
| elaboration 79.8s | |
| elaboration: tactic compilation 599ms | |
| elaboration: tactic execution 69s | |
| parsing 568ms | |
| type checking 331ms | |
| linear_algebra/prod_module.lean | |
| cumulative profiling times: | |
| compilation 0.264ms | |
| decl post-processing 2.25ms | |
| elaboration 2.46s | |
| elaboration: tactic compilation 30.4ms | |
| elaboration: tactic execution 2.87s | |
| parsing 50.3ms | |
| type checking 3.44ms | |
| linear_algebra/quotient_module.lean | |
| cumulative profiling times: | |
| compilation 25.9ms | |
| decl post-processing 25ms | |
| elaboration 3.24s | |
| elaboration: tactic compilation 115ms | |
| elaboration: tactic execution 2.28s | |
| parsing 171ms | |
| type checking 15.2ms | |
| linear_algebra/submodule.lean | |
| cumulative profiling times: | |
| compilation 44.2ms | |
| decl post-processing 57.1ms | |
| elaboration 15.6s | |
| elaboration: tactic compilation 449ms | |
| elaboration: tactic execution 15.3s | |
| parsing 288ms | |
| type checking 31.6ms | |
| linear_algebra/subtype_module.lean | |
| cumulative profiling times: | |
| compilation 22.9ms | |
| decl post-processing 21.8ms | |
| elaboration 3.94s | |
| elaboration: tactic compilation 42.8ms | |
| elaboration: tactic execution 3.38s | |
| parsing 44.3ms | |
| type checking 14.9ms | |
| linear_algebra/tensor_product.lean | |
| cumulative profiling times: | |
| compilation 88.2ms | |
| decl post-processing 189ms | |
| elaboration 19.7s | |
| elaboration: tactic compilation 253ms | |
| elaboration: tactic execution 15.4s | |
| parsing 405ms | |
| type checking 176ms | |
| logic/basic.lean | |
| cumulative profiling times: | |
| compilation 4.4ms | |
| decl post-processing 18ms | |
| elaboration 2.04s | |
| elaboration: tactic compilation 200ms | |
| elaboration: tactic execution 1.29s | |
| parsing 201ms | |
| type checking 14.8ms | |
| logic/embedding.lean | |
| cumulative profiling times: | |
| compilation 22.9ms | |
| decl post-processing 22.9ms | |
| elaboration 1.07s | |
| elaboration: tactic compilation 43.1ms | |
| elaboration: tactic execution 1.2s | |
| parsing 84ms | |
| type checking 8.76ms | |
| logic/function.lean | |
| cumulative profiling times: | |
| compilation 3.55ms | |
| decl post-processing 8.99ms | |
| elaboration 252ms | |
| elaboration: tactic compilation 48.4ms | |
| elaboration: tactic execution 29ms | |
| parsing 72.7ms | |
| type checking 4.36ms | |
| logic/relation.lean | |
| cumulative profiling times: | |
| compilation 0.543ms | |
| decl post-processing 2.95ms | |
| elaboration 1.17s | |
| elaboration: tactic compilation 295ms | |
| elaboration: tactic execution 365ms | |
| parsing 590ms | |
| type checking 3.71ms | |
| logic/relator.lean | |
| cumulative profiling times: | |
| compilation 0.131ms | |
| decl post-processing 0.516ms | |
| elaboration 53.8ms | |
| elaboration: tactic compilation 11.2ms | |
| elaboration: tactic execution 15ms | |
| parsing 15.2ms | |
| type checking 0.623ms | |
| logic/schroeder_bernstein.lean | |
| cumulative profiling times: | |
| compilation 1.92ms | |
| decl post-processing 2.06ms | |
| elaboration 1.45s | |
| elaboration: tactic compilation 116ms | |
| elaboration: tactic execution 982ms | |
| parsing 92.3ms | |
| type checking 1.48ms | |
| meta/rb_map.lean | |
| cumulative profiling times: | |
| compilation 17.9ms | |
| decl post-processing 0.106ms | |
| elaboration 48.7ms | |
| parsing 1.62ms | |
| type checking 1.19ms | |
| number_theory/dioph.lean | |
| cumulative profiling times: | |
| compilation 53.4ms | |
| decl post-processing 84.9ms | |
| elaboration 47.8s | |
| elaboration: tactic compilation 956ms | |
| elaboration: tactic execution 45.3s | |
| parsing 740ms | |
| type checking 37.6ms | |
| number_theory/pell.lean | |
| cumulative profiling times: | |
| compilation 156ms | |
| decl post-processing 147ms | |
| elaboration 139s | |
| elaboration: tactic compilation 4.67s | |
| elaboration: tactic execution 133s | |
| parsing 4.48s | |
| type checking 99.4ms | |
| order/basic.lean | |
| cumulative profiling times: | |
| compilation 25ms | |
| decl post-processing 69.6ms | |
| elaboration 1.88s | |
| elaboration: tactic compilation 162ms | |
| elaboration: tactic execution 989ms | |
| parsing 227ms | |
| type checking 30.7ms | |
| order/boolean_algebra.lean | |
| cumulative profiling times: | |
| compilation 0.0775ms | |
| decl post-processing 2.78ms | |
| elaboration 5.48s | |
| elaboration: tactic compilation 222ms | |
| elaboration: tactic execution 4.62s | |
| parsing 220ms | |
| type checking 7ms | |
| order/bounded_lattice.lean | |
| cumulative profiling times: | |
| compilation 104ms | |
| decl post-processing 82.4ms | |
| elaboration 4.08s | |
| elaboration: tactic compilation 315ms | |
| elaboration: tactic execution 2.32s | |
| parsing 531ms | |
| type checking 58.7ms | |
| order/bounds.lean | |
| cumulative profiling times: | |
| compilation 0.733ms | |
| decl post-processing 3.43ms | |
| elaboration 2.23s | |
| elaboration: tactic compilation 92.1ms | |
| elaboration: tactic execution 1.79s | |
| parsing 146ms | |
| type checking 7.03ms | |
| order/complete_boolean_algebra.lean | |
| cumulative profiling times: | |
| compilation 6.39ms | |
| decl post-processing 3.77ms | |
| elaboration 978ms | |
| elaboration: tactic compilation 32.6ms | |
| elaboration: tactic execution 748ms | |
| parsing 44.9ms | |
| type checking 4.06ms | |
| order/complete_lattice.lean | |
| cumulative profiling times: | |
| compilation 35.4ms | |
| decl post-processing 72.1ms | |
| elaboration 22.7s | |
| elaboration: tactic compilation 567ms | |
| elaboration: tactic execution 17.1s | |
| parsing 343ms | |
| type checking 95ms | |
| order/conditionally_complete_lattice.lean | |
| cumulative profiling times: | |
| compilation 14.7ms | |
| decl post-processing 48.8ms | |
| elaboration 32.6s | |
| elaboration: tactic compilation 1.06s | |
| elaboration: tactic execution 31.7s | |
| parsing 667ms | |
| type checking 52.9ms | |
| order/default.lean | |
| order/filter.lean | |
| cumulative profiling times: | |
| compilation 74.8ms | |
| decl post-processing 453ms | |
| elaboration 14.3s | |
| elaboration: tactic compilation 1.24s | |
| elaboration: tactic execution 8.11s | |
| parsing 1.64s | |
| type checking 428ms | |
| order/fixed_points.lean | |
| cumulative profiling times: | |
| compilation 28.9ms | |
| decl post-processing 21.3ms | |
| elaboration 478ms | |
| elaboration: tactic compilation 20.5ms | |
| elaboration: tactic execution 14ms | |
| parsing 22.8ms | |
| type checking 14.2ms | |
| order/galois_connection.lean | |
| cumulative profiling times: | |
| compilation 32.7ms | |
| decl post-processing 30.7ms | |
| elaboration 2.26s | |
| elaboration: tactic compilation 158ms | |
| elaboration: tactic execution 1.48s | |
| parsing 112ms | |
| type checking 27.7ms | |
| order/lattice.lean | |
| cumulative profiling times: | |
| compilation 17.6ms | |
| decl post-processing 31.2ms | |
| elaboration 23.1s | |
| elaboration: tactic compilation 605ms | |
| elaboration: tactic execution 20.5s | |
| parsing 608ms | |
| type checking 23.9ms | |
| order/liminf_limsup.lean | |
| cumulative profiling times: | |
| compilation 18.3ms | |
| decl post-processing 9.71ms | |
| elaboration 21.9s | |
| elaboration: tactic compilation 189ms | |
| elaboration: tactic execution 19.6s | |
| parsing 141ms | |
| type checking 14.6ms | |
| order/order_iso.lean | |
| cumulative profiling times: | |
| compilation 22.9ms | |
| decl post-processing 35.4ms | |
| elaboration 3.81s | |
| elaboration: tactic compilation 177ms | |
| elaboration: tactic execution 2.88s | |
| parsing 271ms | |
| type checking 17.9ms | |
| order/zorn.lean | |
| cumulative profiling times: | |
| compilation 0.535ms | |
| decl post-processing 3.59ms | |
| elaboration 5.02s | |
| elaboration: tactic compilation 183ms | |
| elaboration: tactic execution 4.08s | |
| parsing 384ms | |
| type checking 3.32ms | |
| pending/default.lean | |
| ring_theory/associated.lean | |
| cumulative profiling times: | |
| compilation 40.9ms | |
| decl post-processing 30.3ms | |
| elaboration 32.7s | |
| elaboration: tactic compilation 473ms | |
| elaboration: tactic execution 28.5s | |
| parsing 777ms | |
| type checking 44.3ms | |
| ring_theory/determinant.lean | |
| cumulative profiling times: | |
| compilation 7.99ms | |
| decl post-processing 6.64ms | |
| elaboration 6.75s | |
| elaboration: tactic compilation 123ms | |
| elaboration: tactic execution 5.74s | |
| parsing 226ms | |
| type checking 4.79ms | |
| ring_theory/ideals.lean | |
| cumulative profiling times: | |
| compilation 34.7ms | |
| decl post-processing 55.2ms | |
| elaboration 4.8s | |
| elaboration: tactic compilation 125ms | |
| elaboration: tactic execution 3.38s | |
| parsing 113ms | |
| type checking 41ms | |
| ring_theory/localization.lean | |
| cumulative profiling times: | |
| compilation 51.6ms | |
| decl post-processing 43.1ms | |
| elaboration 14.1s | |
| elaboration: tactic compilation 157ms | |
| elaboration: tactic execution 11s | |
| parsing 292ms | |
| type checking 24.4ms | |
| ring_theory/matrix.lean | |
| cumulative profiling times: | |
| compilation 89.5ms | |
| decl post-processing 89.6ms | |
| elaboration 32.7s | |
| elaboration: tactic compilation 239ms | |
| elaboration: tactic execution 29.7s | |
| parsing 334ms | |
| type checking 61.5ms | |
| ring_theory/noetherian.lean | |
| cumulative profiling times: | |
| compilation 2.84ms | |
| decl post-processing 4.1ms | |
| elaboration 4.1s | |
| elaboration: tactic compilation 93.4ms | |
| elaboration: tactic execution 4.44s | |
| parsing 266ms | |
| type checking 1.58ms | |
| ring_theory/principal_ideal_domain.lean | |
| cumulative profiling times: | |
| compilation 0.942ms | |
| decl post-processing 6.34ms | |
| elaboration 2.13s | |
| elaboration: tactic compilation 84.7ms | |
| elaboration: tactic execution 2.43s | |
| parsing 133ms | |
| type checking 4.45ms | |
| ring_theory/subring.lean | |
| cumulative profiling times: | |
| compilation 23.1ms | |
| decl post-processing 18.5ms | |
| elaboration 1.19s | |
| elaboration: tactic compilation 14.5ms | |
| elaboration: tactic execution 1.01s | |
| parsing 4.79ms | |
| type checking 10.7ms | |
| ring_theory/unique_factorization_domain.lean | |
| cumulative profiling times: | |
| compilation 66.2ms | |
| decl post-processing 43.6ms | |
| elaboration 11.4s | |
| elaboration: tactic compilation 245ms | |
| elaboration: tactic execution 9.05s | |
| parsing 341ms | |
| type checking 59.5ms | |
| set_theory/cardinal.lean | |
| cumulative profiling times: | |
| compilation 20.8ms | |
| decl post-processing 34.2ms | |
| elaboration 106s | |
| elaboration: tactic compilation 2.09s | |
| elaboration: tactic execution 106s | |
| parsing 2.12s | |
| type checking 52.3ms | |
| set_theory/cofinality.lean | |
| cumulative profiling times: | |
| compilation 0.621ms | |
| decl post-processing 10ms | |
| elaboration 82.7s | |
| elaboration: tactic compilation 1.09s | |
| elaboration: tactic execution 85.7s | |
| parsing 1.54s | |
| type checking 10.5ms | |
| set_theory/lists.lean | |
| cumulative profiling times: | |
| compilation 38.6ms | |
| decl post-processing 29.1ms | |
| elaboration 8.03s | |
| elaboration: tactic compilation 290ms | |
| elaboration: tactic execution 7.96s | |
| parsing 420ms | |
| type checking 7.25ms | |
| set_theory/ordinal.lean | |
| cumulative profiling times: | |
| compilation 56ms | |
| decl post-processing 170ms | |
| elaboration 19s | |
| elaboration: tactic compilation 2.48s | |
| elaboration: tactic execution 8.32s | |
| parsing 3.9s | |
| type checking 98.5ms | |
| set_theory/ordinal_notation.lean | |
| cumulative profiling times: | |
| compilation 61.5ms | |
| decl post-processing 80.4ms | |
| elaboration 60.6s | |
| elaboration: tactic compilation 907ms | |
| elaboration: tactic execution 52.9s | |
| parsing 2.81s | |
| type checking 22.1ms | |
| set_theory/zfc.lean | |
| cumulative profiling times: | |
| compilation 28.6ms | |
| decl post-processing 71.8ms | |
| elaboration 7.18s | |
| elaboration: tactic compilation 429ms | |
| elaboration: tactic execution 4.41s | |
| parsing 535ms | |
| type checking 23.7ms | |
| tactic/abel.lean | |
| cumulative profiling times: | |
| compilation 256ms | |
| decl post-processing 2.86ms | |
| elaboration 48.4s | |
| elaboration: tactic compilation 273ms | |
| elaboration: tactic execution 42.5s | |
| parsing 245ms | |
| type checking 33.4ms | |
| tactic/algebra.lean | |
| cumulative profiling times: | |
| compilation 7.16ms | |
| decl post-processing 0.177ms | |
| elaboration 42.5ms | |
| elaboration: tactic compilation 0.213ms | |
| elaboration: tactic execution 0ms | |
| parsing 0.64ms | |
| type checking 0.55ms | |
| tactic/alias.lean | |
| cumulative profiling times: | |
| compilation 50.5ms | |
| decl post-processing 0.234ms | |
| elaboration 216ms | |
| elaboration: tactic compilation 0.392ms | |
| elaboration: tactic execution 0ms | |
| parsing 4.06ms | |
| type checking 2.84ms | |
| tactic/auto_cases.lean | |
| cumulative profiling times: | |
| compilation 71.5ms | |
| decl post-processing 0.0125ms | |
| elaboration 95.1ms | |
| parsing 13ms | |
| type checking 2.46ms | |
| tactic/basic.lean | |
| cumulative profiling times: | |
| compilation 340ms | |
| decl post-processing 0.378ms | |
| elaboration 722ms | |
| elaboration: tactic compilation 4.09ms | |
| elaboration: tactic execution 0ms | |
| parsing 26.4ms | |
| type checking 16.7ms | |
| tactic/cache.lean | |
| cumulative profiling times: | |
| compilation 13.3ms | |
| decl post-processing 0.0275ms | |
| elaboration 30.2ms | |
| parsing 1.18ms | |
| type checking 4.4ms | |
| tactic/chain.lean | |
| cumulative profiling times: | |
| compilation 44.7ms | |
| decl post-processing 0.126ms | |
| elaboration 141ms | |
| parsing 6.48ms | |
| type checking 1.82ms | |
| tactic/converter/binders.lean | |
| cumulative profiling times: | |
| compilation 131ms | |
| decl post-processing 0.778ms | |
| elaboration 810ms | |
| elaboration: tactic compilation 20.4ms | |
| elaboration: tactic execution 434ms | |
| parsing 24.5ms | |
| type checking 6.72ms | |
| tactic/converter/interactive.lean | |
| cumulative profiling times: | |
| compilation 31.3ms | |
| decl post-processing 0.0471ms | |
| elaboration 91ms | |
| parsing 2.35ms | |
| type checking 2.13ms | |
| tactic/converter/old_conv.lean | |
| cumulative profiling times: | |
| compilation 190ms | |
| decl post-processing 0.258ms | |
| elaboration 413ms | |
| parsing 18.4ms | |
| type checking 10.8ms | |
| tactic/default.lean | |
| tactic/explode.lean | |
| cumulative profiling times: | |
| compilation 36.5ms | |
| decl post-processing 2.15ms | |
| elaboration 107ms | |
| parsing 4.1ms | |
| type checking 2.1ms | |
| tactic/ext.lean | |
| cumulative profiling times: | |
| compilation 33.4ms | |
| decl post-processing 3.29ms | |
| elaboration 355ms | |
| elaboration: tactic compilation 5.94ms | |
| elaboration: tactic execution 47ms | |
| parsing 28.2ms | |
| type checking 3.31ms | |
| tactic/find.lean | |
| cumulative profiling times: | |
| compilation 25.6ms | |
| decl post-processing 0.0644ms | |
| elaboration 132ms | |
| parsing 3.45ms | |
| type checking 1.39ms | |
| tactic/finish.lean | |
| cumulative profiling times: | |
| compilation 185ms | |
| decl post-processing 0.745ms | |
| elaboration 496ms | |
| parsing 15.8ms | |
| type checking 8.99ms | |
| tactic/generalize_proofs.lean | |
| cumulative profiling times: | |
| compilation 3.79ms | |
| decl post-processing 0.0119ms | |
| elaboration 89.4ms | |
| parsing 2.79ms | |
| type checking 0.22ms | |
| tactic/interactive.lean | |
| cumulative profiling times: | |
| compilation 345ms | |
| decl post-processing 0.126ms | |
| elaboration 753ms | |
| elaboration: tactic compilation 8.11ms | |
| elaboration: tactic execution 3ms | |
| parsing 55.5ms | |
| type checking 38.4ms | |
| tactic/linarith.lean | |
| cumulative profiling times: | |
| compilation 495ms | |
| decl post-processing 13.8ms | |
| elaboration 93.8s | |
| elaboration: tactic compilation 634ms | |
| elaboration: tactic execution 79.8s | |
| parsing 631ms | |
| type checking 70.8ms | |
| tactic/mk_iff_of_inductive_prop.lean | |
| cumulative profiling times: | |
| compilation 92.5ms | |
| decl post-processing 2.16ms | |
| elaboration 174ms | |
| parsing 6.52ms | |
| type checking 3.7ms | |
| tactic/norm_num.lean | |
| cumulative profiling times: | |
| compilation 936ms | |
| decl post-processing 0.566ms | |
| elaboration 6.77s | |
| elaboration: tactic compilation 157ms | |
| elaboration: tactic execution 3.74s | |
| parsing 192ms | |
| type checking 18.7ms | |
| tactic/pi_instances.lean | |
| cumulative profiling times: | |
| compilation 23.7ms | |
| decl post-processing 0.00991ms | |
| elaboration 68.4ms | |
| elaboration: tactic compilation 2.03ms | |
| elaboration: tactic execution 0ms | |
| parsing 1.35ms | |
| type checking 0.866ms | |
| tactic/rcases.lean | |
| cumulative profiling times: | |
| compilation 62ms | |
| decl post-processing 5.4ms | |
| elaboration 279ms | |
| elaboration: tactic compilation 8.4ms | |
| elaboration: tactic execution 4ms | |
| parsing 54.6ms | |
| type checking 3.75ms | |
| tactic/replacer.lean | |
| cumulative profiling times: | |
| compilation 32.9ms | |
| decl post-processing 0.0786ms | |
| elaboration 224ms | |
| elaboration: tactic compilation 0.229ms | |
| elaboration: tactic execution 0ms | |
| parsing 4.74ms | |
| type checking 1.53ms | |
| tactic/restate_axiom.lean | |
| cumulative profiling times: | |
| compilation 20.4ms | |
| decl post-processing 0.0538ms | |
| elaboration 54.9ms | |
| parsing 1.42ms | |
| type checking 1.15ms | |
| tactic/rewrite.lean | |
| cumulative profiling times: | |
| compilation 74.7ms | |
| decl post-processing 0.0792ms | |
| elaboration 336ms | |
| parsing 9.92ms | |
| type checking 4.31ms | |
| tactic/ring.lean | |
| cumulative profiling times: | |
| compilation 121ms | |
| decl post-processing 1.24ms | |
| elaboration 27.9s | |
| elaboration: tactic compilation 174ms | |
| elaboration: tactic execution 23.5s | |
| parsing 237ms | |
| type checking 15.6ms | |
| tactic/ring2.lean | |
| cumulative profiling times: | |
| compilation 106ms | |
| decl post-processing 25.2ms | |
| elaboration 14.3s | |
| elaboration: tactic compilation 239ms | |
| elaboration: tactic execution 11.5s | |
| parsing 669ms | |
| type checking 6.54ms | |
| tactic/scc.lean | |
| cumulative profiling times: | |
| compilation 75.1ms | |
| decl post-processing 0.084ms | |
| elaboration 281ms | |
| parsing 6.97ms | |
| type checking 3.38ms | |
| tactic/split_ifs.lean | |
| cumulative profiling times: | |
| compilation 18.8ms | |
| decl post-processing 0.031ms | |
| elaboration 151ms | |
| elaboration: tactic compilation 1.98ms | |
| elaboration: tactic execution 5ms | |
| parsing 12.1ms | |
| type checking 1.47ms | |
| tactic/squeeze.lean | |
| cumulative profiling times: | |
| compilation 83.5ms | |
| decl post-processing 0.0272ms | |
| elaboration 223ms | |
| parsing 9.31ms | |
| type checking 6.67ms | |
| tactic/subtype_instance.lean | |
| cumulative profiling times: | |
| compilation 60ms | |
| decl post-processing 0.927ms | |
| elaboration 80.2ms | |
| parsing 18.2ms | |
| type checking 1.88ms | |
| tactic/tauto.lean | |
| cumulative profiling times: | |
| compilation 78.6ms | |
| decl post-processing 0.0441ms | |
| elaboration 743ms | |
| parsing 21.9ms | |
| type checking 3.95ms | |
| tactic/tfae.lean | |
| cumulative profiling times: | |
| compilation 41.9ms | |
| decl post-processing 0.013ms | |
| elaboration 102ms | |
| parsing 5.11ms | |
| type checking 1.97ms | |
| tactic/tidy.lean | |
| cumulative profiling times: | |
| compilation 38.7ms | |
| decl post-processing 0.116ms | |
| elaboration 134ms | |
| elaboration: tactic compilation 2.29ms | |
| elaboration: tactic execution 0ms | |
| parsing 19.3ms | |
| type checking 1.95ms | |
| tactic/wlog.lean | |
| cumulative profiling times: | |
| compilation 168ms | |
| decl post-processing 0.0324ms | |
| elaboration 383ms | |
| parsing 9.06ms | |
| type checking 6.27ms | |
| tests/examples.lean | |
| cumulative profiling times: | |
| compilation 0.362ms | |
| decl post-processing 1ms | |
| elaboration 2.11s | |
| elaboration: tactic compilation 139ms | |
| elaboration: tactic execution 5.1s | |
| parsing 374ms | |
| type checking 0.711ms | |
| tests/finish1.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 1.05s | |
| elaboration: tactic execution 29.7s | |
| parsing 262ms | |
| tests/finish2.lean | |
| cumulative profiling times: | |
| compilation 0.0046ms | |
| decl post-processing 0.0256ms | |
| elaboration 426ms | |
| elaboration: tactic compilation 2.37s | |
| elaboration: tactic execution 59.7s | |
| parsing 527ms | |
| type checking 0.34ms | |
| tests/finish3.lean | |
| cumulative profiling times: | |
| compilation 0.0192ms | |
| decl post-processing 0.0645ms | |
| elaboration 1.51s | |
| elaboration: tactic compilation 988ms | |
| elaboration: tactic execution 33.4s | |
| parsing 246ms | |
| type checking 0.725ms | |
| tests/linarith.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 239ms | |
| elaboration: tactic execution 3.71s | |
| parsing 343ms | |
| tests/mk_iff_of_inductive.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 21.3ms | |
| elaboration: tactic execution 53ms | |
| tests/norm_num.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 371ms | |
| elaboration: tactic execution 8.56s | |
| parsing 204ms | |
| tests/replacer.lean | |
| cumulative profiling times: | |
| compilation 16.1ms | |
| decl post-processing 2.19ms | |
| elaboration 23ms | |
| elaboration: tactic compilation 34.6ms | |
| elaboration: tactic execution 1ms | |
| parsing 2.24ms | |
| type checking 0.987ms | |
| tests/restate_axiom.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 16.1ms | |
| elaboration: tactic execution 1ms | |
| parsing 8.14ms | |
| tests/ring.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 37.6ms | |
| elaboration: tactic execution 6.12s | |
| parsing 33.8ms | |
| tests/solve_by_elim.lean | |
| cumulative profiling times: | |
| compilation 3.03ms | |
| decl post-processing 0.551ms | |
| elaboration 5.87ms | |
| elaboration: tactic compilation 85.2ms | |
| elaboration: tactic execution 52ms | |
| parsing 90.5ms | |
| type checking 0.299ms | |
| tests/split_ifs.lean | |
| cumulative profiling times: | |
| elaboration: tactic compilation 39.1ms | |
| elaboration: tactic execution 151ms | |
| parsing 39.9ms | |
| tests/tactics.lean | |
| cumulative profiling times: | |
| compilation 3.55ms | |
| decl post-processing 11.4ms | |
| elaboration 918ms | |
| elaboration: tactic compilation 703ms | |
| elaboration: tactic execution 6.26s | |
| parsing 1.33s | |
| type checking 0.976ms | |
| tests/tidy.lean | |
| cumulative profiling times: | |
| compilation 3.97ms | |
| decl post-processing 1.47ms | |
| elaboration 514ms | |
| elaboration: tactic compilation 21.8ms | |
| elaboration: tactic execution 386ms | |
| parsing 22.3ms | |
| type checking 0.552ms |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment