Unable to interacting Lean 4 with toy example

[chenyang-an]

Description:

I've pip install lean-dojo. When I try to run the code

from lean_dojo import *

repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "7d711f6da4584ecb7d4f057715e1f72ba175c910")
theorem = Theorem(repo, "Lean4Example.lean", "hello_world")

with Dojo(theorem) as (dojo, init_state):
  print(init_state)
  result = dojo.run_tac(init_state, "rw [add_assoc, add_comm b, ←add_assoc]")
  assert isinstance(result, ProofFinished)
  print(result)

the following error comes out.

2023-11-02 06:51:36.500 | WARNING  | lean_dojo.interaction.dojo:__init__:174 - Using Lean 4 without a hard timeout may hang indefinitely.
2023-11-02 06:51:51.337 | INFO     | lean_dojo.utils:execute:115 -
2023-11-02 06:51:51.338 | ERROR    | lean_dojo.utils:execute:116 - info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2023-11-01
info: downloading component 'lean'
info: installing component 'lean'
error: ./lake-manifest.json: improperly formatted manifest: incompatible manifest version `4`

Traceback (most recent call last):

  File "<stdin>", line 1, in <module>
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 291, in __enter__
    raise ex
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 235, in __enter__
    self.container.run(
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/container.py", line 315, in run
    execute(cmd, capture_output=capture_output)
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/utils.py", line 117, in execute
    raise ex
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/utils.py", line 112, in execute
    res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command 'docker run --cidfile dlab0mxb.cid --rm -u 501 --mount type=bind,src="/private/var/folders/n1/_6m_g32x3hd51l481mdbdc480000gn/T/tmpay8lgw4e/lean4-example",target="/workspace/lean4-example" --workdir /workspace/lean4-example yangky11/lean-dojo lake build Lean4Repl' returned non-zero exit status 1

The entire operation is on Mac M2 chip.

I've lean 4 installed through VS code on this machine.

The toy code for lean 3 example works just fine, producing the tactic state and the proof finished information.

Thanks for your efforts! This project is amazing!

[yangky11]

Hi,

What's your LeanDojo version?

import lean_dojo
print(lean_dojo.__version__)

[chenyang-an]

Its version is 1.2.5

>>> import lean_dojo
print(lean_dojo.__version__)
>>> print(lean_dojo.__version__)
1.2.5

[yangky11]

I cannot reproduce the problem. Can you quickly try upgrading to the latest version 1.3.0 and see if the problem still persists?

[yangky11]

It should be sufficient to install elan via the instructions here: https://github.com/leanprover/elan#manual-installation. Please try and let me know. Thanks!

[chenyang-an]

After I upgrade to lean 1.3.0 and installed elan from the link, the problem for the example code for interaction with lean 4 persists and there is problem for the example code for interaction with lean 3.

#this is for lean 3
>>> from lean_dojo import *
>>>
>>> repo = LeanGitRepo("https://github.com/yangky11/lean-example", "5a0360e49946815cb53132638ccdd46fb1859e2a")
>>> theorem = Theorem(repo, "src/example.lean", "hello_world")
>>>
>>> with Dojo(theorem) as (dojo, init_state):
...   print(init_state)
...   result = dojo.run_tac(init_state, "rw [add_assoc, add_comm b, ←add_assoc]")
...   assert isinstance(result, ProofFinished)
...   print(result)
...
2023-11-02 07:55:37.178 | WARNING  | lean_dojo.interaction.dojo:__enter__:227 - Docker is strongly recommended when using LeanDojo with Lean 3. See https://leandojo.readthedocs.io/en/latest/user-guide.html#advanced-running-within-docker.
2023-11-02 07:55:37.178 | WARNING  | lean_dojo.container:run_interactive:209 - Disregarding `cpu_limit = 1 since NativeContainer does not support CPU limit.`
2023-11-02 07:55:37.178 | WARNING  | lean_dojo.container:run_interactive:213 - Disregarding `memory_limit = 16g` since NativeContainer does not support memory limit.
Traceback (most recent call last):
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 261, in __enter__
    res = json.loads(self._read_next_line()[0])
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 607, in _read_next_line
    raise EOFError
EOFError

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 293, in __enter__
    raise ex
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 268, in __enter__
    raise DojoInitError("EOF")
lean_dojo.interaction.dojo.DojoInitError: EOF

#this is for lean 4
>>> from lean_dojo import *
>>>
>>> repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "7d711f6da4584ecb7d4f057715e1f72ba175c910")
>>> theorem = Theorem(repo, "Lean4Example.lean", "hello_world")
>>>
>>> with Dojo(theorem) as (dojo, init_state):
...   print(init_state)
...   result = dojo.run_tac(init_state, "rw [add_assoc, add_comm b, ←add_assoc]")
...   assert isinstance(result, ProofFinished)
...   print(result)
...
2023-11-02 07:55:57.964 | WARNING  | lean_dojo.interaction.dojo:__init__:172 - Using Lean 4 without a hard timeout may hang indefinitely.
2023-11-02 07:55:59.850 | INFO     | lean_dojo.utils:execute:115 -
2023-11-02 07:55:59.850 | ERROR    | lean_dojo.utils:execute:116 - error: ./lake-manifest.json: improperly formatted manifest: incompatible manifest version `4`

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 293, in __enter__
    raise ex
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 237, in __enter__
    self.container.run(
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/container.py", line 193, in run
    execute(cmd, capture_output=capture_output)
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/utils.py", line 117, in execute
    raise ex
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/utils.py", line 112, in execute
    res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
  File "/Users/anchenyang/anaconda3/envs/ReProver/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 1.

[yangky11]

The Lean 3 error above is probably related to this warning message: Docker is strongly recommended when using LeanDojo with Lean 3. See https://leandojo.readthedocs.io/en/latest/user-guide.html#advanced-running-within-docker.

In the lastest version of LeanDojo, we made running w/o Docker the default setting. So you may need to set the environment variable CONTAINER to docker when using LeanDojo for Lean 3.

The Lean 4 error above may be related to this line: https://github.com/leanprover/lean4/blob/4934f5c56d5796a19d8669cbe90fd5f238d9810c/src/lake/Lake/Load/Manifest.lean#L87. I'll try updating the lean4-example and let you know.

[chenyang-an]

The Lean 3 error has been resolved by setting the CONTAINER environment variable. And I believe this is the reason for the lean 4 error.

Thanks for your help! And again thanks for this amazing project! This project really makes Lean possible to be used as the backbone for LLM search for theorem proof.