Skip to content

Commit

Permalink
Commenting out prover application
Browse files Browse the repository at this point in the history
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](actions/checkout#956)
Trying 1001 instead of root first
Upgraded checkout action
Added job names
Fixed test target
Removed user option
  • Loading branch information
thierrymarianne committed Feb 15, 2024
1 parent 40e2316 commit 6d5cc2f
Show file tree
Hide file tree
Showing 7 changed files with 40 additions and 20 deletions.
2 changes: 1 addition & 1 deletion .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": {
}
}
42 changes: 30 additions & 12 deletions .github/workflows/continuous-integration.yaml
Expand Up @@ -3,7 +3,7 @@ name: Apply ATP prover on FOF files
on:
push:
tags:
- atp-lptp-v*.*.*
- v*.*.*
pull_request:
branches:
- '*'
Expand All @@ -12,6 +12,8 @@ jobs:
release:
runs-on: ubuntu-latest

name: Create release

steps:
- name: Set env
run: |
Expand Down Expand Up @@ -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:
Expand All @@ -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
Expand All @@ -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'
2 changes: 1 addition & 1 deletion .github/workflows/release/build-archive.sh
Expand Up @@ -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 \
Expand Down
4 changes: 2 additions & 2 deletions .github/workflows/release/publish-archive.sh
Expand Up @@ -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}"
Expand All @@ -53,4 +53,4 @@ function publish() {
"${upload_url}?name=${archive_name}.sha256sum"
}

publish './'"${RELEASE_NAME}"
publish '/usr/local/atp-prolog-verification/'"${RELEASE_NAME}"
4 changes: 2 additions & 2 deletions 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 <thierry.marianne@univ-reunion.fr>"

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 \
./ \
Expand Down
2 changes: 2 additions & 0 deletions 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
Expand Down
4 changes: 2 additions & 2 deletions etc/docker-compose.yaml
Expand Up @@ -10,14 +10,14 @@ 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
retries: 3
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'

0 comments on commit 6d5cc2f

Please sign in to comment.