From ccf5a036478aacd14ddd3595d80a89ebed1b58e2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 5 Dec 2023 22:45:59 -0800 Subject: [PATCH] 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"}