Lean Repl unable to run with canonical

[FrederickPu]

I have a lean project that is dependent on both canonical and lean repl. But when I try to call the canonical tactic in lean repl it fails.

import json
import subprocess
import os
import sys
from typing import List, Any

process = subprocess.Popen(
    ["lake", "exe", "repl", "--load-dynlib=./.lake/packages/Canonical/.lake/build/lib/canonical_lean.dll"],
    stdin=subprocess.PIPE,
    stdout=subprocess.PIPE,
    text=True,
    bufsize=1,
    env=os.environ,
)

def send_command(command):
    json_command = json.dumps(command, ensure_ascii=False) + "\n\n"
    process.stdin.write(json_command)
    process.stdin.flush()

    response_lines = []
    while True:
        stdout_line = process.stdout.readline()
        if stdout_line.strip() == "":
            break
        response_lines.append(stdout_line)

    return json.loads("".join(response_lines))

lol = send_command({ "cmd" : "import Canonical\nimport Mathlib\ntheorem womp : (2:Nat) + 2 = 4 := by canonical" })
print(lol)
env_import = lol["env"]
print(env_import)

The above code produces the following error:

{'sorries': [{'proofState': 0, 'pos': {'line': 3, 'column': 37}, 'goal': '⊢ 2 + 2 = 4', 'endPos': {'line': 3, 'column': 42}}], 'messages': [{'severity': 'warning', 'pos': {'line': 3, 'column': 8}, 'endPos': {'line': 3, 'column': 12}, 'data': "declaration uses 'sorry'"}], 'env': 0}
0
PS C:\Users\pufre\Downloads\CodingProjects\CanonicalDrafter> python .\canonical_repl_broken_mwe.py
libc++abi: terminating due to uncaught exception of type lean::exception: Could not find native implementation of external declaration 'Canonical.canonical' (symbols 'l_Canonical_canonical___boxed' or 'l_Canonical_canonical').
For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.
Traceback (most recent call last):
  File "C:\Users\pufre\Downloads\CodingProjects\CanonicalDrafter\canonical_repl_broken_mwe.py", line 30, in <module>
    lol = send_command({ "cmd" : "import Canonical\nimport Mathlib\ntheorem womp : (2:Nat) + 2 = 4 := by canonical" })
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\Downloads\CodingProjects\CanonicalDrafter\canonical_repl_broken_mwe.py", line 28, in send_command
    return json.loads("".join(response_lines))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.11.0b4\Lib\json\__init__.py", line 346, in loads
    return _default_decoder.decode(s)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.11.0b4\Lib\json\decoder.py", line 337, in decode
    obj, end = self.raw_decode(s, idx=_w(s, 0).end())
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.11.0b4\Lib\json\decoder.py", line 355, in raw_decode
    raise JSONDecodeError("Expecting value", s, err.value) from None
json.decoder.JSONDecodeError: Expecting value: line 1 column 1 (char 0)

[augustepoiroux]

Interesting, do you have a minimal Github Lean project with canonical set up? I am interested in reproducing your issue.
Are you on Windows? I see a canonical_lean.dll

[FrederickPu]

yeah im on windows

[FrederickPu]

im gonna try again on linux to see if I still get the error

[FrederickPu]

this is my lakefile (it's basically an empty project)

import Lake
open Lake DSL

package canonicaldrafter where
  name := `CanonicalDrafter
  defaultTargets := #["canonicaldrafter-wrapper"]
  supportInterpreter := true

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "v4.21.0"

require "chasenorman" / "Canonical"

require REPL from git "https://github.com/leanprover-community/repl" @ "v4.21.0"

lean_lib CanonicalDrafter where
  -- Your library code here if needed

[FrederickPu]

when I switch to linux the error is gone but i still get a elaboration issue:

(base) neuman@Neuman:/mnt/c/Users/pufre/Downloads/CodingProjects/CanonicalDrafter$ python canonical_repl_broken_mwe.py 
{'messages': [{'severity': 'error', 'pos': {'line': 3, 'column': 22}, 'endPos': {'line': 3, 'column': 24}, 'data': "unexpected token '+'; expected ':=', 'where' or '|'"}], 'env': 0}

[augustepoiroux]

I think this last error you get is because Canonical is not imported (maybe lake build failed or something?)
I tried on Linux, and I get the same error than the one you get on Windows. Not sure how to solve this ^^'

[FrederickPu]

yee

(base) neuman@Neuman:/mnt/c/Users/pufre/Downloads/CodingProjects/CanonicalDrafter$ lake exe repl
{ "cmd" : "import Canonical" }

uncaught exception: {"message": "Could not parse JSON:\noffset 27: unexpected character in object"}

[eric-wieser]

That looks like a stray \r caused by the windows line endings?

[FrederickPu]

I don't think that's the issue cause when I run with lake env i get the libc++abi error again

[FrederickPu]

I was able to get it working by using Lean.loadDynlib in the runCommand function
https://github.com/FrederickPu/repl/blob/595d86879967f7cb0b982ad5436662783ac375a1/REPL/Main.lean#L296
I think the repl doesn't currently support taking Dynlib's as arguments

[FrederickPu]

Should we add a dynlib command line option for lean repl? We've had similar issues come up when trying to use it for LeanEuclid

[augustepoiroux]

Sounds good to me!

[FrederickPu]

I've done the changes here: https://github.com/leanprover-community/repl/pull/124/files. I'm not sure how to write a test for it tho do we add canonical or leansmt to the test folder kinda like we do for mathlib?

[augustepoiroux]

Nice! Regarding the test, it might be a bit tricky to maintain such a test if canonical or leansmt are not updated for each Lean version... Don't know what would be the best option. Maybe creating a dummy dynlib for testing?

[FrederickPu]

The tests would prob only work one platform (eg linux is .so windows is .dll and make is .dynlib). So we might need a cmakelists too