From 3cb0795bb626f088fe776d09f327d830140784c8 Mon Sep 17 00:00:00 2001
From: Leni Ven <leniv@stanford.edu>
Date: Fri, 12 May 2023 16:12:21 -0700
Subject: [PATCH] Add unsafe filtering in catalog

---
 Main.lean                | 12 +++++++++---
 Pantograph.lean          |  2 ++
 Pantograph/Commands.lean |  2 ++
 Pantograph/Symbols.lean  | 18 ++++++++++++++++++
 README.md                | 12 +++++++++++-
 lakefile.lean            |  5 ++---
 6 files changed, 44 insertions(+), 7 deletions(-)
 create mode 100644 Pantograph.lean
 create mode 100644 Pantograph/Symbols.lean

diff --git a/Main.lean b/Main.lean
index 53db5b7..f8ad1e1 100644
--- a/Main.lean
+++ b/Main.lean
@@ -2,6 +2,7 @@ import Lean.Data.Json
 import Lean.Environment
 
 import Pantograph.Commands
+import Pantograph.Symbols
 
 namespace Pantograph
 
@@ -35,7 +36,12 @@ def create (args: Create): Subroutine CreateResult := do
     (opts := {})
     (trustLevel := 1)
   modify fun s => { environments := s.environments.push env }
-  return { id := id }
+  let num_filtered_symbols := env.constants.fold (init := 0) (λ acc name info =>
+    acc + if is_symbol_unsafe_or_internal name info then 0 else 1)
+  return {
+    id := id,
+    symbols := env.constants.size,
+    filtered_symbols := num_filtered_symbols }
   where strTransform (s: String): Lean.Import :=
       let li := s.split (λ c => c == '.')
       let name := li.foldl (λ pre segment => Lean.Name.str pre segment) Lean.Name.anonymous
@@ -46,8 +52,7 @@ def catalog (args: Catalog): Subroutine CatalogResult := do
   match state.environments.get? args.id with
   | .some env =>
     let names := env.constants.fold (init := []) (λ es name info =>
-      if info.isUnsafe ∨ es.length > 500 then es else (toString name)::es)
-    --let names := env.constants.toList.map (λ ⟨x, _⟩ => toString x)
+      if es.length > 3000 ∨ is_symbol_unsafe_or_internal name info then es else (toString name)::es)
     return { theorems := names }
   | .none => throw s!"Invalid environment id {args.id}"
 
@@ -99,5 +104,6 @@ unsafe def loop : T IO Unit := do
   loop
 
 unsafe def main : IO Unit := do
+  Lean.enableInitializersExecution
   Lean.initSearchPath (← Lean.findSysroot)
   StateT.run' loop ⟨#[]⟩
diff --git a/Pantograph.lean b/Pantograph.lean
new file mode 100644
index 0000000..cd13b6f
--- /dev/null
+++ b/Pantograph.lean
@@ -0,0 +1,2 @@
+import Pantograph.Commands
+import Pantograph.Symbols
diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean
index 14059d7..675a2cf 100644
--- a/Pantograph/Commands.lean
+++ b/Pantograph/Commands.lean
@@ -12,6 +12,8 @@ structure Catalog where
 
 structure CreateResult where
   id: Nat
+  symbols: Nat
+  filtered_symbols: Nat
   deriving Lean.ToJson
 structure CatalogResult where
   theorems: List String
diff --git a/Pantograph/Symbols.lean b/Pantograph/Symbols.lean
new file mode 100644
index 0000000..824d8f1
--- /dev/null
+++ b/Pantograph/Symbols.lean
@@ -0,0 +1,18 @@
+/-
+ - Manages the visibility status of symbols
+ -/
+import Lean.Declaration
+
+namespace Pantograph
+
+def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
+  let nameDeduce: Bool := match n.getRoot with
+  | .str _ name => name.startsWith "_" ∨ name == "Lean"
+  | _ => true
+  let stemDeduce: Bool := match n with
+  | .anonymous => true
+  | .str _ name => name.startsWith "_"
+  | .num _ _ => true
+  nameDeduce ∨ stemDeduce ∨ info.isUnsafe
+
+end Pantograph
diff --git a/README.md b/README.md
index c40c470..ccdf941 100644
--- a/README.md
+++ b/README.md
@@ -11,6 +11,8 @@ lake build
 In order to use `mathlib`, its binary must also be built
 
 ``` sh
+lake build Qq
+lake build aesop
 lake build std
 lake build mathlib
 ```
@@ -18,11 +20,19 @@ lake build mathlib
 ## Usage
 
 The binary must be run inside a `lake env` environment.
+
+Example: (~5k symbols)
+```
+$ lake env build/bin/Pantograph
+{"cmd": "create", "payload": {"imports": ["Init"]}}
+{"cmd": "catalog", "payload": {"id": 0}}
+```
+Example with `mathlib` (~90k symbols)
 ```
 $ lake env build/bin/Pantograph
 {"cmd": "create", "payload": {"imports": ["Mathlib.Analysis.Seminorm"]}}
 {"cmd": "catalog", "payload": {"id": 0}}
 ```
-There is temporarily a limit of 500 symbols to prevent stack overflow.
+
 
 
diff --git a/lakefile.lean b/lakefile.lean
index f5d3fc2..d3acec1 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,9 +2,7 @@ import Lake
 open Lake DSL
 
 
-package pantograph {
-  -- add package configuration options here
-}
+package pantograph
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @  "8e5a00a8afc8913c0584cb85f37951995275fd87"
@@ -16,5 +14,6 @@ lean_lib Pantograph {
 @[default_target]
 lean_exe pantograph {
   root := `Main
+  -- Somehow solves the native symbol not found problem
   supportInterpreter := true
 }