Skip to content

Added worklow

Added worklow #13

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 # or use coqcommunity/docker-coq:latest
options: --user 0 # Run as root to install dependencies
steps:
- name: Checkout repository
uses: actions/checkout@v3
with:
submodules: true # This ensures that all submodules are also 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
- name: Build package
run: python -m build
- name: Install package
run: pip install dist/*.whl
- name: Verify Coq and opam versions
run: |
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: |
# 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: |
# Load environments before running tests
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_env_test.py