diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index eaacac9..1290355 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -3,7 +3,7 @@ name: Docker CI on: push: branches: - - master + - v8.18 pull_request: branches: - '**' @@ -15,7 +15,7 @@ jobs: strategy: matrix: image: - - 'coqorg/coq:dev' + - 'coqorg/coq:8.18' fail-fast: false steps: - uses: actions/checkout@v3 diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml deleted file mode 100644 index 25264ba..0000000 --- a/.github/workflows/nix-action.yml +++ /dev/null @@ -1,47 +0,0 @@ -# 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: Nix CI - -on: - push: - branches: - - master - pull_request: - paths: - - .github/workflows/** - pull_request_target: - -jobs: - build: - runs-on: ubuntu-latest - strategy: - matrix: - overrides: - - 'coq = "master"' - fail-fast: false - steps: - - name: Determine which commit to test - run: | - if [[ ${{ github.event_name }} =~ "pull_request" ]]; then - merge_commit=$(git ls-remote ${{ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge | cut -f1) - if [ -z "$merge_commit" ]; then - echo "tested_commit=${{ github.event.pull_request.head.sha }}" >> $GITHUB_ENV - else - echo "tested_commit=$merge_commit" >> $GITHUB_ENV - fi - else - echo "tested_commit=${{ github.sha }}" >> $GITHUB_ENV - fi - - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - uses: cachix/cachix-action@v12 - with: - name: coq-community - authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - extraPullNames: coq, math-comp - - uses: actions/checkout@v3 - with: - ref: ${{ env.tested_commit }} - - run: > - nix-build https://coq.inria.fr/nix/toolbox --argstr job stalmarck --arg override '{ ${{ matrix.overrides }}; stalmarck = builtins.filterSource (path: _: baseNameOf path != ".git") ./.; }' diff --git a/README.md b/README.md index 2e5b370..26ba8f4 100644 --- a/README.md +++ b/README.md @@ -5,18 +5,14 @@ Follow the instructions on https://github.com/coq-community/templates to regener # Stalmarck [![Docker CI][docker-action-shield]][docker-action-link] -[![Nix CI][nix-action-shield]][nix-action-link] [![Contributing][contributing-shield]][contributing-link] [![Code of Conduct][conduct-shield]][conduct-link] [![Zulip][zulip-shield]][zulip-link] [![DOI][doi-shield]][doi-link] -[docker-action-shield]: https://github.com/coq-community/stalmarck/workflows/Docker%20CI/badge.svg?branch=master +[docker-action-shield]: https://github.com/coq-community/stalmarck/workflows/Docker%20CI/badge.svg?branch=v8.18 [docker-action-link]: https://github.com/coq-community/stalmarck/actions?query=workflow:"Docker%20CI" -[nix-action-shield]: https://github.com/coq-community/stalmarck/workflows/Nix%20CI/badge.svg?branch=master -[nix-action-link]: https://github.com/coq-community/stalmarck/actions?query=workflow:"Nix%20CI" - [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md @@ -41,7 +37,7 @@ algorithm in Coq. - Coq-community maintainer(s): - Karl Palmskog ([**@palmskog**](https://github.com/palmskog)) - License: [GNU Lesser General Public License v2.1 or later](LICENSE) -- Compatible Coq versions: Coq master (use the corresponding branch or release for other Coq versions) +- Compatible Coq versions: 8.18 (use the corresponding branch or release for other Coq versions) - Additional dependencies: none - Coq namespace: `Stalmarck.Algorithm` - Related publication(s): diff --git a/coq-stalmarck-tactic.opam b/coq-stalmarck-tactic.opam index bd80662..8cc6646 100644 --- a/coq-stalmarck-tactic.opam +++ b/coq-stalmarck-tactic.opam @@ -13,7 +13,7 @@ build: ["dune" "build" "-p" name "-j" jobs] depends: [ "ocaml" {>= "4.09.0"} "dune" {>= "2.8"} - "coq" {= "dev"} + "coq" {>= "8.18" & < "8.19"} "coq-stalmarck" {= version} ] diff --git a/coq-stalmarck.opam b/coq-stalmarck.opam index ef29c4a..b78e2c6 100644 --- a/coq-stalmarck.opam +++ b/coq-stalmarck.opam @@ -18,7 +18,7 @@ algorithm in Coq.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {= "dev"} + "coq" {>= "8.18" & < "8.19"} ] tags: [ diff --git a/meta.yml b/meta.yml index b8dfd26..3f1f38c 100644 --- a/meta.yml +++ b/meta.yml @@ -4,10 +4,9 @@ shortname: stalmarck organization: coq-community community: true action: true -nix: true doi: 10.1007/3-540-44659-1_24 plugin: true -branch: master +branch: 'v8.18' dune: false synopsis: Verified implementation of Stålmarck's algorithm for proving tautologies in Coq @@ -40,11 +39,11 @@ license: identifier: LGPL-2.1-or-later supported_coq_versions: - text: Coq master (use the corresponding branch or release for other Coq versions) - opam: '{= "dev"}' + text: 8.18 (use the corresponding branch or release for other Coq versions) + opam: '{>= "8.18" & < "8.19"}' tested_coq_nix_versions: -- coq_version: 'master' +- coq_version: '8.18' tested_coq_opam_versions: - version: 'dev'