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](actions/checkout#956)
Trying 1001 instead of root first
Upgraded checkout action
Added job names
Fixed test target
Removed user option
Align file owner uid / gid
Removed test detecting missing FR locale from container

.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": {
   }
 }

.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 }}
-      options: --cpus 2
+      volumes:
+        - ${{ github.workspace }}:/workspace
+      options: --cpus 2 --user 1001
       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'

.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 \

.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}"

Dockerfile

@@ -1,10 +1,10 @@
-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 \
+COPY        --chown=1001:1001 \
             ./ \
             /usr/local/atp-prolog-verification
 
@@ -23,6 +23,6 @@ RUN         apt update \
             --no-install-recommends && \
             /bin/bash -c 'cd /usr/local/atp-prolog-verification && make help'
 
-USER        1000:1000
+USER        1001:1001
 
 WORKDIR     /usr/local/atp-prolog-verification

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 

bin/print.sh

@@ -226,7 +226,6 @@ LaTeX
 # actual="$(print_utf8 '%.0f' '45.4')";expected="45";message='print_utf8'
 # actual="$(print_utf8 '%.0f' '45.5')";expected="46";message='print_utf8'
 # actual="$(print_utf8 '%.0f' '45')";expected="45";message='print_utf8'
-# actual="$(PRINT_LOCALE='fr_FR.UTF-8' print_utf8 '%.0f' '45.7' 2>&1 | grep 'invalid number' -c)";expected="1";message='print_utf8'
 # ```
 #
 # See also [printf command](https://www.ibm.com/docs/en/aix/7.2?topic=p-printf-command)

etc/docker-compose.yaml

@@ -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'