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?

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

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
+      let projectorName := getProjFnForField? env typeName fieldName |>.get!
-      assert! !inner.isProj
+      let e := Expr.app (.const  projectorName []) inner
-      self inner
+      self e
   -- Elides all unhygenic names
   binder_info_to_ast : Lean.BinderInfo → String
     | .default => ""

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"}