Sebastian Ullrich
1dc3626ff7
perf: remove most remaining async blockers in Init.Data.List.Sublist ( #7500 )
2025-03-15 15:26:06 +00:00
Sebastian Ullrich
6f445a1c05
chore: Task.get block profiling ( #7016 )
...
* `--profile` now reports `blocking` time spent in `Task.get` inside
other profiling categories
* environment variable `LEAN_TRACE_TASK_GET_BLOCKED` when set makes
`lean` dump stack traces of `Task.get` blocks
2025-02-10 10:56:49 +00:00
Leonardo de Moura
b8b6b219c3
chore: move trace.cpp to kernel ( #4014 )
...
Motivation: trace kernel `is_def_eq`
2024-04-28 17:24:48 +00:00
Sebastian Ullrich
b076d488e3
feat: show typeclass and tactic names in profile output
2023-03-27 17:47:52 +02:00
Sebastian Ullrich
c826168cfa
fix: atomic --profile output for xargs -P
2023-02-11 17:41:07 +01:00
Sebastian Ullrich
b13d3e6ca5
fix: dllexport functions not already annotated in header
2021-09-20 18:41:46 +02:00
Sebastian Ullrich
389a274d45
fix: show exclusive profiling times everywhere
2021-06-17 11:25:58 +02:00
Leonardo de Moura
a58ff18a5b
refactor: pos at time_task::time_task was a dead field
2021-01-30 11:10:18 -08:00
Sebastian Ullrich
a6c319a25c
chore: remove message_builder from time_task
2021-01-12 09:51:14 -08:00
Sebastian Ullrich
0720334450
feat: make profileit actually usable
2020-10-23 18:34:47 +02:00
Sebastian Ullrich
c32f843efc
fix: profiling from the new frontend; use trace out for the time being
2020-10-22 16:00:03 +02:00
Sebastian Ullrich
f2a161e5a9
feat(library/init/lean/util): Lean API for profiler
2019-03-06 10:37:38 +01:00
Sebastian Ullrich
c9bebb7411
feat(library/time_task): do not report inclusive times
2018-11-05 17:06:32 +01:00
Leonardo de Moura
3f04d041f6
chore(library/time_task): style
2018-02-19 10:30:49 -08:00
Sebastian Ullrich
f247363305
feat(library/time_task): print cumulative times on --profile
2018-02-19 09:13:24 -08:00
