From fbdcaab009e099c14e4f864fb0615c93dd45cfbf Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 28 Jul 2021 13:08:46 +0200
Subject: [PATCH] feat: show number of mmap-ed modules in --stats

---
 src/Lean/Environment.lean  | 9 ++++++---
 src/include/lean/compact.h | 1 +
 src/runtime/compact.cpp    | 4 ++++
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 03acb0d358..4736872daf 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -37,8 +37,11 @@ instance : ToString Import := ⟨fun imp => toString imp.module ++ if imp.runtim
   files are compacted regions. -/
 def CompactedRegion := USize
 
+@[extern "lean_compacted_region_is_memory_mapped"]
+constant CompactedRegion.isMemoryMapped : CompactedRegion → Bool
+
 /-- Free a compacted region and its contents. No live references to the contents may exist at the time of invocation. -/
-@[extern 2 "lean_compacted_region_free"]
+@[extern "lean_compacted_region_free"]
 unsafe constant CompactedRegion.free : CompactedRegion → IO Unit
 
 /- Environment fields that are not used often. -/
@@ -701,9 +704,9 @@ def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
 @[export lean_display_stats]
 def displayStats (env : Environment) : IO Unit := do
   let pExtDescrs ← persistentEnvExtensionsRef.get
-  let numModules := ((pExtDescrs.get! 0).toEnvExtension.getState env).importedEntries.size;
   IO.println ("direct imports:                        " ++ toString env.header.imports);
-  IO.println ("number of imported modules:            " ++ toString numModules);
+  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 consts:                      " ++ toString env.constants.size);
   IO.println ("number of imported consts:             " ++ toString env.constants.stageSizes.1);
   IO.println ("number of local consts:                " ++ toString env.constants.stageSizes.2);
diff --git a/src/include/lean/compact.h b/src/include/lean/compact.h
index 616495912d..b866956f1c 100644
--- a/src/include/lean/compact.h
+++ b/src/include/lean/compact.h
@@ -87,5 +87,6 @@ public:
     compacted_region operator=(compacted_region const &) = delete;
     compacted_region operator=(compacted_region &&) = delete;
     object * read();
+    bool is_memory_mapped() const { return m_mmap_addr; }
 };
 }
diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp
index 9976ebec99..01917e4723 100644
--- a/src/runtime/compact.cpp
+++ b/src/runtime/compact.cpp
@@ -463,6 +463,10 @@ object * compacted_region::read() {
     return root;
 }
 
+extern "C" uint8 lean_compacted_region_is_memory_mapped(usize region) {
+    return reinterpret_cast<compacted_region *>(region)->is_memory_mapped();
+}
+
 extern "C" obj_res lean_compacted_region_free(usize region, object *) {
     delete reinterpret_cast<compacted_region *>(region);
     return lean_io_result_mk_ok(lean_box(0));