Fixed install and action script.

Author: Amitayush Thakur

.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
 

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