From ccf5a036478aacd14ddd3595d80a89ebed1b58e2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 5 Dec 2023 22:45:59 -0800
Subject: [PATCH 1/2] fix: Printing projection leads to crash

---
 Pantograph/Protocol.lean | 2 +-
 Pantograph/Serial.lean   | 6 +++---
 lake-manifest.json       | 5 +++--
 3 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 582ee1d..a88a54a 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -119,7 +119,7 @@ structure LibInspect where
 structure LibInspectResult where
   type: Expression
   value?: Option Expression := .none
-  module?: Option String
+  module?: Option String    := .none
   -- If the name is private, displays the public facing name
   publicName?: Option String := .none
   typeDependency?: Option (Array String) := .none
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 959cc0b..42fc4e2 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -145,9 +145,9 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
     | .proj typeName idx inner => do
       let env ← getEnv
       let fieldName := getStructureFields env typeName |>.get! idx
-      let inner ← Meta.mkProjection inner fieldName
-      assert! !inner.isProj
-      self inner
+      let projectorName := getProjFnForField? env typeName fieldName |>.get!
+      let e := Expr.app (.const  projectorName []) inner
+      self e
   -- Elides all unhygenic names
   binder_info_to_ast : Lean.BinderInfo → String
     | .default => ""
diff --git a/lake-manifest.json b/lake-manifest.json
index 5a13649..6c2efa0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,4 +1,4 @@
-{"version": 5,
+{"version": 6,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
@@ -8,4 +8,5 @@
     "opts": {},
     "name": "LSpec",
     "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-    "inherited": false}}]}
+    "inherited": false}}],
+ "name": "pantograph"}

From 2dc7657e2a225564dba5887b3b82bf046c58c876 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 6 Dec 2023 15:05:04 -0800
Subject: [PATCH 2/2] doc: getUsedConstants bug about projections

---
 Pantograph.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Pantograph.lean b/Pantograph.lean
index 958e43c..a66db35 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -86,6 +86,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         type := ← serialize_expression state.options info.type,
         value? := ← value?.mapM (λ v => serialize_expression state.options v),
         publicName? := Lean.privateToUserName? name |>.map (·.toString),
+        -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
         typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
         valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
         module? := module?