|
1 | 1 | import os |
| 2 | +import random |
| 3 | +import string |
2 | 4 |
|
3 | 5 | file_path = os.path.abspath(__file__) |
| 6 | +def generate_random_string(length, allowed_chars = None): |
| 7 | + if allowed_chars is None: |
| 8 | + allowed_chars = string.ascii_letters + string.digits |
| 9 | + return ''.join(random.choice(allowed_chars) for _ in range(length)) |
| 10 | + |
4 | 11 | def install_itp_interface(): |
5 | 12 | print("Installing itp_interface") |
6 | 13 | itp_dir = os.path.dirname(os.path.dirname(file_path)) |
@@ -62,27 +69,34 @@ def install_lean_repl(): |
62 | 69 | else: |
63 | 70 | print("Installing .elan") |
64 | 71 | elan_url = "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh" |
65 | | - os.system(f"curl -sSL {elan_url} | sh") |
| 72 | + os.system(f"curl -sSL {elan_url} -sSf | sh -s -- -y") |
66 | 73 | print("[OK] .elan installed") |
67 | 74 | lean_repo = "leanprover/lean4" |
68 | 75 | # Create a temporary script to run |
69 | | - shell_code = f""" |
70 | | -source $HOME/.elan/env |
| 76 | + shell_code = f"""source $HOME/.elan/env |
71 | 77 | echo "Installing Lean 4 ({lean_repo}:{lean_version})..." |
72 | 78 | elan toolchain install {lean_repo}:{lean_version} |
73 | 79 | elan override set {lean_repo}:{lean_version} |
74 | 80 | echo "Installed Lean 4 ({lean_repo}:{lean_version}) successfully!" |
75 | | -export PATH=$PATH:$HOME/.elan/bin |
76 | | -""" |
| 81 | +export PATH=$PATH:$HOME/.elan/bin""" |
77 | 82 | random_string = os.urandom(8).hex() |
78 | | - with open(f"/tmp/{random_string}.sh", "w") as f: |
| 83 | + number = random.randint(1, 10) |
| 84 | + lens = [random.randint(1, 10) for _ in range(number)] |
| 85 | + rand_dirnames = [generate_random_string(l) for l in lens] |
| 86 | + random_path = "/".join(rand_dirnames) |
| 87 | + os.makedirs(f"/tmp/{random_path}", exist_ok=True) |
| 88 | + random_sh_path = f"/tmp/{random_path}/{random_string}.sh" |
| 89 | + print(f"Writing the script to {random_sh_path}") |
| 90 | + with open(random_sh_path, "w") as f: |
79 | 91 | f.write(shell_code) |
80 | | - os.system(f"chmod +x /tmp/{random_string}.sh") |
| 92 | + os.system(f"chmod +x {random_sh_path}") |
81 | 93 | print("Running the script") |
82 | | - os.system(f"bash /tmp/{random_string}.sh") |
| 94 | + os.system(f"bash {random_sh_path}") |
83 | 95 | print("Removing the script") |
84 | | - os.system(f"rm /tmp/{random_string}.sh") |
85 | | - assert os.system("lean --version") == 0, "Lean 4 is not installed aborting" |
| 96 | + os.system(f"rm {random_sh_path}") |
| 97 | + os.system(f"rmdir /tmp/{random_path}") |
| 98 | + os.system("ls -l $HOME/.elan/bin") |
| 99 | + assert os.system("export PATH=$PATH:$HOME/.elan/bin && lean --version") == 0, "Lean 4 is not installed aborting" |
86 | 100 | print("[OK] Lean 4 installed successfully") |
87 | 101 | print("NOTE: Please run `install-itp-interface` to finish the installation") |
88 | 102 |
|
|
0 commit comments