From 2ec4efde55169272a45dc05d306d5f8b24efff1a Mon Sep 17 00:00:00 2001
From: Leni Ven <leniv@stanford.edu>
Date: Sun, 14 May 2023 15:22:41 -0700
Subject: [PATCH] Add stack size troubleshooting

---
 Main.lean               |  4 +++-
 Pantograph/Symbols.lean | 17 +++++++++++++++++
 README.md               |  5 +++++
 3 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/Main.lean b/Main.lean
index f8ad1e1..7c159a3 100644
--- a/Main.lean
+++ b/Main.lean
@@ -52,7 +52,9 @@ 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 es.length > 3000 ∨ is_symbol_unsafe_or_internal name info then es else (toString name)::es)
+      match to_filtered_symbol name info with
+      | .some x => x::es
+      | .none => es)
     return { theorems := names }
   | .none => throw s!"Invalid environment id {args.id}"
 
diff --git a/Pantograph/Symbols.lean b/Pantograph/Symbols.lean
index 824d8f1..97dafc7 100644
--- a/Pantograph/Symbols.lean
+++ b/Pantograph/Symbols.lean
@@ -15,4 +15,21 @@ def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool
   | .num _ _ => true
   nameDeduce ∨ stemDeduce ∨ info.isUnsafe
 
+def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+  let pref := match info with
+  | .axiomInfo  _ => "axiom"
+  | .defnInfo   _ => "defn"
+  | .thmInfo    _ => "thm"
+  | .opaqueInfo _ => "opaque"
+  | .quotInfo   _ => "quot"
+  | .inductInfo _ => "induct"
+  | .ctorInfo   _ => "ctor"
+  | .recInfo    _ => "rec"
+  s!"{pref}|{toString n}"
+
+def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
+  if is_symbol_unsafe_or_internal n info
+  then Option.none
+  else Option.some <| to_compact_symbol_name n info
+
 end Pantograph
diff --git a/README.md b/README.md
index ccdf941..2cee1a0 100644
--- a/README.md
+++ b/README.md
@@ -35,4 +35,9 @@ $ lake env build/bin/Pantograph
 ```
 
 
+## Troubleshooting
 
+If lean encounters stack overflow problems when printing catalog, execute this before running lean:
+```sh
+ulimit -s unlimited
+```