Bumped

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")