Using the Repl from another project (again) v4.9.0

Stream: general

[Riyaz Ahuja]

Continued from previous topic. Prev topic was resolved for v4.8.0 but seems to have broke again in v4.9.0.

With the new 4.9.0 release of the repl, the same old issue is coming up again despite both the repl and the project being on v4.9.0 (the fix for the previous question). The same MWE as before is causing the same issue, but the versions are the same, and I'm running from the directory with the lakefile as suggested before. Any ideas on how to fix this?

[Kim Morrison]

Note that repl master is now on v4.10.0-rc1.

[Kim Morrison]

Can you tell me how to repro what you're seeing? (i.e. exactly what do I type!)

[Riyaz Ahuja]

Yep I saw, Its just that my project that uses the repl is currently on v4.9.0 just for consistency with all its other dependencies. I'll port to v4.10.0 whenever it is released and the project has matured a bit.

As for how to reproduce, the same MWE from the linked previous thread causes the same error. For reference, here it is:

As a MWE, I made a fresh clone of the github above to Desktop/lean-repl, and ran the lake exe repl to initially build everything and then echo '{"path": "test/file.lean", "allTactics": true}' | lake exe repl as per the ReadMe. I get the expected output, completely identical to test/file.expected.out.

Then I made an empty folder Desktop/test and used the VSCode widget (∀) to make a new lean 4 project with mathlib called Test. I then go to my project folder Desktop/test/Test and with the default Test/Basic.lean, I copied over the file.in and file.lean from the REPL's source code. Note that the infoview works perfectly fine and running lake build returned success. Then, just as the readme says, i ran from this directory: lake env /Users/ahuja/Desktop/lean-repl/.lake/build/bin/repl < Test/file.in and got the following:

{"messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 15},
   "endPos": {"line": 1, "column": 17},
   "data": "unknown constant 'OfNat'"},
  {"severity": "error",
   "pos": {"line": 1, "column": 15},
   "endPos": {"line": 1, "column": 17},
   "data": "unknown constant 'sorryAx'"},
  {"severity": "error",
   "pos": {"line": 1, "column": 4},
   "endPos": {"line": 1, "column": 5},
   "data": "unknown constant 'sorryAx'"},
  {"severity": "error",
   "pos": {"line": 3, "column": 9},
   "endPos": {"line": 3, "column": 10},
   "data": "unknown constant 'OfNat'"},
  {"severity": "error",
   "pos": {"line": 3, "column": 9},
   "endPos": {"line": 3, "column": 10},
   "data": "unknown constant 'sorryAx'"},
  {"severity": "error",
   "pos": {"line": 5, "column": 13},
   "endPos": {"line": 5, "column": 15},
   "data": "unexpected token '+'; expected ':=', 'where' or '|'"}],
 "env": 0}

In comparison to when run as mentioned before from the repl's directory:

{"tactics":
 [{"tactic": "exact rfl",
   "proofState": 0,
   "pos": {"line": 5, "column": 29},
   "goals": "⊢ f + g = 39",
   "endPos": {"line": 5, "column": 38}}],
 "env": 0}

For reference, here's the file.lean that is copied in Desktop/lean-repl and Desktop/test/Test/Test:

def f : Nat := 37

def g := 2

theorem h : f + g = 39 := by exact rfl

I made sure that Test/lakefile.lean has the requires statement for mathlib, and still getting this issue. Any help would be super appreciated.

[Riyaz Ahuja]

Note that I just tested on v4.10.0-rc1 and the same error came up

[Kim Morrison]

Sorry, I don't have much time to look at this right now. Could you give me a super easy set of instructions to reproduce it, e.g. by preparing a repo in exactly the bad state, so I just have two or three explicit commands to type?

[Utensil Song]

I can confirm that running repl on v4.10.0-rc1 without a elan default leanprover/lean4:v4.10.0-rc1 will fail on almost all lean4_jupyter test cases (similar errors to yours, inside or outside a project).

@Riyaz Ahuja You may use elan default leanprover/lean4:v4.10.0-rc1 as a workaround for now. Sorry, I can't investigate this further at the moment.

[Malvin Gattinger]

I don't have a solution for the newer problem, but can confirm that this note here by Utensil helped me a lot :thank_you:
Utensil Song said:

This error occurs if your project is on a newer toolchain than repl. It's on 4.8.0 rc1, and yours is likely on 4.8.0 rc2.

To be precise, I had the inverse problem: my project is on an older toolchain than repl.

It would have helped me to read more about this before and to see an example, so I will leave some of my notes here. The example commands only need Mathlib, what myproject is does not matter.

With lean --stdin we can do this:

~/myproject $ cat commands.txt
import Mathlib.Logic.Lemmas
#print axioms iff_assoc
#print axioms Prop.forall
~/myproject $ lake env lean --stdin  < commands.txt
'iff_assoc' depends on axioms: [Classical.choice, propext, Quot.sound]
'Prop.forall' depends on axioms: [Classical.choice, propext, Quot.sound]

But trying to do the same thing with repl I got this error:

~/myproject $ cat commands.json
{ "cmd" : "import Mathlib.Logic.Lemmas" }

{ "cmd" : "#print axioms iff_assoc", "env" : 0 }
~/myproject $ lake env ../lean4-repl/.lake/build/bin/repl < commands.json
{"env": 0}

{"messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 14},
   "endPos": {"line": 1, "column": 23},
   "data": "unknown constant 'iff_assoc'"}],
 "env": 1}

Why is iff_assoc unknown? :thinking: It happened because this is how I installed/compiled repl:

git clone git@github.com:leanprover-community/repl.git ~/lean4-repl
cd ~/lean4-repl
lake build

But that gave me the latest version from the master branch. Instead, I should do this:

git clone git@github.com:leanprover-community/repl.git ~/lean4-repl
cd ~/lean4-repl
git checkout v4.9.0
lake build

Because in myproject I am using v4.9.0. Now I get

~/gits/pdl ⑂main* $ lake env ../lean4-repl/.lake/build/bin/repl < commands.json
{"env": 0}

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "'iff_assoc' depends on axioms: [Classical.choice, propext, Quot.sound]"}],
 "env": 1}

:tada:

I think a note that the versions must match in the "Using the REPL from another project" readme section would be good. Should I try to write something and make a PR?

[Kim Morrison]

Malvin Gattinger said:

I think a note that the versions must match in the "Using the REPL from another project" readme section would be good. Should I try to write something and make a PR?

Yes please! (Sorry, I haven't had much time for the REPL recently, but am happy to see work on it happening.)