Initial commit

pre-release check
Commenting prover application temporarily for pre-release validation
Fixed LaTeX results making target in continuous integration workflow
Revised container image names
First attempt to produce results archive on pull-request
Declare dependency between release creation and Push docker image
Installing dependencies without interaction
Removed [environment variables setting from job container](https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions\#setting-an-environment-variable)
Write results to ./out directory
Applied custom sort after parsing results
Revised release workflow
Revised working directory
Revised archiving script
Removed left workspace occurrences
Added results to archive
Injecting missing release name into job container
Revise step name
Revise intermediate success rate filename display
Injecting missing release name into job container
Try to avoid [untrusted state](https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands)
Replace slashes with dashes
Trying to replace `marvinpinto/action-automatic-releases@latest` with official action from GitHub
Revise package updates
Removed bash as default shell
Install dependencies on image build
Removed requirements details
Trying to restore container initialization
Revise step title
Revise paths

.devcontainer/devcontainer.json

@@ -0,0 +1,5 @@
+{
+  "image": "ghcr.io/thierrymarianne/automated-theorem-proving-for-prolog-verification:latest",
+  "features": {
+  }
+}

.env.local.dist

@@ -0,0 +1,6 @@
+PROGRAM_OWNER_UID=1000
+PROGRAM_OWNER_GID=1000
+COMPOSE_PROJECT_NAME=atp
+# See [BUILDKIT_PROGRESS](https://docs.docker.com/build/building/env-vars/#buildkit_progress)
+BUILDKIT_PROGRESS=plain
+DOCKER_DEFAULT_PLATFORM=linux/amd64

.github/workflows/continuous-integration.yaml

@@ -0,0 +1,128 @@
+name: Apply ATP prover on FOF files
+
+on:
+  push:
+    tags:
+      - atp-lptp-v*.*.*
+  pull_request:
+    branches:
+      - '*'
+
+jobs:
+  release:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Set env
+        run: |
+          RELEASE_NAME="${GITHUB_REF#refs/*/}"
+          RELEASE_NAME="$(echo $RELEASE_NAME | sed 's/\//-/g')"
+          echo "RELEASE_NAME=${RELEASE_NAME}" >> $GITHUB_ENV
+
+      - name: Create a release
+        uses: "marvinpinto/action-automatic-releases@latest"
+        with:
+          repo_token: ${{ secrets.GITHUB_TOKEN }}
+          prerelease: false
+          automatic_release_tag: ${{ env.RELEASE_NAME }}
+
+  push_to_registry:
+    needs: release
+
+    name: Push Docker image to Container Registry
+    runs-on: ubuntu-latest
+    outputs:
+      docker_image: ${{ steps.meta.outputs.tags }}
+      release_name: ${{ env.RELEASE_NAME }}
+    permissions:
+      packages: write
+      contents: read
+
+    steps:
+      - name: Set env
+        run: | 
+          RELEASE_NAME="${GITHUB_REF#refs/*/}"
+          RELEASE_NAME="$(echo $RELEASE_NAME | sed 's/\//-/g')"
+          echo "RELEASE_NAME=${RELEASE_NAME}" >> $GITHUB_ENV
+          echo "release_name=${RELEASE_NAME}" >> $GITHUB_OUTPUT
+
+      - name: Check out the repo
+        uses: actions/checkout@v4
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
+
+      - name: Log in to the Container registry
+        uses: docker/login-action@343f7c4344506bcbf9b4de18042ae17996df046d
+        with:
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Extract metadata (tags, labels) for Docker
+        id: meta
+        uses: docker/metadata-action@8e5442c4ef9f78752691e2d8f8d19755c6f78e81
+        with:
+          images: |
+            ghcr.io/${{ github.repository }}
+
+      - name: Build and push Docker images
+        uses: docker/build-push-action@4a13e500e55cf31b7a5d59a38ab2040ab0f42f56
+        with:
+          context: .
+          push: true
+          tags: ${{ steps.meta.outputs.tags }}
+          labels: ${{ steps.meta.outputs.labels }}
+
+  build-fof_apply-provers:
+    needs: push_to_registry
+
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        shell: bash
+
+    container:
+      image: ${{ needs.push_to_registry.outputs.docker_image }}
+      credentials:
+        username: ${{ github.actor }}
+        password: ${{ secrets.github_token }}
+      options: --cpus 2
+      env:
+        RELEASE_NAME: ${{ needs.push_to_registry.outputs.release_name }}
+
+    steps:
+      - 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: Parse results
+        working-directory: /usr/local/atp-prolog-verification
+        run: make all-results
+
+      - name: Convert results to LaTeX
+        working-directory: /usr/local/atp-prolog-verification
+        run: make all-results-in-latex
+
+      - 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'
+
+      - uses: actions/upload-artifact@main
+        with:
+          path: |
+            /usr/local/atp-prolog-verification/$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

.github/workflows/release/build-archive.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+function build() {
+  tar cvzf \
+    '/usr/local/atp-prolog-verification/'$RELEASE_NAME'.tar.gz' \
+    './out/'*.out \
+    './out/'results.* \
+    './src/'*/*.fof \
+    && \
+    echo '=> Built ./'$RELEASE_NAME
+}
+build

.github/workflows/release/publish-archive.sh

@@ -0,0 +1,56 @@
+#!/bin/bash
+
+function publish() {
+  local results
+  results="${1}"
+
+  echo "=> About to publish ""${results}"
+
+  if [ ! -e "${results}" ];
+  then
+      echo 'Invalid results ('"${results}"')'
+      return 1
+  fi
+
+  local checksum
+  checksum="$(sha256sum "${results}" | cut -d ' ' -f 1)"
+
+  local base_url
+  base_url='https://api.github.com/repos/'"${GITHUB_REPOSITORY}"
+
+  local upload_url
+  upload_url="$(curl \
+    -H 'Content-Type: application/octet-stream' \
+    -H "Authorization: Bearer ${GITHUB_TOKEN}" \
+    "${base_url}"/releases 2>> /dev/null | \
+    jq -r '.[] | .upload_url' | \
+    head -n1)"
+
+  upload_url=${upload_url/\{?name,label\}/}
+
+  local archive_name
+  archive_name="$(curl \
+    -H 'Content-Type: application/octet-stream' \
+    -H "Authorization: Bearer ${GITHUB_TOKEN}" \
+    "${base_url}"/releases 2>> /dev/null | \
+    jq -r '.[] | .tag_name' | \
+    head -n1).tar.gz"
+
+  echo '=> Archive name is '"${archive_name}"
+
+  curl \
+    -X POST \
+    --data-binary @"${result}" \
+    -H 'Content-Type: application/octet-stream' \
+    -H "Authorization: Bearer ${GITHUB_TOKEN}" \
+    "${upload_url}?name=${archive_name}"
+
+  curl \
+    -X POST \
+    --data "$checksum" \
+    -H 'Content-Type: text/plain' \
+    -H "Authorization: Bearer ${GITHUB_TOKEN}" \
+    "${upload_url}?name=${archive_name}.sha256sum"
+}
+
+publish './'"${RELEASE_NAME}"

.gitignore

@@ -0,0 +1,15 @@
+ATP-LPTP-LaTeX-1/.texpadtmp
+*\.DS_Store
+*\.aux
+*\.dvi
+*\.log
+*\.out
+*\.bbl
+*\.blg
+*\.toc
+*-all*.fof
+*-all.pr
+*-all.pl
+*-all.gr
+tmp_*
+*\.env.local