Allows more granular config for an existing installation of Lake/Lean/REPL

[vadimkantorov]

No docs yet for the new arguments

import os
from lean_interact import LeanREPLConfig, LeanServer, Command

# config = LeanREPLConfig(verbose=True) # download and build Lean REPL
config = LeanREPLConfig(
    lean_version = '',
    setup = False,
    lake_env_repl_path = 'repl',
    lake_command = 'exe',
    lake_path = os.path.expanduser('~/.elan/bin/lake'),
    working_dir = os.path.expanduser('~/mathlib4')
)

server = LeanServer(config)
print(server.run(Command(cmd="theorem ex (n : Nat) : n = 5 → n = 5 := id")))

[vadimkantorov]

without "\n\n\n\n" I was getting hangs with my existing installation of REPL

or maybe it's because "\r\n\r\n" is needed in input as well, as was discussed in leanprover-community/repl#5 (comment) ?

leanprover-community/repl#5 (comment) suggests that "\r\n" is part of JSON-RPC standard

@augustepoiroux I also noticed that you are using universal_newlines=True which seems the deprecated version of text=True, according to https://docs.python.org/3/library/subprocess.html

[augustepoiroux]

Thanks for the PR. I am on vacation now and won't have time to have a proper look into this before a week.

It seems that the REPL has changed since the PR you mention and the version you are using, hence "\n\n" is now enough. It is possible that "\n\n\n\n" or "\r\n\r\n" will not work with current REPL versions.

@augustepoiroux I also noticed that you are using universal_newlines=True which seems the deprecated version of text=True, according to https://docs.python.org/3/library/subprocess.html

If I am not mistaken, we are using text=True in Leaninteract and not universal_newlines=True.

[vadimkantorov]

(You are right, sorry about universal_newlines - I confused it with something else)

[augustepoiroux]

Solved by #21