From 9f53781ffe548fbd0ef6e4c61e725a53233b17e2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 12 May 2023 01:08:36 -0700
Subject: [PATCH] Add working catalog code and example

---
 Main.lean |  7 +++++--
 README.md | 17 ++++++++++++-----
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/Main.lean b/Main.lean
index 76523bf..53db5b7 100644
--- a/Main.lean
+++ b/Main.lean
@@ -45,7 +45,9 @@ def catalog (args: Catalog): Subroutine CatalogResult := do
   let state ← get
   match state.environments.get? args.id with
   | .some env =>
-    let names := env.constants.toList.map (λ ⟨x, _⟩ => toString x)
+    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)
     return { theorems := names }
   | .none => throw s!"Invalid environment id {args.id}"
 
@@ -96,5 +98,6 @@ unsafe def loop : T IO Unit := do
   | .ok obj => IO.println <| toString <| obj
   loop
 
-unsafe def main : IO Unit :=
+unsafe def main : IO Unit := do
+  Lean.initSearchPath (← Lean.findSysroot)
   StateT.run' loop ⟨#[]⟩
diff --git a/README.md b/README.md
index f890444..c40c470 100644
--- a/README.md
+++ b/README.md
@@ -8,14 +8,21 @@ Install `elan` and `lean4`. Then, execute
 ``` sh
 lake build
 ```
+In order to use `mathlib`, its binary must also be built
+
+``` sh
+lake build std
+lake build mathlib
+```
 
 ## Usage
 
-Before usage, put the packages that you wish the REPL to use into a directory
-and build them. Put this directory into the variable `$LEAN_PATH`. Then
-``` 
-$ build/bin/Pantograph
-{"cmd": "create", "payload": {"imports": ["Mathlib.Analysis.Seminorm"]}}
+The binary must be run inside a `lake env` environment.
 ```
+$ 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.