From 6b6118d6a4ef25c04db6c9a82df4bdbcf43d3499 Mon Sep 17 00:00:00 2001 From: "Ruben Thijssen (@rubenthijssen)" Date: Fri, 28 Mar 2025 18:11:44 +1100 Subject: [PATCH] fix: used os.system instead of file in /tmp --- src/itp_interface/main/install.py | 57 +++++++++++++------------------ 1 file changed, 24 insertions(+), 33 deletions(-) diff --git a/src/itp_interface/main/install.py b/src/itp_interface/main/install.py index 19a15ce..b580d7b 100644 --- a/src/itp_interface/main/install.py +++ b/src/itp_interface/main/install.py @@ -3,29 +3,35 @@ import string file_path = os.path.abspath(__file__) -def generate_random_string(length, allowed_chars = None): + + +def generate_random_string(length, allowed_chars=None): if allowed_chars is None: allowed_chars = string.ascii_letters + string.digits return ''.join(random.choice(allowed_chars) for _ in range(length)) + def install_itp_interface(): print("Installing itp_interface") itp_dir = os.path.dirname(os.path.dirname(file_path)) tools_dir = os.path.join(itp_dir, "tools") repl_dir = os.path.join(tools_dir, "repl") assert os.path.exists(repl_dir), f"repl_dir: {repl_dir} does not exist" - assert os.path.exists(os.path.join(repl_dir, "lean-toolchain")), f"lean-toolchain does not exist in {repl_dir}, build has failed" + assert os.path.exists(os.path.join(repl_dir, "lean-toolchain") + ), f"lean-toolchain does not exist in {repl_dir}, build has failed" print("repl_dir: ", repl_dir) print("Building itp_interface") os.system(f"cd {repl_dir} && lake build repl") + def install_lean_repl(): print("Updating Lean") itp_dir = os.path.dirname(os.path.dirname(file_path)) tools_dir = os.path.join(itp_dir, "tools") repl_dir = os.path.join(tools_dir, "repl") assert os.path.exists(repl_dir), f"repl_dir: {repl_dir} does not exist" - assert os.path.exists(os.path.join(repl_dir, "lean-toolchain")), f"lean-toolchain does not exist in {repl_dir}, build has failed" + assert os.path.exists(os.path.join(repl_dir, "lean-toolchain") + ), f"lean-toolchain does not exist in {repl_dir}, build has failed" print("repl_dir: ", repl_dir) assert os.system("git --version") == 0, "git is not installed" print("[OK] git is installed") @@ -48,7 +54,8 @@ def install_lean_repl(): output = os.popen(cmd_to_run).read() print("Output: ", output) if output == "": - print(f"Could not find a commit with message containing {lean_version}") + print( + f"Could not find a commit with message containing {lean_version}") print("Probably this version does not exist in the git history of the REPL") lean_version = "4.7.0-rc2" print("Switching to v4.7.0-rc2 on commit 97182f0") @@ -71,36 +78,20 @@ def install_lean_repl(): elan_url = "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh" os.system(f"curl -sSL {elan_url} -sSf | sh -s -- -y") print("[OK] .elan installed") + lean_repo = "leanprover/lean4" - # Create a temporary script to run - shell_code = f"""source $HOME/.elan/env -echo "Installing Lean 4 ({lean_repo}:{lean_version})..." -elan toolchain install {lean_repo}:{lean_version} -elan override set {lean_repo}:{lean_version} -echo "Installed Lean 4 ({lean_repo}:{lean_version}) successfully!" -export PATH=$PATH:$HOME/.elan/bin""" - random_string = os.urandom(8).hex() - number = random.randint(1, 10) - lens = [random.randint(1, 10) for _ in range(number)] - rand_dirnames = [generate_random_string(l) for l in lens] - random_path = "/".join(rand_dirnames) - os.makedirs(f"/tmp/{random_path}", exist_ok=True) - random_sh_path = f"/tmp/{random_path}/{random_string}.sh" - print(f"Writing the script to {random_sh_path}") - with open(random_sh_path, "w") as f: - f.write(shell_code) - os.system(f"chmod +x {random_sh_path}") - print("Running the script") - os.system(f"bash {random_sh_path}") - print("Removing the script") - os.system(f"rm {random_sh_path}") - os.system(f"rmdir /tmp/{random_path}") + os.system("source $HOME/.elan/env") + os.system(f"echo 'Installing Lean 4 ({lean_repo}:{lean_version})...'") + os.system(f"elan toolchain install {lean_repo}:{lean_version}") + os.system(f"elan override set {lean_repo}:{lean_version}") + os.system( + f"echo 'Installed Lean 4 ({lean_repo}:{lean_version}) successfully!'") + os.system("export PATH=$PATH:$HOME/.elan/bin") + os.system("ls -l $HOME/.elan/bin") - assert os.system("export PATH=$PATH:$HOME/.elan/bin && lean --version") == 0, "Lean 4 is not installed aborting" - print("[OK] Lean 4 installed successfully") - print("NOTE: Please run `install-itp-interface` to finish the installation") + assert os.system( + "export PATH=$PATH:$HOME/.elan/bin && lean --version") == 0, "Lean 4 is not installed aborting" + print("[OK] Lean 4 installed successfully") - - - + print("NOTE: Please run `install-itp-interface` to finish the installation")