Skip to content

Commit 8579d10

Browse files
authored
Use opam tests for Rocq 9.0 (#205)
1 parent f2daf2b commit 8579d10

1 file changed

Lines changed: 2 additions & 8 deletions

File tree

.github/workflows/docker-action.yml

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -25,16 +25,13 @@ jobs:
2525
custom_image: ${{ matrix.image }}
2626
custom_script: |
2727
{{before_install}}
28-
# Ensure the current user owns the workspace
29-
sudo chown -R $(whoami) /github/workspace
30-
3128
startGroup "Build coq-hammer-tactics dependencies"
3229
opam pin add -n -y -k path coq-hammer-tactics .
3330
opam update -y
3431
opam install -y -j $(nproc) coq-hammer-tactics --deps-only
3532
endGroup
3633
startGroup "Build coq-hammer-tactics"
37-
opam install -y -v -j $(nproc) coq-hammer-tactics
34+
opam install -y -v -j $(nproc) coq-hammer-tactics --with-test
3835
opam list
3936
endGroup
4037
startGroup "Build coq-hammer dependencies"
@@ -43,12 +40,9 @@ jobs:
4340
opam install -y -j $(nproc) coq-hammer --deps-only
4441
endGroup
4542
startGroup "Build coq-hammer"
46-
opam install -y -v -j $(nproc) coq-hammer
43+
opam install -y -v -j $(nproc) coq-hammer --with-test
4744
opam list
4845
endGroup
49-
startGroup "Tactics test"
50-
make quicktest
51-
endGroup
5246
startGroup "Uninstallation test"
5347
opam remove -y coq-hammer
5448
opam remove -y coq-hammer-tactics

0 commit comments

Comments
 (0)