From 4abbdddae69da974f80461c0561ba92cf62851c4 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Fri, 21 Mar 2025 11:20:09 -0500 Subject: [PATCH 1/2] Fixed build script --- .github/workflows/github-build-actions.yaml | 20 ++++++++----- pyproject.toml | 4 +-- src/itp_interface/main/install.py | 31 +++++++++++++++------ 3 files changed, 37 insertions(+), 18 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 96da286..4e58cdb 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -54,17 +54,23 @@ jobs: opam repo add coq-released https://coq.inria.fr/opam/released opam pin add -y coq-lsp 0.1.8+8.18 - - name: Install Lean (elan) - shell: bash - run: | - curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y - source $HOME/.elan/env + # - name: Install Lean (elan) + # shell: bash + # run: | + # curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y + # source $HOME/.elan/env - - name: Prepare Lean REPL + - name: Install Lean (elan) and prepare Lean REPL shell: bash run: | - source $HOME/.elan/env install-lean-repl + source $HOME/.elan/env + + # - name: Prepare Lean REPL + # shell: bash + # run: | + # source $HOME/.elan/env + # install-lean-repl - name: Build Lean REPL for itp-interface shell: bash diff --git a/pyproject.toml b/pyproject.toml index 8d03d97..60dc23f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -5,7 +5,7 @@ requires = [ build-backend = "hatchling.build" [project] name = "itp_interface" -version = "1.1.8" +version = "1.1.9" authors = [ { name="Amitayush Thakur", email="amitayush@utexas.edu" }, ] @@ -26,7 +26,7 @@ dependencies = [ "sexpdata==1.0.0", "pampy==0.3.0", "ray==2.36.0", - "pydantic==1.10.13", + "pydantic>=2.10.6", "faiss-cpu>=1.6.1", "filelock==3.12.4", "regex==2023.10.3", diff --git a/src/itp_interface/main/install.py b/src/itp_interface/main/install.py index 2fc8b5b..971b043 100644 --- a/src/itp_interface/main/install.py +++ b/src/itp_interface/main/install.py @@ -1,6 +1,13 @@ import os +import random +import string file_path = os.path.abspath(__file__) +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)) @@ -66,23 +73,29 @@ def install_lean_repl(): print("[OK] .elan installed") lean_repo = "leanprover/lean4" # Create a temporary script to run - shell_code = f""" -source $HOME/.elan/env + 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 -""" +export PATH=$PATH:$HOME/.elan/bin""" random_string = os.urandom(8).hex() - with open(f"/tmp/{random_string}.sh", "w") as f: + 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 /tmp/{random_string}.sh") + os.system(f"chmod +x {random_sh_path}") print("Running the script") - os.system(f"bash /tmp/{random_string}.sh") + os.system(f"bash {random_sh_path}") print("Removing the script") - os.system(f"rm /tmp/{random_string}.sh") - assert os.system("lean --version") == 0, "Lean 4 is not installed aborting" + os.system(f"rm {random_sh_path}") + os.system(f"rmdir /tmp/{random_path}") + assert os.system("source $HOME/.elan/env && 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") From 4e4e0c8171dbf27f41c20fd0a5f07e0fcbad2f33 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Fri, 21 Mar 2025 11:58:12 -0500 Subject: [PATCH 2/2] Fixed install and action script. --- .github/workflows/github-build-actions.yaml | 36 +++++++-------------- src/itp_interface/main/install.py | 5 +-- 2 files changed, 15 insertions(+), 26 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 4e58cdb..302425c 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -41,6 +41,18 @@ jobs: - name: Install package run: pip install dist/*.whl --break-system-packages + - name: Install Lean (elan) and prepare Lean REPL + shell: bash + run: | + install-lean-repl + source $HOME/.elan/env + + - name: Build Lean REPL for itp-interface + shell: bash + run: | + source $HOME/.elan/env + install-itp-interface + - name: Check and Init opam version run: | opam --version @@ -54,30 +66,6 @@ jobs: opam repo add coq-released https://coq.inria.fr/opam/released opam pin add -y coq-lsp 0.1.8+8.18 - # - name: Install Lean (elan) - # shell: bash - # run: | - # curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y - # source $HOME/.elan/env - - - name: Install Lean (elan) and prepare Lean REPL - shell: bash - run: | - install-lean-repl - source $HOME/.elan/env - - # - name: Prepare Lean REPL - # shell: bash - # run: | - # source $HOME/.elan/env - # install-lean-repl - - - name: Build Lean REPL for itp-interface - shell: bash - run: | - source $HOME/.elan/env - install-itp-interface - - name: List repository files (debug step) run: find . -type f diff --git a/src/itp_interface/main/install.py b/src/itp_interface/main/install.py index 971b043..19a15ce 100644 --- a/src/itp_interface/main/install.py +++ b/src/itp_interface/main/install.py @@ -69,7 +69,7 @@ def install_lean_repl(): else: print("Installing .elan") elan_url = "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh" - os.system(f"curl -sSL {elan_url} | 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 @@ -95,7 +95,8 @@ def install_lean_repl(): print("Removing the script") os.system(f"rm {random_sh_path}") os.system(f"rmdir /tmp/{random_path}") - assert os.system("source $HOME/.elan/env && export PATH=$PATH:$HOME/.elan/bin && lean --version") == 0, "Lean 4 is not installed aborting" + 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")