Skip to content

Commit

Permalink
Simplify the test-suite infrastructure in CI
Browse files Browse the repository at this point in the history
  • Loading branch information
pi8027 committed May 28, 2024
1 parent 0132827 commit c77ff3d
Show file tree
Hide file tree
Showing 3 changed files with 12 additions and 11 deletions.
16 changes: 5 additions & 11 deletions .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
# This file was generated from `meta.yml` using the coq-community templates and
# then patched to support the test-suite. Be careful when regenerate it.
# 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:
Expand Down Expand Up @@ -38,15 +38,9 @@ jobs:
with:
opam_file: 'coq-mathcomp-zify.opam'
custom_image: ${{ matrix.image }}
after_script: |
startGroup "Run tests"
sudo chown -R coq:coq .
make test-suite TEST_SKIP_BUILD=1
endGroup
- name: Revert permissions
if: ${{ always() }}
run: sudo chown -R 1001:116 .

export: 'OPAMWITHTEST'
env:
OPAMWITHTEST: true

# See also:
# https://github.com/coq-community/docker-coq-action#readme
Expand Down
1 change: 1 addition & 0 deletions coq-mathcomp-zify.opam
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ for goals stated with the definitions of the Mathematical Components library
by extending the zify tactic."""

build: [make "-j%{jobs}%"]
run-test: [make "-j%{jobs}%" "test-suite"]
install: [make "install"]
depends: [
"coq" {>= "8.16"}
Expand Down
6 changes: 6 additions & 0 deletions meta.yml
Original file line number Diff line number Diff line change
Expand Up @@ -71,8 +71,14 @@ dependencies:
description: |-
[MathComp](https://math-comp.github.io) algebra
test_target: test-suite
namespace: mathcomp.zify

action_appendix: |2-
export: 'OPAMWITHTEST'
env:
OPAMWITHTEST: true
documentation: |-
## File contents
Expand Down

0 comments on commit c77ff3d

Please sign in to comment.