chore: bump to v4.28.0-rc1 (#718)

Author: david-christiansen

.gitignore

@@ -17,4 +17,6 @@ profile.json.gz
 /src/tests/integration/**/*.out
 /src/tests/integration/**/*.pdf
 /src/tests/integration/**/*.toc
-
+multi.json
+single.json
+*.html

index.html

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
+   "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lake-manifest.json

@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0-rc1

lean-toolchain

@@ -209,7 +209,7 @@ def DeclType.ofName (c : Name)
               parentProjFns.mapIdxM fun i parentProj => do
                 let proj := mkApp (mkAppN (.const parentProj us) params) s
                 let type ← inferType proj >>= instantiateMVars
-                let projType ← withOptions (·.setInt `format.width 40 |>.setBool `pp.tagAppFns true) <| Widget.ppExprTagged type
+                let projType ← withOptions (·.set `format.width (40 : Int) |>.setBool `pp.tagAppFns true) <| Widget.ppExprTagged type
                 if let .const parentName _  := type.getAppFn then
                   pure ⟨parentProj, parentName, ← renderTagged none projType hlCtx, i⟩
                 else
@@ -222,8 +222,8 @@ def DeclType.ofName (c : Name)
               allFields.filterMapM fun fieldName => do
                 let proj ← mkProjection s fieldName
                 let type ← inferType proj >>= instantiateMVars
-                let type' ← withOptions (·.setInt `format.width 40 |>.setBool `pp.tagAppFns true) <| (Widget.ppExprTagged type)
-                let projType ← withOptions (·.setInt `format.width 40 |>.setBool `pp.tagAppFns true) <| ppExpr type
+                let type' ← withOptions (·.set `format.width (40 : Int) |>.setBool `pp.tagAppFns true) <| (Widget.ppExprTagged type)
+                let projType ← withOptions (·.set `format.width (40 : Int) |>.setBool `pp.tagAppFns true) <| ppExpr type
                 let fieldFrom? := findField? env c fieldName
                 let fieldPath? := fieldFrom? >>= (getStructurePathToBaseStructure? env · c)
                 let fieldFrom ← fieldPath?.getD [] |>.mapM (DocName.ofName (showUniverses := false))