From bc7a5f1ba20427848bdedfd8c316a5f48f87b94f Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Tue, 16 Sep 2025 07:22:27 +0200 Subject: [PATCH] ci: Switch to Github Actions --- .circleci/config.yml | 94 --------------------------- .github/workflows/build-with-make.yml | 38 +++++++++++ .github/workflows/docker-action.yml | 50 ++++++++++++++ meta.yml | 17 +++++ 4 files changed, 105 insertions(+), 94 deletions(-) delete mode 100644 .circleci/config.yml create mode 100644 .github/workflows/build-with-make.yml create mode 100644 .github/workflows/docker-action.yml create mode 100644 meta.yml diff --git a/.circleci/config.yml b/.circleci/config.yml deleted file mode 100644 index e43d40c5..00000000 --- a/.circleci/config.yml +++ /dev/null @@ -1,94 +0,0 @@ -version: 2.1 - -commands: - setup: - steps: - - checkout - - run: - name: Configure environment - command: echo . ~/.profile >> $BASH_ENV - - run: - name: Install dependencies - command: | - opam repo -a add coq-extra-dev https://coq.inria.fr/opam/extra-dev - opam update - opam pin remove dune -n - opam install --deps-only . - - run: - name: List installed packages - command: opam list - -defaults: &defaults - environment: - OPAMBESTEFFORT: true - OPAMJOBS: 2 - OPAMVERBOSE: 1 - OPAMWITHTEST: true - OPAMYES: true - TERM: xterm - resource_class: medium - steps: - - setup - - run: - name: Build, test, and install package - command: opam install . - - run: - name: Uninstall package - command: opam remove . - -jobs: - test: - parameters: - coq: - type: string - docker: - - image: <> - <<: *defaults - - test-with-make: - parameters: - coq: - type: string - docker: - - image: <> - <<: *defaults - steps: - - setup - - run: - name: Build, test - command: make all - - run: - name: Clean - command: make clean - -workflows: - version: 2 - build: - jobs: - - test: - name: "Coq 8.14" - coq: "coqorg/coq:8.14" - - test: - name: "Coq 8.15" - coq: "coqorg/coq:8.15" - - test: - name: "Coq 8.16" - coq: "coqorg/coq:8.16" - - test: - name: "Coq 8.17" - coq: "coqorg/coq:8.17" - - test: - name: "Coq 8.18" - coq: "coqorg/coq:8.18" - - test: - name: "Coq 8.19" - coq: "coqorg/coq:8.19" - - test: - name: "Coq 8.20" - coq: "coqorg/coq:8.20" - - test: - name: "Coq dev" - coq: "rocq/rocq-prover:dev-ocaml-4.13-flambda" - - test-with-make: - name: "Coq 8.17 + make" - coq: "coqorg/coq:8.17" diff --git a/.github/workflows/build-with-make.yml b/.github/workflows/build-with-make.yml new file mode 100644 index 00000000..c671f950 --- /dev/null +++ b/.github/workflows/build-with-make.yml @@ -0,0 +1,38 @@ +name: Build with Make + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + build-with-make: + # the OS must be GNU/Linux to be able to use the docker-coq-action + runs-on: ubuntu-latest + strategy: + matrix: + image: + - 'coqorg/coq:8.20' + fail-fast: false + steps: + - uses: actions/checkout@v4 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-itree.opam' + custom_image: ${{ matrix.image }} + before_script: | + startGroup "Workaround permission issue" + sudo chown -R 1000:1000 . + endGroup + script: | + startGroup "Build" + make all + make install + endGroup + after_script: | + startGroup "Clean" + make clean + endGroup diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 00000000..c0c1ea85 --- /dev/null +++ b/.github/workflows/docker-action.yml @@ -0,0 +1,50 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +name: Docker CI + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + build: + # the OS must be GNU/Linux to be able to use the docker-coq-action + runs-on: ubuntu-latest + strategy: + matrix: + image: + - 'coqorg/coq:8.14' + - 'coqorg/coq:8.15' + - 'coqorg/coq:8.16' + - 'coqorg/coq:8.17' + - 'coqorg/coq:8.18' + - 'coqorg/coq:8.19' + - 'coqorg/coq:8.20' + - 'rocq/rocq-prover:9.0' + - 'rocq/rocq-prover:dev' + fail-fast: false + steps: + - uses: actions/checkout@v4 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-itree.opam' + custom_image: ${{ matrix.image }} + after_script: | + startGroup "Test dependants" + PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,) + PACKAGES=`opam list -s --depends-on coq-itree --coinstallable-with $PINS` + for PACKAGE in $PACKAGES + do DEPS_FAILED=false + opam install -y --deps-only $PACKAGE || DEPS_FAILED=true + [ $DEPS_FAILED == true ] || opam install -t $PACKAGE + done + endGroup + + +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/meta.yml b/meta.yml new file mode 100644 index 00000000..0b81fee9 --- /dev/null +++ b/meta.yml @@ -0,0 +1,17 @@ +fullname: Interaction Trees +shortname: itree +organization: DeepSpec +action: true +ci_test_dependants: true +dune: true +tested_coq_opam_versions: +- version: '8.14' +- version: '8.15' +- version: '8.16' +- version: '8.17' +- version: '8.18' +- version: '8.19' +- version: '8.20' +tested_rocq_opam_versions: +- version: '9.0' +- version: 'dev'