diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml
new file mode 100644
index 0000000..07fb70d
--- /dev/null
+++ b/.github/workflows/github-build-actions.yaml
@@ -0,0 +1,83 @@
+name: Build, Package, and Test
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+jobs:
+  build-test:
+    runs-on: ubuntu-latest
+    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
+        uses: actions/checkout@v3
+        with:
+          submodules: true  # Ensure submodules are checked out
+
+      - 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
+
+      - name: Upgrade pip and install build tool
+        run: |
+          python -m pip install --upgrade pip --break-system-packages
+          pip install build --break-system-packages
+
+      - name: Build package
+        run: python -m build
+
+      - name: Install package
+        run: pip install dist/*.whl --break-system-packages
+
+      - name: Check and Init opam version
+        run: |
+          opam --version
+          opam init --disable-sandboxing --yes
+      
+      - 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-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
+
+      - name: Run tests
+        shell: bash
+        run: |
+          eval $(opam env)
+          source $HOME/.elan/env
+          python src/test/simple_env_test.py
\ No newline at end of file
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/.github/workflows/github-publish-actions.yaml b/.github/workflows/github-publish-actions.yaml
new file mode 100644
index 0000000..818ee6c
--- /dev/null
+++ b/.github/workflows/github-publish-actions.yaml
@@ -0,0 +1,38 @@
+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 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
+        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.
diff --git a/README.md b/README.md
index 80abe48..ee1c034 100644
--- a/README.md
+++ b/README.md
@@ -137,11 +137,10 @@ 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',
-        '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/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",
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")
diff --git a/src/test/simpl_env_test.py b/src/test/simple_env_test.py
similarity index 98%
rename from src/test/simpl_env_test.py
rename to src/test/simple_env_test.py
index 03abd04..b4e9c92 100644
--- a/src/test/simpl_env_test.py
+++ b/src/test/simple_env_test.py
@@ -21,14 +21,13 @@ 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',
-                'opam pin add -y coq 8.18.0',
                 'opam pin add -y coq-lsp 0.1.8+8.18'
             ]
             final_cmd = ' && '.join(cmds)