Fixed build script; updated pydantic; fixed install race conditions

.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,24 +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: 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
 

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

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))
@@ -62,27 +69,34 @@ 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
-        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}")
+        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")