From 6d5cc2fd6ec207254d078858fd9721f0f857c69f Mon Sep 17 00:00:00 2001 From: Thierry Marianne Date: Thu, 15 Feb 2024 01:54:25 +0100 Subject: [PATCH] Commenting out prover application Revised paths Fixed reference format Try fixing env var injection Injecting GitHub secret into container Added visual help Injecting workspace path Fixed path to workspace Tried fixing permission issue Added continuous integration status badge Run tests continuously Run as root user Downgrading [checkout](https://github.com/actions/checkout/issues/956) Trying 1001 instead of root first Upgraded checkout action Added job names Fixed test target Removed user option --- .devcontainer/devcontainer.json | 2 +- .github/workflows/continuous-integration.yaml | 42 +++++++++++++------ .github/workflows/release/build-archive.sh | 2 +- .github/workflows/release/publish-archive.sh | 4 +- Dockerfile | 4 +- README.md | 2 + etc/docker-compose.yaml | 4 +- 7 files changed, 40 insertions(+), 20 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 54b698f..4a1cabc 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,5 +1,5 @@ { - "image": "ghcr.io/thierrymarianne/automated-theorem-proving-for-prolog-verification:latest", + "image": "ghcr.io/atp-lptp/automated-theorem-proving-for-prolog-verification:latest", "features": { } } diff --git a/.github/workflows/continuous-integration.yaml b/.github/workflows/continuous-integration.yaml index 2e2024f..9f3e2a9 100644 --- a/.github/workflows/continuous-integration.yaml +++ b/.github/workflows/continuous-integration.yaml @@ -3,7 +3,7 @@ name: Apply ATP prover on FOF files on: push: tags: - - atp-lptp-v*.*.* + - v*.*.* pull_request: branches: - '*' @@ -12,6 +12,8 @@ jobs: release: runs-on: ubuntu-latest + name: Create release + steps: - name: Set env run: | @@ -76,6 +78,8 @@ jobs: build-fof_apply-provers: needs: push_to_registry + name: Build FOF files, apply provers, parse results + runs-on: ubuntu-latest defaults: run: @@ -86,20 +90,32 @@ jobs: credentials: username: ${{ github.actor }} password: ${{ secrets.github_token }} + volumes: + - ${{ github.workspace }}:/workspace options: --cpus 2 env: RELEASE_NAME: ${{ needs.push_to_registry.outputs.release_name }} + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} steps: + - name: Check out the repo + uses: actions/checkout@v4.1.1 + with: + ref: ${{ github.event.pull_request.head.sha }} + + - name: Run tests + working-directory: /usr/local/atp-prolog-verification + run: make test + - name: Make FOF files working-directory: /usr/local/atp-prolog-verification run: | echo 'release '$RELEASE_NAME make build-fof-for-each-program - #- name: Applying provers on FOF files for all programs available in ./src - # working-directory: /usr/local/atp-prolog-verification - # run: make apply-provers-for-each-program + ## - name: Applying provers on FOF files for all programs available in ./src + ## working-directory: /usr/local/atp-prolog-verification + ## run: make apply-provers-for-each-program - name: Parse results working-directory: /usr/local/atp-prolog-verification @@ -111,18 +127,20 @@ jobs: - name: Archive FOF files, results working-directory: /usr/local/atp-prolog-verification - env: - RELEASE_NAME: ${{ env.RELEASE_NAME }} - run: /bin/bash -c '. .github/workflows/release/build-archive.sh' + run: | + echo 'release '$RELEASE_NAME + RELEASE_NAME=$RELEASE_NAME /bin/bash -c '. .github/workflows/release/build-archive.sh' + cp /usr/local/atp-prolog-verification/$RELEASE_NAME /workspace/$RELEASE_NAME - uses: actions/upload-artifact@main with: path: | - /usr/local/atp-prolog-verification/$RELEASE_NAME + ${{ github.workspace }}/$RELEASE_NAME - name: Publish release working-directory: /usr/local/atp-prolog-verification - run: /bin/bash -c '. ./.github/workflows/release/publish-archive.sh' - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - RELEASE_NAME: $RELEASE_NAME + run: | + echo 'release '$RELEASE_NAME + GITHUB_TOKEN=$GITHUB_TOKEN \ + RELEASE_NAME=$RELEASE_NAME \ + /bin/bash -c '. ./.github/workflows/release/publish-archive.sh' diff --git a/.github/workflows/release/build-archive.sh b/.github/workflows/release/build-archive.sh index 9a07066..94db538 100644 --- a/.github/workflows/release/build-archive.sh +++ b/.github/workflows/release/build-archive.sh @@ -2,7 +2,7 @@ function build() { tar cvzf \ - '/usr/local/atp-prolog-verification/'$RELEASE_NAME'.tar.gz' \ + '/usr/local/atp-prolog-verification/'$RELEASE_NAME \ './out/'*.out \ './out/'results.* \ './src/'*/*.fof \ diff --git a/.github/workflows/release/publish-archive.sh b/.github/workflows/release/publish-archive.sh index ee4f5ad..c9916d2 100644 --- a/.github/workflows/release/publish-archive.sh +++ b/.github/workflows/release/publish-archive.sh @@ -40,7 +40,7 @@ function publish() { curl \ -X POST \ - --data-binary @"${result}" \ + --data-binary @"${results}" \ -H 'Content-Type: application/octet-stream' \ -H "Authorization: Bearer ${GITHUB_TOKEN}" \ "${upload_url}?name=${archive_name}" @@ -53,4 +53,4 @@ function publish() { "${upload_url}?name=${archive_name}.sha256sum" } -publish './'"${RELEASE_NAME}" +publish '/usr/local/atp-prolog-verification/'"${RELEASE_NAME}" diff --git a/Dockerfile b/Dockerfile index 5d04b24..4fac2d1 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,8 +1,8 @@ -FROM ghcr.io/thierrymarianne/automated-theorem-proving-for-prolog-verification:base +FROM ghcr.io/atp-lptp/automated-theorem-proving-for-prolog-verification:base LABEL maintainer="Thierry Marianne " -LABEL org.opencontainers.image.source="https://github.com/thierrymarianne/automated-theorem-proving-for-prolog-verification" +LABEL org.opencontainers.image.source="https://github.com/atp-lptp/automated-theorem-proving-for-prolog-verification" COPY --chown=1000:1000 \ ./ \ diff --git a/README.md b/README.md index 9e21aeb..9b03cbb 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,7 @@ # Automated Theorem Proving for Prolog Verification +[![Apply ATP prover on FOF files](https://github.com/atp-lptp/automated-theorem-proving-for-prolog-verification/actions/workflows/continuous-integration.yaml/badge.svg)](https://github.com/atp-lptp/automated-theorem-proving-for-prolog-verification/actions/workflows/continuous-integration.yaml) + [Automated Theorem Proving for Prolog Verification [PDF]](ATP-for-LP-Verif.pdf) ## Build FOF files diff --git a/etc/docker-compose.yaml b/etc/docker-compose.yaml index 20bd5dc..4689a81 100644 --- a/etc/docker-compose.yaml +++ b/etc/docker-compose.yaml @@ -10,7 +10,7 @@ services: - OWNER_UID=${PROGRAM_OWNER_UID:-1000} - OWNER_GID=${PROGRAM_OWNER_GID:-1000} tags: - - "ghcr.io/thierrymarianne/automated-theorem-proving-for-prolog-verification:base" + - "ghcr.io/atp-lptp/automated-theorem-proving-for-prolog-verification:base" healthcheck: interval: 30s timeout: 10s @@ -18,6 +18,6 @@ services: start_period: 1m test: ["CMD", "/bin/bash", "-c", "( test $(ps ax | grep -E 'tini' -c) -gt 0 )"] labels: - org.opencontainers.image.source: 'https://github.com/thierrymarianne/automated-theorem-proving-for-prolog-verification' + org.opencontainers.image.source: 'https://github.com/atp-lptp/automated-theorem-proving-for-prolog-verification' restart: 'always' platform: 'linux/amd64'