Skip to content

Refactoring of the category theory example + removing plan B #1063

Refactoring of the category theory example + removing plan B

Refactoring of the category theory example + removing plan B #1063

Workflow file for this run

# This is a basic workflow to help you get started with Actions
name: docker CI
# Controls when the action will run. Triggers the workflow on push or pull request
# events but only for the master branch
on:
push:
branches: [ master ]
tags: [ "v*.*.*" ]
pull_request:
branches: [ master ]
jobs:
opam:
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
coq_version:
- '8.16'
- '8.17'
- '8.18'
steps:
- uses: actions/checkout@v2
- uses: coq-community/docker-coq-action@v1
with:
opam_file: './coq-hierarchy-builder.opam'
coq_version: ${{ matrix.coq_version }}
export: 'OPAMWITHTEST' # space-separated list of variables
env:
OPAMWITHTEST: 'true'
plan-B:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- uses: coq-community/docker-coq-action@v1
with:
opam_file: './coq-hierarchy-builder.opam'
coq_version: '8.16'
ocaml_version: '4.09-flambda'
script: |
mkdir /home/coq/workspace
cp -ra . /home/coq/workspace
cd /home/coq/workspace
opam install ./coq-hierarchy-builder.opam
sed -i.bak -e "s/-Q . HB//" -e "s|tests/factory_sort_tac.v||" _CoqProject.test-suite
# This is what a user does to cut HB loose
export COQ_ELPI_ATTRIBUTES="hb(log(raw))"
make test-suite -j2
wc -l `find . -name \*.v`
coq.hb patch `find . -name \*.v`
wc -l `find . -name \*.v`
if git diff --quiet; then echo "No patch!"; exit 1; fi
make clean
opam remove coq-hierarchy-builder
opam install ./coq-hierarchy-builder-shim.opam
# Does it work?
make test-suite -j2
# We also test the reset facility works (we rebuild hb locally)
make coq.hb
./coq.hb reset `find . -name \*.v`
mv _CoqProject.test-suite.bak _CoqProject.test-suite
git diff --exit-code
release:
runs-on: ubuntu-latest
if: startsWith(github.ref, 'refs/tags/')
needs: [opam]
steps:
- name: Checkout
uses: actions/checkout@v3
- name: Inject slug/short variables
uses: rlespinasse/github-slug-action@v4
- name: Create archive
run: |
VERSION="${GITHUB_REF_NAME_SLUG#v}"
git archive -o hierarchy-builder-$VERSION.tar.gz --prefix=hierarchy-builder-$VERSION/ $GITHUB_SHA .
- name: Release
uses: softprops/action-gh-release@v1
with:
files: hierarchy-builder-*.tar.gz
fail_on_unmatched_files: true
prerelease: true
generate_release_notes: true
name: Hierarchy Builder ${{ github.ref }}
- name: Use OCaml 4.14.x
uses: avsm/setup-ocaml@v2
with:
ocaml-compiler: 4.14.x
opam-local-packages: |
!coq-hierarchy-builder*.opam
- name: Write PAT
env:
OPAM_PUBLISH_TOKEN: ${{ secrets.OPAM_PUBLISH_TOKEN }}
run: |
mkdir -p ~/.opam/plugins/opam-publish
printf "$OPAM_PUBLISH_TOKEN" > ~/.opam/plugins/opam-publish/coqelpibot.token
- name: Setup SSH
uses: webfactory/[email protected]
with:
ssh-private-key: ${{ secrets.BOT_SSH_KEY }}
- name: Install opam-publish # 2.0.3 because more recent versions do not respect OPAMYES
run: opam install -y -j 2 opam-publish=2.0.3
- name: Publish
run: |
eval $(opam env)
git config --global user.name coqelpibot
git config --global user.email [email protected]
OPAM_SUITE=released
TAG=`git tag --sort=-v:refname|head -1`
opam-publish --tag=$TAG --packages-directory=$OPAM_SUITE/packages --repo=coq/opam --no-browser -v ${TAG##v} https://github.com/math-comp/hierarchy-builder/releases/download/$TAG/hierarchy-builder-${TAG##v}.tar.gz