Skip to content

Commit

Permalink
Drop PL tutorial duplicate work in CI (#3963)
Browse files Browse the repository at this point in the history
Previously, we were doing a lot of repeated work here, and the explicit
clone step is pulling a defunct repository (k-exercises; superseded by
pl-tutorial). We should therefore just drop this step in CI as it's
superseded by other places in the workflow.

Fixes #3962
  • Loading branch information
Baltoli authored Feb 6, 2024
1 parent 2292867 commit 6d630cc
Showing 1 changed file with 0 additions and 20 deletions.
20 changes: 0 additions & 20 deletions .github/workflows/test-pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -66,26 +66,6 @@ jobs:
llvm: 15
- name: 'Build and Test K'
run: docker exec -t k-ci-${GITHUB_SHA} /bin/bash -c 'mvn verify -Dspotless.check.skip=true --batch-mode -U'
- name: 'Check out k-exercises'
uses: actions/checkout@v3
with:
repository: runtimeverification/k-exercises
token: ${{ secrets.JENKINS_GITHUB_PAT }}
submodules: recursive
path: k-exercises
- name: 'Check out pl-tutorial'
uses: actions/checkout@v3
with:
repository: runtimeverification/pl-tutorial
token: ${{ secrets.JENKINS_GITHUB_PAT }}
submodules: recursive
path: k-distribution/pl-tutorial
- name: 'Tutorial Integration Tests'
run: |
docker exec -t k-ci-${GITHUB_SHA} /bin/bash -c 'k-distribution/target/release/k/bin/spawn-kserver kserver.log'
docker exec -t k-ci-${GITHUB_SHA} /bin/bash -c 'cd k-exercises/tutorial && make -j`nproc` --output-sync'
docker exec -t k-ci-${GITHUB_SHA} /bin/bash -c 'cd k-distribution/k-tutorial/1_basic && ./test_kompile.sh'
docker exec -t k-ci-${GITHUB_SHA} /bin/bash -c 'cd k-distribution/k-tutorial/2_intermediate && ./test_kompile.sh'
- name: 'Tear down Docker'
if: always()
run: |
Expand Down

0 comments on commit 6d630cc

Please sign in to comment.