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'