From 3d65bb65d82f39d8cd537a2840ead86d4243b0ff Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 22:09:54 -0600 Subject: [PATCH 01/22] Create github-build-actions.yaml Added vanilla build actions Signed-off-by: Amitayush Thakur --- .github/workflows/github-build-actions.yaml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 .github/workflows/github-build-actions.yaml diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml new file mode 100644 index 0000000..3f5e224 --- /dev/null +++ b/.github/workflows/github-build-actions.yaml @@ -0,0 +1,18 @@ +name: GitHub itp-interface build +run-name: ${{ github.actor }} is testing out GitHub Actions 🚀 +on: [push] +jobs: + Explore-GitHub-Actions: + runs-on: ubuntu-latest + steps: + - run: echo "🎉 The job was automatically triggered by a ${{ github.event_name }} event." + - run: echo "🐧 This job is now running on a ${{ runner.os }} server hosted by GitHub!" + - run: echo "🔎 The name of your branch is ${{ github.ref }} and your repository is ${{ github.repository }}." + - name: Check out repository code + uses: actions/checkout@v4 + - run: echo "💡 The ${{ github.repository }} repository has been cloned to the runner." + - run: echo "🖥️ The workflow is now ready to test your code on the runner." + - name: List files in the repository + run: | + ls ${{ github.workspace }} + - run: echo "🍏 This job's status is ${{ job.status }}." From 245ae8a187e4982d9311cc8d6aee6c6e1f1ba820 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 22:12:49 -0600 Subject: [PATCH 02/22] Changed the build action --- .github/workflows/github-build-actions.yaml | 47 ++++++++++++++------- 1 file changed, 32 insertions(+), 15 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 3f5e224..a584c65 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -1,18 +1,35 @@ -name: GitHub itp-interface build -run-name: ${{ github.actor }} is testing out GitHub Actions 🚀 -on: [push] +name: Build, Package, and Test + +on: + push: + branches: [main] + pull_request: + branches: [main] + jobs: - Explore-GitHub-Actions: + build-test: runs-on: ubuntu-latest + steps: - - run: echo "🎉 The job was automatically triggered by a ${{ github.event_name }} event." - - run: echo "🐧 This job is now running on a ${{ runner.os }} server hosted by GitHub!" - - run: echo "🔎 The name of your branch is ${{ github.ref }} and your repository is ${{ github.repository }}." - - name: Check out repository code - uses: actions/checkout@v4 - - run: echo "💡 The ${{ github.repository }} repository has been cloned to the runner." - - run: echo "🖥️ The workflow is now ready to test your code on the runner." - - name: List files in the repository - run: | - ls ${{ github.workspace }} - - run: echo "🍏 This job's status is ${{ job.status }}." + - name: Checkout repository + uses: actions/checkout@v3 + + - name: Set up Python 3.10 + uses: actions/setup-python@v4 + with: + python-version: '3.10' + + - name: Upgrade pip + run: python -m pip install --upgrade pip + + - name: Install build tool + run: pip install build + + - name: Build package + run: python -m build + + - name: Install package + run: pip install dist/*.whl + + - name: Run tests + run: python src/test/simple_env_test.py \ No newline at end of file From 8533f59408fd6ae54c361dc8e64803eeb3687a8f Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 22:26:54 -0600 Subject: [PATCH 03/22] Fixed the workflow --- .github/workflows/github-build-actions.yaml | 49 ++++++++++++++++--- .../{simpl_env_test.py => simple_env_test.py} | 0 2 files changed, 43 insertions(+), 6 deletions(-) rename src/test/{simpl_env_test.py => simple_env_test.py} (100%) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index a584c65..ff62111 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -19,11 +19,10 @@ jobs: with: python-version: '3.10' - - name: Upgrade pip - run: python -m pip install --upgrade pip - - - name: Install build tool - run: pip install build + - name: Upgrade pip and install build tool + run: | + python -m pip install --upgrade pip + pip install build - name: Build package run: python -m build @@ -31,5 +30,43 @@ jobs: - name: Install package run: pip install dist/*.whl + - name: Install opam and OCaml + run: | + sudo apt-get update + sudo apt-get install -y build-essential unzip bubblewrap + # Install opam via the official script + sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) + # Initialize opam without sandboxing (suitable for CI) + opam init --disable-sandboxing --yes + # Create a switch with OCaml 4.14.0 (adjust as needed) + opam switch create default ocaml-base-compiler.4.14.0 --yes + # Make sure the current shell knows about the opam environment + eval $(opam env) + + - name: Install Lean (elan) + run: | + # Install elan, the Lean version manager + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y + # Source the Lean environment so that lean is on the PATH + source $HOME/.elan/env + + - name: Prepare Lean REPL + run: | + source $HOME/.elan/env + # Run the project script to prepare the Lean REPL + install-lean-repl + + - name: Build Lean REPL for itp-interface + run: | + source $HOME/.elan/env + install-itp-interface + + - name: List repository files (debug step) + run: find . -type f + - name: Run tests - run: python src/test/simple_env_test.py \ No newline at end of file + run: | + # Load environments before running tests + eval $(opam env) + source $HOME/.elan/env + python src/test/simple_env_test.py \ No newline at end of file diff --git a/src/test/simpl_env_test.py b/src/test/simple_env_test.py similarity index 100% rename from src/test/simpl_env_test.py rename to src/test/simple_env_test.py From 52ca507d1d3bdc046d7aa8bd90e0fa1f573308f7 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 22:31:37 -0600 Subject: [PATCH 04/22] Fixed the opam installation to non-interactive --- .github/workflows/github-build-actions.yaml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index ff62111..f5197c3 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -34,13 +34,13 @@ jobs: run: | sudo apt-get update sudo apt-get install -y build-essential unzip bubblewrap - # Install opam via the official script - sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) - # Initialize opam without sandboxing (suitable for CI) + # Install opam non-interactively by piping the default answer + printf "/usr/local/bin\n" | sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) + # Initialize opam (disable sandboxing for CI) opam init --disable-sandboxing --yes - # Create a switch with OCaml 4.14.0 (adjust as needed) + # Create an OCaml switch with the desired compiler version (adjust as needed) opam switch create default ocaml-base-compiler.4.14.0 --yes - # Make sure the current shell knows about the opam environment + # Update the shell environment for opam eval $(opam env) - name: Install Lean (elan) From 15d706e0af87664f19bf488b935251aafa8fd0a7 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 22:37:59 -0600 Subject: [PATCH 05/22] Added default switch check --- .github/workflows/github-build-actions.yaml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index f5197c3..47d4376 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -38,10 +38,14 @@ jobs: printf "/usr/local/bin\n" | sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) # Initialize opam (disable sandboxing for CI) opam init --disable-sandboxing --yes - # Create an OCaml switch with the desired compiler version (adjust as needed) - opam switch create default ocaml-base-compiler.4.14.0 --yes - # Update the shell environment for opam - eval $(opam env) + # Check if the "default" switch exists; if not, create it. + if opam switch list --short | grep -q "^default$"; then + echo "Switch 'default' already exists, using it." + else + opam switch create default ocaml-base-compiler.4.14.0 --yes + fi + # Update the current shell's environment with the default switch + eval $(opam env --switch=default) - name: Install Lean (elan) run: | From 01b14ceb4cbb42ec7c555982d74ef2c36289a7b0 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 22:43:42 -0600 Subject: [PATCH 06/22] Added publish yaml --- .github/workflows/github-publish-actions.yaml | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 .github/workflows/github-publish-actions.yaml diff --git a/.github/workflows/github-publish-actions.yaml b/.github/workflows/github-publish-actions.yaml new file mode 100644 index 0000000..527e10a --- /dev/null +++ b/.github/workflows/github-publish-actions.yaml @@ -0,0 +1,36 @@ +name: Publish to PyPI + +on: + push: + # This example triggers on any branch named "release" + branches: + - release + +jobs: + publish: + runs-on: ubuntu-latest + permissions: + contents: read + id-token: write # Required for OIDC authentication + + steps: + - name: Checkout code + uses: actions/checkout@v3 + + - name: Set up Python + uses: actions/setup-python@v4 + with: + python-version: '3.10' # Adjust your Python version as needed + + - name: Upgrade pip and install build tools + run: | + python -m pip install --upgrade pip + pip install build twine + + - name: Build package + run: python -m build + + - name: Publish package to PyPI via OIDC + uses: pypa/gh-action-pypi-publish@v1.5.0 + # Do not specify the `pypi-token` input so that the action uses OIDC authentication. + # If you need to debug, you can set a token via secrets, but for OIDC leave it out. From 083f628c945beb28c28f3f7dd85a36b81b4f8a3a Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 22:48:02 -0600 Subject: [PATCH 07/22] Fixed submodule checkout --- .github/workflows/github-build-actions.yaml | 2 ++ .github/workflows/github-publish-actions.yaml | 4 +++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 47d4376..7cd603e 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -13,6 +13,8 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@v3 + with: + submodules: true # This ensures that all submodules are also checked out - name: Set up Python 3.10 uses: actions/setup-python@v4 diff --git a/.github/workflows/github-publish-actions.yaml b/.github/workflows/github-publish-actions.yaml index 527e10a..818ee6c 100644 --- a/.github/workflows/github-publish-actions.yaml +++ b/.github/workflows/github-publish-actions.yaml @@ -14,8 +14,10 @@ jobs: id-token: write # Required for OIDC authentication steps: - - name: Checkout code + - name: Checkout repository uses: actions/checkout@v3 + with: + submodules: true # This ensures that all submodules are also checked out - name: Set up Python uses: actions/setup-python@v4 From b698e9907ebd44f5db0163c0c106f4bfaf6c793d Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 23:24:48 -0600 Subject: [PATCH 08/22] Added default coq image --- .github/workflows/github-build-actions.yaml | 39 ++++++++++++------- .../github-enforce-main-to-release.yaml | 19 +++++++++ src/test/simple_env_test.py | 4 +- 3 files changed, 45 insertions(+), 17 deletions(-) create mode 100644 .github/workflows/github-enforce-main-to-release.yaml diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 7cd603e..0bc1f55 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -9,6 +9,8 @@ on: jobs: build-test: runs-on: ubuntu-latest + container: + image: coqorg/coq:8.18.0-ocaml-4.14.2-flambda # or use coqcommunity/docker-coq:latest steps: - name: Checkout repository @@ -32,22 +34,29 @@ jobs: - name: Install package run: pip install dist/*.whl - - name: Install opam and OCaml + - name: Verify Coq and opam versions run: | - sudo apt-get update - sudo apt-get install -y build-essential unzip bubblewrap - # Install opam non-interactively by piping the default answer - printf "/usr/local/bin\n" | sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) - # Initialize opam (disable sandboxing for CI) - opam init --disable-sandboxing --yes - # Check if the "default" switch exists; if not, create it. - if opam switch list --short | grep -q "^default$"; then - echo "Switch 'default' already exists, using it." - else - opam switch create default ocaml-base-compiler.4.14.0 --yes - fi - # Update the current shell's environment with the default switch - eval $(opam env --switch=default) + echo "Coq version:" + coqc --version + echo "opam version:" + opam --version + + # - name: Install opam and OCaml + # run: | + # sudo apt-get update + # sudo apt-get install -y build-essential unzip bubblewrap + # # Install opam non-interactively by piping the default answer + # printf "/usr/local/bin\n" | sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) + # # Initialize opam (disable sandboxing for CI) + # opam init --disable-sandboxing --yes + # # Check if the "default" switch exists; if not, create it. + # if opam switch list --short | grep -q "^default$"; then + # echo "Switch 'default' already exists, using it." + # else + # opam switch create default ocaml-base-compiler.4.14.0 --yes + # fi + # # Update the current shell's environment with the default switch + # eval $(opam env --switch=default) - name: Install Lean (elan) run: | diff --git a/.github/workflows/github-enforce-main-to-release.yaml b/.github/workflows/github-enforce-main-to-release.yaml new file mode 100644 index 0000000..8f5bf91 --- /dev/null +++ b/.github/workflows/github-enforce-main-to-release.yaml @@ -0,0 +1,19 @@ +name: Enforce Main-to-Release Merges + +on: + pull_request: + # This workflow will run for any PR whose base branch is "release" + branches: [release] + types: [opened, synchronize, reopened] + +jobs: + check-source-branch: + runs-on: ubuntu-latest + steps: + - name: Check that PR comes from main branch + run: | + echo "PR head branch: ${{ github.event.pull_request.head.ref }}" + if [ "${{ github.event.pull_request.head.ref }}" != "main" ]; then + echo "Error: Only PRs originating from the 'main' branch can be merged into 'release'." + exit 1 + fi diff --git a/src/test/simple_env_test.py b/src/test/simple_env_test.py index 03abd04..bfc24bf 100644 --- a/src/test/simple_env_test.py +++ b/src/test/simple_env_test.py @@ -21,10 +21,10 @@ def build_coq_project(self, project_folder): except: self.current_switch = None # Check if the switch exists - # opam switch create simple_grp_theory 4.14.1 + # opam switch create simple_grp_theory 4.14.2 if os.system("opam switch simple_grp_theory") != 0: cmds = [ - 'opam switch create simple_grp_theory 4.14.1', + 'opam switch create simple_grp_theory 4.14.2', 'opam switch simple_grp_theory', 'eval $(opam env)', 'opam repo add coq-released https://coq.inria.fr/opam/released', From 59976440b06527a1ca3383aed69d72e9c64c52cf Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 23:29:30 -0600 Subject: [PATCH 09/22] Added root dependencies --- .github/workflows/github-build-actions.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 0bc1f55..1b142fa 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -11,6 +11,7 @@ jobs: runs-on: ubuntu-latest container: image: coqorg/coq:8.18.0-ocaml-4.14.2-flambda # or use coqcommunity/docker-coq:latest + options: --user 0 # Run as root to install dependencies steps: - name: Checkout repository From e49ef18e607d5a66a435ce70ced30614e7111231 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 23:48:41 -0600 Subject: [PATCH 10/22] Changing the python to 3.9 which is Debian Bullseye --- .github/workflows/github-build-actions.yaml | 4 ++-- README.md | 2 +- pyproject.toml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 1b142fa..234977a 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -19,10 +19,10 @@ jobs: with: submodules: true # This ensures that all submodules are also checked out - - name: Set up Python 3.10 + - name: Set up Python 3.9 uses: actions/setup-python@v4 with: - python-version: '3.10' + python-version: '3.9' - name: Upgrade pip and install build tool run: | diff --git a/README.md b/README.md index 80abe48..9215122 100644 --- a/README.md +++ b/README.md @@ -137,7 +137,7 @@ file_path = "src/data/test/coq/custom_group_theory/theories/grpthm.v" # Create a switch for building the Coq project if os.system("opam switch simple_grp_theory") != 0: cmds = [ - 'opam switch create simple_grp_theory 4.14.1', + 'opam switch create simple_grp_theory 4.14.2', 'opam switch simple_grp_theory', 'eval $(opam env)', 'opam repo add coq-released https://coq.inria.fr/opam/released', diff --git a/pyproject.toml b/pyproject.toml index 557bdcb..bc40253 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -11,7 +11,7 @@ authors = [ ] description = "Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving." readme = "README.md" -requires-python = ">=3.10, <3.13" +requires-python = ">=3.9, <3.13" classifiers = [ "Programming Language :: Python :: 3", "License :: OSI Approved :: MIT License", From 304c271ea91d912d46afb371c1a2030c6378beae Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 23:56:10 -0600 Subject: [PATCH 11/22] Fixed python version --- .github/workflows/github-build-actions.yaml | 7 +++---- .github/workflows/github-publish-actions.yaml | 7 +++---- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 234977a..bdf3ec1 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -19,10 +19,9 @@ jobs: with: submodules: true # This ensures that all submodules are also checked out - - name: Set up Python 3.9 - uses: actions/setup-python@v4 - with: - python-version: '3.9' + # Omit the setup-python step to use the container's Python + - name: Check system Python version + run: python --version - name: Upgrade pip and install build tool run: | diff --git a/.github/workflows/github-publish-actions.yaml b/.github/workflows/github-publish-actions.yaml index 818ee6c..aeed8e3 100644 --- a/.github/workflows/github-publish-actions.yaml +++ b/.github/workflows/github-publish-actions.yaml @@ -19,10 +19,9 @@ jobs: with: submodules: true # This ensures that all submodules are also checked out - - name: Set up Python - uses: actions/setup-python@v4 - with: - python-version: '3.10' # Adjust your Python version as needed + # Omit the setup-python step to use the container's Python + - name: Check system Python version + run: python --version - name: Upgrade pip and install build tools run: | From 35194e7a4d7d3655c0847c821553cb846897011c Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 00:02:47 -0600 Subject: [PATCH 12/22] Added python setup code. --- .github/workflows/github-build-actions.yaml | 7 ++++++- .github/workflows/github-publish-actions.yaml | 7 ++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index bdf3ec1..6a6c7fa 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -19,7 +19,12 @@ jobs: with: submodules: true # This ensures that all submodules are also checked out - # Omit the setup-python step to use the container's Python + - name: Install Python and pip + run: | + apt-get update + apt-get install -y python3 python3-pip + ln -sf /usr/bin/python3 /usr/bin/python + - name: Check system Python version run: python --version diff --git a/.github/workflows/github-publish-actions.yaml b/.github/workflows/github-publish-actions.yaml index aeed8e3..818ee6c 100644 --- a/.github/workflows/github-publish-actions.yaml +++ b/.github/workflows/github-publish-actions.yaml @@ -19,9 +19,10 @@ jobs: with: submodules: true # This ensures that all submodules are also checked out - # Omit the setup-python step to use the container's Python - - name: Check system Python version - run: python --version + - name: Set up Python + uses: actions/setup-python@v4 + with: + python-version: '3.10' # Adjust your Python version as needed - name: Upgrade pip and install build tools run: | From a50197b5e491238c2d501c97a63db0ca4080f79d Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 00:06:08 -0600 Subject: [PATCH 13/22] Added break system flag. --- .github/workflows/github-build-actions.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 6a6c7fa..65631d0 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -30,7 +30,7 @@ jobs: - name: Upgrade pip and install build tool run: | - python -m pip install --upgrade pip + python -m pip install --upgrade pip --break-system-packages pip install build - name: Build package From 274b39587611be40d963cb11a67bc94dcb8f6ae7 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 00:10:29 -0600 Subject: [PATCH 14/22] Added break system packages --- .github/workflows/github-build-actions.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 65631d0..b970992 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -31,7 +31,7 @@ jobs: - name: Upgrade pip and install build tool run: | python -m pip install --upgrade pip --break-system-packages - pip install build + pip install build --break-system-packages - name: Build package run: python -m build From aaa92fa20a6cd9456e5378cdae43cf8176d6ec0a Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 00:13:53 -0600 Subject: [PATCH 15/22] Fixed pip issues. --- .github/workflows/github-build-actions.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index b970992..828ef54 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -37,7 +37,7 @@ jobs: run: python -m build - name: Install package - run: pip install dist/*.whl + run: pip install dist/*.whl --break-system-packages - name: Verify Coq and opam versions run: | From 1e5c565b5d27be4458cb7d9ad4c8074d04f6f9c8 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 00:18:56 -0600 Subject: [PATCH 16/22] Added instructions for coq installation --- .github/workflows/github-build-actions.yaml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 828ef54..94ba021 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -39,12 +39,24 @@ jobs: - name: Install package run: pip install dist/*.whl --break-system-packages + - name: Check opam version + run: opam --version + + - name: Install Coq + run: | + opam switch create simple_grp_theory 4.14.2 + opam switch simple_grp_theory + eval $(opam env) + opam repo add coq-released https://coq.inria.fr/opam/released + opam pin add -y coq 8.18.0 + opam pin add -y coq-lsp 0.1.8+8.18 + - name: Verify Coq and opam versions run: | - echo "Coq version:" - coqc --version echo "opam version:" opam --version + echo "Coq version:" + coqc --version # - name: Install opam and OCaml # run: | From 3aee74dffdf8249cec80f14a4113823a6c01bebf Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 00:22:16 -0600 Subject: [PATCH 17/22] Added opam init --- .github/workflows/github-build-actions.yaml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 94ba021..a2a4471 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -39,8 +39,10 @@ jobs: - name: Install package run: pip install dist/*.whl --break-system-packages - - name: Check opam version - run: opam --version + - name: Check and Init opam version + run: | + opam --version + opam init - name: Install Coq run: | From 6aaddef278ed6a4e46b967fa07b729631c1e9476 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 00:25:44 -0600 Subject: [PATCH 18/22] Disabled sandboxing and added accepting conditions. --- .github/workflows/github-build-actions.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index a2a4471..97f3801 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -42,7 +42,7 @@ jobs: - name: Check and Init opam version run: | opam --version - opam init + opam init --disable-sandboxing --yes - name: Install Coq run: | From 8041aff78827fd4e84142b4306b1951d34562218 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 01:06:34 -0600 Subject: [PATCH 19/22] removed coq installation --- .github/workflows/github-build-actions.yaml | 25 --------------------- 1 file changed, 25 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 97f3801..d0db748 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -50,33 +50,8 @@ jobs: opam switch simple_grp_theory eval $(opam env) opam repo add coq-released https://coq.inria.fr/opam/released - opam pin add -y coq 8.18.0 opam pin add -y coq-lsp 0.1.8+8.18 - - name: Verify Coq and opam versions - run: | - echo "opam version:" - opam --version - echo "Coq version:" - coqc --version - - # - name: Install opam and OCaml - # run: | - # sudo apt-get update - # sudo apt-get install -y build-essential unzip bubblewrap - # # Install opam non-interactively by piping the default answer - # printf "/usr/local/bin\n" | sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) - # # Initialize opam (disable sandboxing for CI) - # opam init --disable-sandboxing --yes - # # Check if the "default" switch exists; if not, create it. - # if opam switch list --short | grep -q "^default$"; then - # echo "Switch 'default' already exists, using it." - # else - # opam switch create default ocaml-base-compiler.4.14.0 --yes - # fi - # # Update the current shell's environment with the default switch - # eval $(opam env --switch=default) - - name: Install Lean (elan) run: | # Install elan, the Lean version manager From 4eea768bc8b982e3c8194de7bdfb43660b139536 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 01:25:06 -0600 Subject: [PATCH 20/22] Fixed root github build action --- .github/workflows/github-build-actions.yaml | 23 +++++++++++---------- README.md | 1 - src/test/simple_env_test.py | 1 - 3 files changed, 12 insertions(+), 13 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index d0db748..42248ea 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -10,14 +10,14 @@ jobs: build-test: runs-on: ubuntu-latest container: - image: coqorg/coq:8.18.0-ocaml-4.14.2-flambda # or use coqcommunity/docker-coq:latest - options: --user 0 # Run as root to install dependencies + image: coqorg/coq:8.18.0-ocaml-4.14.2-flambda + options: --user 0 # Running as root; no sudo needed steps: - name: Checkout repository uses: actions/checkout@v3 with: - submodules: true # This ensures that all submodules are also checked out + submodules: true # Ensure submodules are checked out - name: Install Python and pip run: | @@ -53,29 +53,30 @@ jobs: opam pin add -y coq-lsp 0.1.8+8.18 - name: Install Lean (elan) + shell: bash run: | - # Install elan, the Lean version manager + export HOME=/root curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y - # Source the Lean environment so that lean is on the PATH - source $HOME/.elan/env + source /root/.elan/env - name: Prepare Lean REPL + shell: bash run: | - source $HOME/.elan/env - # Run the project script to prepare the Lean REPL + source /root/.elan/env install-lean-repl - name: Build Lean REPL for itp-interface + shell: bash run: | - source $HOME/.elan/env + source /root/.elan/env install-itp-interface - name: List repository files (debug step) run: find . -type f - name: Run tests + shell: bash run: | - # Load environments before running tests eval $(opam env) - source $HOME/.elan/env + source /root/.elan/env python src/test/simple_env_test.py \ No newline at end of file diff --git a/README.md b/README.md index 9215122..ee1c034 100644 --- a/README.md +++ b/README.md @@ -141,7 +141,6 @@ if os.system("opam switch simple_grp_theory") != 0: 'opam switch simple_grp_theory', 'eval $(opam env)', 'opam repo add coq-released https://coq.inria.fr/opam/released', - 'opam pin add -y coq 8.18.0', 'opam pin add -y coq-lsp 0.1.8+8.18' ] final_cmd = ' && '.join(cmds) diff --git a/src/test/simple_env_test.py b/src/test/simple_env_test.py index bfc24bf..b4e9c92 100644 --- a/src/test/simple_env_test.py +++ b/src/test/simple_env_test.py @@ -28,7 +28,6 @@ def build_coq_project(self, project_folder): 'opam switch simple_grp_theory', 'eval $(opam env)', 'opam repo add coq-released https://coq.inria.fr/opam/released', - 'opam pin add -y coq 8.18.0', 'opam pin add -y coq-lsp 0.1.8+8.18' ] final_cmd = ' && '.join(cmds) From 0ca3b4787bd65aaf68708d296f34a2ec45f8d9c4 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 01:48:08 -0600 Subject: [PATCH 21/22] Fixed installation script. --- src/itp_interface/main/install.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/itp_interface/main/install.py b/src/itp_interface/main/install.py index 1cca885..d52c5fd 100644 --- a/src/itp_interface/main/install.py +++ b/src/itp_interface/main/install.py @@ -57,7 +57,7 @@ def install_lean_repl(): break # Make sure that .elan is installed print("Checking if .elan is installed") - if os.path.exists(os.path.expanduser("~/.elan")): + if os.system("elan --version") == 0: print("[OK] .elan is installed") else: print("Installing .elan") From ce361faed74d53aee9d3729a5b7f7a3aab042b73 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 02:13:16 -0600 Subject: [PATCH 22/22] Added home. --- .github/workflows/github-build-actions.yaml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 42248ea..07fb70d 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.github/workflows/github-build-actions.yaml @@ -12,6 +12,8 @@ jobs: container: image: coqorg/coq:8.18.0-ocaml-4.14.2-flambda options: --user 0 # Running as root; no sudo needed + env: + HOME: /root steps: - name: Checkout repository @@ -55,20 +57,19 @@ jobs: - name: Install Lean (elan) shell: bash run: | - export HOME=/root curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y - source /root/.elan/env + source $HOME/.elan/env - name: Prepare Lean REPL shell: bash run: | - source /root/.elan/env + source $HOME/.elan/env install-lean-repl - name: Build Lean REPL for itp-interface shell: bash run: | - source /root/.elan/env + source $HOME/.elan/env install-itp-interface - name: List repository files (debug step) @@ -78,5 +79,5 @@ jobs: shell: bash run: | eval $(opam env) - source /root/.elan/env + source $HOME/.elan/env python src/test/simple_env_test.py \ No newline at end of file