fix: `print-paths` changed to `setup-file` in Lean v4.4.0 #55

utensil · 2023-12-11T13:03:13Z

Description

LeanInk/Analysis/LeanContext.lean relies on print-paths to initializeLakeContext, but in leanprover/lean4#2858 which is part of Lean v4.4.0 release, print-paths is changed to setup-file, with an extra parameter and changed JSON output.

This PR bumps LeanInk to use v4.4.0-rc1, replacing print-paths with setup-file and handles the parameter and output change accordingly.

There is probably no immediate need to merge this PR as doc-gen4 is using https://github.com/hargoniX/LeanInk/ which is 30+ commits behind leanprover/LeanInk and doesn't have this file, and I'm not aware of other major users.

More discussions on Zulip.

Notable Changes

Additional Notes

utensil · 2023-12-11T13:07:29Z

Locally it works fine (on Mac and my Ubuntu CI), but CI is red. Will look into that later.

utensil · 2023-12-12T06:02:13Z

There is no way I can pass the test for LeanInk. I tried the 2 approaches:

bumping Lean for LeanInk, so LeanInk itself and the target Lean program are both on v4.4.0, but tests in LeanInk are outdated by this leap of Lean toolchain, causing many failures that I don't intend to fix in this PR (or should I?). (this is now at my fix-print-path-bump branch)
don't bump Lean for LeanInk, so LeanInk itself is on old Lean (on this PR branch), it works fine for a target Lean program on v4.4.0 (locally), but tests in LeanInk are still failing because now the target Lean programs are the tests in LeanInk on the old Lean toolchain which doesn't play with setup-file.

utensil · 2023-12-12T06:55:20Z

I'll take approach 1, and fix the tests later. In the meanwhile, code in this PR or branch fix-print-path-nobump can lake build and works for target Lean code on Lean v4.4.0.

utensil · 2023-12-12T10:50:53Z

test/bench/Basic.lean.leanInk.expected

@@ -980,7 +980,7 @@
    "The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or\nnon-dependent hypotheses. It has many variants:\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged\n  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.\n  If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with\n  `f` are used. This provides a convenient way to unfold `f`.\n- `simp [*]` simplifies the main goal target using the lemmas tagged with the\n  attribute `[simp]` and all hypotheses.\n- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.\n- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged\n  with the attribute `[simp]`, but removes the ones named `idᵢ`.\n- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If\n  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis\n  `hᵢ` is introduced, but the old one remains in the local context.\n- `simp at *` simplifies all the hypotheses and the target.\n- `simp [*] at *` simplifies target and all (propositional) hypotheses using the\n  other hypotheses.\n",
    "_type": "token"},
   {"typeinfo":
-    {"type": "{α : Type ?u.3247} → [self : BEq α] → α → α → Bool",
+    {"type": "{α : Type ?u.3298} → [self : BEq α] → α → α → Bool",


De Bruijn index change across versions seems to be normal.

utensil · 2023-12-12T10:55:59Z

test/bench/Basic.lean.leanInk.expected

@@ -1939,7 +1939,7 @@
    "raw": "absurd",
    "link": null,
    "docstring":
-    "Anything follows from two contradictory hypotheses. Example:\n```\nexample (hp : p) (hnp : ¬p) : q := absurd hp hnp\n```\nFor more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)\n",
+    "Anything follows from two contradictory hypotheses. Example:\n```\nexample (hp : p) (hnp : ¬p) : q := absurd hp hnp\n```\nFor more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)\n",


This file is full of this url change. Here is the meaningful diff produced by

git diff 71b8365e08fb8b786cff628bbea38a2512370ca7 0227adbf7ee9b323efa0c47bbd00c8976b51e4a1 test/bench/Basic.lean.leanInk.expected|grep -E '^[-+] '|grep -v theorem_proving_in_lean4

- {"type": "{α : Type ?u.3247} → [self : BEq α] → α → α → Bool", + {"type": "{α : Type ?u.3298} → [self : BEq α] → α → α → Bool", - {"typeinfo": {"type": "m + n = k + m", "name": "h", "_type": "typeinfo"}, + {"typeinfo": {"type": "n + m = k + m", "name": "h", "_type": "typeinfo"}, - "conclusion": "0 = 0 + zero * k", + "conclusion": "0 = zero * m + zero * k", - [{"name": "", - "hypotheses": [], - "conclusion": "Goals accomplished! 🐙", + [{"name": "zero", + "hypotheses": + [{"type": "Nat", "names": ["m", "k"], "body": "", "_type": "hypothesis"}], + "conclusion": "0 = 0 + zero * k", - [{"name": "zero", - "hypotheses": - [{"type": "Nat", "names": ["m", "k"], "body": "", "_type": "hypothesis"}], - "conclusion": "0 = zero * m + zero * k", + [{"name": "", + "hypotheses": [], + "conclusion": "Goals accomplished! 🐙", - {"typeinfo": {"type": "n * m = k * m", "name": "h", "_type": "typeinfo"}, + {"typeinfo": {"type": "m * n = k * m", "name": "h", "_type": "typeinfo"}, - "raw": " => ", + "raw": " ", - {"messages": [], + {"messages": + [{"contents": + "Error: unsolved goals\ncase succ\nn : Nat\nih : 0 - n = 0\n⊢ pred 0 = 0", + "_type": "message"}], - [{"name": "", - "hypotheses": [], - "conclusion": "Goals accomplished! 🐙", + [{"name": "succ", + "hypotheses": + [{"type": "Nat", "names": ["n"], "body": "", "_type": "hypothesis"}, + {"type": "0 - n = 0", "names": ["ih"], "body": "", "_type": "hypothesis"}], + "conclusion": "0 - succ n = 0", + "_type": "goal"}], + "contents": + [{"typeinfo": null, + "semanticType": null, + "raw": "=> ", + "link": null, + "docstring": + "In induction alternative, which can have 1 or more cases on the left\nand `_`, `?_`, or a tactic sequence after the `=>`.\n", + "_type": "token"}], + "_type": "sentence"}, + {"messages": + [{"contents": + "Error: unsolved goals\ncase succ\nn : Nat\nih : 0 - n = 0\n⊢ pred 0 = 0", + "_type": "message"}], + "goals": + [{"name": "succ", + "hypotheses": + [{"type": "Nat", "names": ["n"], "body": "", "_type": "hypothesis"}, + {"type": "0 - n = 0", "names": ["ih"], "body": "", "_type": "hypothesis"}], + "conclusion": "pred 0 = 0",

utensil · 2023-12-12T10:58:03Z

test/dep/Main.lean.leanInk.expected

@@ -40,7 +40,7 @@
    "raw": "Unit",
    "link": null,
    "docstring":
-    "The unit type, the canonical type with one element, named `unit` or `()`.\nIn other words, it describes only a single value, which consists of said constructor applied\nto no arguments whatsoever.\nThe `Unit` type is similar to `void` in languages derived from C.\n\n`Unit` is actually defined as `PUnit.{0}` where `PUnit` is the universe\npolymorphic version. The `Unit` should be preferred over `PUnit` where possible to avoid\nunnecessary universe parameters.\n\nIn functional programming, `Unit` is the return type of things that \"return\nnothing\", since a type with one element conveys no additional information.\nWhen programming with monads, the type `m Unit` represents an action that has\nsome side effects but does not return a value, while `m α` would be an action\nthat has side effects and returns a value of type `α`.\n",
+    "The unit type, the canonical type with one element, named `unit` or `()`.\nIn other words, it describes only a single value, which consists of said constructor applied\nto no arguments whatsoever.\nThe `Unit` type is similar to `void` in languages derived from C.\n\n`Unit` is actually defined as `PUnit.{1}` where `PUnit` is the universe\npolymorphic version. The `Unit` should be preferred over `PUnit` where possible to avoid\nunnecessary universe parameters.\n\nIn functional programming, `Unit` is the return type of things that \"return\nnothing\", since a type with one element conveys no additional information.\nWhen programming with monads, the type `m Unit` represents an action that has\nsome side effects but does not return a value, while `m α` would be an action\nthat has side effects and returns a value of type `α`.\n",


PUnit.{0} changed to PUnit.{1}.

utensil · 2023-12-12T10:58:49Z

test/playground/infoTree.lean.leanInk.expected

@@ -103,7 +103,7 @@
    "link": null,
    "docstring": null,
    "_type": "token"},
-   {"typeinfo": {"type": "A × A → B", "name": "B", "_type": "typeinfo"},
+   {"typeinfo": {"type": "Type", "name": "B", "_type": "typeinfo"},


No idea why this is A × A → B before. B is

structure B where pair : A × A

Obviously B is just a Type.

utensil · 2023-12-12T11:22:50Z

test/bench/Basic.lean.leanInk.expected

+ {"messages":
+  [{"contents":
+    "Error: unsolved goals\ncase succ\nn : Nat\nih : 0 - n = 0\n⊢ pred 0 = 0",
+    "_type": "message"}],


This proof is no longer proven, will investigate. The same applies to all Error: unsolved goals.

@[simp] protected theorem zero_sub (n : Nat) : 0 - n = 0 := by induction n with | zero => rfl | succ n ih => simp [ih, Nat.sub_succ]

This proof failed to use the protected simp lemma pred_zero in the same namespace, is this expected?

utensil · 2023-12-12T11:27:20Z

LeanInk/Analysis/LeanContext.lean

@@ -51,11 +56,13 @@ def initializeLakeContext (lakeFile : FilePath) (header : Syntax) : AnalysisM Un
    | 0 => do
      let stdout := stdout.split (· == '\n') |>.getLast!
      match Json.parse stdout with
-      | Except.error _ => throw <| IO.userError s!"Failed to parse lake output: {stdout}"
+      | Except.error msg => throw <| IO.userError s!"Failed to parse lake output: {stdout}\nerror: {msg}"


The msg is helpful for debugging.

femtomc · 2023-12-28T02:54:33Z

Note that this branch (and its fixes) also fixes my issue #56.

utensil added 2 commits December 12, 2023 13:51

fix: print-paths changed to setup-file

12b983d

fix: output of setup-file has changed

c65e5f2

utensil force-pushed the fix-print-path branch from f056779 to c65e5f2 Compare December 12, 2023 05:54

utensil added 3 commits December 12, 2023 18:07

chore: bump to v4.4.0-rc1

5fe974d

chore: bump tests to v4.4.0-rc1 and lake update

71b8365

chore: update tests by lake script run capture

0227adb

utensil commented Dec 12, 2023

View reviewed changes

mhuisi approved these changes Jan 10, 2024

View reviewed changes

mhuisi merged commit 58755bf into leanprover:main Jan 10, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix: `print-paths` changed to `setup-file` in Lean v4.4.0 #55

fix: `print-paths` changed to `setup-file` in Lean v4.4.0 #55

utensil commented Dec 11, 2023 •

edited

Loading

utensil commented Dec 11, 2023 •

edited

Loading

utensil commented Dec 12, 2023 •

edited

Loading

utensil commented Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023

utensil Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023

femtomc commented Dec 28, 2023

fix: print-paths changed to setup-file in Lean v4.4.0 #55

fix: print-paths changed to setup-file in Lean v4.4.0 #55

Conversation

utensil commented Dec 11, 2023 • edited Loading

Description

Notable Changes

Additional Notes

utensil commented Dec 11, 2023 • edited Loading

utensil commented Dec 12, 2023 • edited Loading

utensil commented Dec 12, 2023 • edited Loading

utensil Dec 12, 2023

Choose a reason for hiding this comment

utensil Dec 12, 2023 • edited Loading

Choose a reason for hiding this comment

utensil Dec 12, 2023 • edited Loading

Choose a reason for hiding this comment

utensil Dec 12, 2023 • edited Loading

Choose a reason for hiding this comment

utensil Dec 12, 2023 • edited Loading

Choose a reason for hiding this comment

utensil Dec 12, 2023 • edited Loading

Choose a reason for hiding this comment

utensil Dec 12, 2023

Choose a reason for hiding this comment

femtomc commented Dec 28, 2023

fix: `print-paths` changed to `setup-file` in Lean v4.4.0 #55

fix: `print-paths` changed to `setup-file` in Lean v4.4.0 #55

utensil commented Dec 11, 2023 •

edited

Loading

utensil commented Dec 11, 2023 •

edited

Loading

utensil commented Dec 12, 2023 •

edited

Loading

utensil commented Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023 •

edited

Loading

utensil Dec 12, 2023 •

edited

Loading