From f0347ee719abfbbe27159ebf896877411966f5bf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 12 Jun 2025 10:29:42 +0200 Subject: [PATCH] chore: `lean --stats` gives number of imported bytes (#8725) Thanks to `mmap`, startup time is not necessarily related to this figure, but it can be used as a rough measure for that and how much data the module depends on, i.e. the rebuild chance. Also adds new cumulative benchmarks for this metric as well as the number of imported constants and env ext entries. --- src/Lean/Environment.lean | 5 +++++ src/runtime/compact.cpp | 5 +++++ src/runtime/compact.h | 2 ++ tests/bench/accumulate_profile.py | 3 ++- tests/bench/speedcenter.exec.velcom.yaml | 2 +- 5 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 7c48ea8334..74549680bb 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -103,6 +103,10 @@ def CompactedRegion := USize @[extern "lean_compacted_region_is_memory_mapped"] opaque CompactedRegion.isMemoryMapped : CompactedRegion → Bool +/-- Size in bytes. -/ +@[extern "lean_compacted_region_size"] +opaque CompactedRegion.size : CompactedRegion → USize + /-- Free a compacted region and its contents. No live references to the contents may exist at the time of invocation. -/ @[extern "lean_compacted_region_free"] unsafe opaque CompactedRegion.free : CompactedRegion → IO Unit @@ -2178,6 +2182,7 @@ def displayStats (env : Environment) : IO Unit := do IO.println ("direct imports: " ++ toString env.header.imports); IO.println ("number of imported modules: " ++ toString env.header.regions.size); IO.println ("number of memory-mapped modules: " ++ toString (env.header.regions.filter (·.isMemoryMapped) |>.size)); + IO.println ("number of imported bytes: " ++ toString (env.header.regions.map (·.size) |>.sum)); IO.println ("number of imported consts: " ++ toString env.constants.map₁.size); IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets); IO.println ("trust level: " ++ toString env.header.trustLevel); diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp index 786eca5d06..faf3965ecb 100644 --- a/src/runtime/compact.cpp +++ b/src/runtime/compact.cpp @@ -379,6 +379,7 @@ void object_compactor::operator()(object * o) { } compacted_region::compacted_region(size_t sz, void * data, void * base_addr, bool is_mmap, std::function free_data): + m_size(sz), m_base_addr(base_addr), m_is_mmap(is_mmap), m_free_data(free_data), @@ -502,6 +503,10 @@ extern "C" LEAN_EXPORT uint8 lean_compacted_region_is_memory_mapped(usize region return reinterpret_cast(region)->is_memory_mapped(); } +extern "C" LEAN_EXPORT usize lean_compacted_region_size(usize region) { + return reinterpret_cast(region)->size(); +} + extern "C" LEAN_EXPORT obj_res lean_compacted_region_free(usize region, object *) { delete reinterpret_cast(region); return lean_io_result_mk_ok(lean_box(0)); diff --git a/src/runtime/compact.h b/src/runtime/compact.h index 911e2670a2..4284d3b48e 100644 --- a/src/runtime/compact.h +++ b/src/runtime/compact.h @@ -57,6 +57,7 @@ public: }; class LEAN_EXPORT compacted_region { + size_t m_size; // see `object_compactor::m_base_addr` void * m_base_addr; bool m_is_mmap; @@ -88,5 +89,6 @@ public: compacted_region operator=(compacted_region &&) = delete; object * read(); bool is_memory_mapped() const { return m_is_mmap; } + size_t size() const { return m_size; } }; } diff --git a/tests/bench/accumulate_profile.py b/tests/bench/accumulate_profile.py index a018f83d0f..1a21ff947d 100755 --- a/tests/bench/accumulate_profile.py +++ b/tests/bench/accumulate_profile.py @@ -6,7 +6,8 @@ import sys cats = collections.defaultdict(lambda: 0) for line in sys.stdin: - if m := re.match("(.+?) ([\d.]+)(m?)s", line): + if m := re.match(r"(.+?) ([\d.]+)(m?)s", line) or \ + re.match(r"\s*(number of imported bytes|number of imported consts|number of imported entries):\s+(\d+)()", line): cats[m[1].strip()] += float(m[2]) * (1e-3 if m[3] else 1) sys.stderr.write(line) diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 11db80fa7b..3d5e3b4780 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -18,7 +18,7 @@ run_config: <<: *time cmd: | - bash -c 'set -eo pipefail; touch ../../src/Init/Prelude.lean; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=9999" -C ${BUILD:-../../build/release}/stage2 --output-sync -j$(nproc) 2>&1 | ./accumulate_profile.py' + bash -c 'set -eo pipefail; touch ../../src/Init/Prelude.lean; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=99999 --stats" -C ${BUILD:-../../build/release}/stage2 --output-sync -j$(nproc) 2>&1 | ./accumulate_profile.py' max_runs: 2 parse_output: true # initialize stage2 cmake + warmup