Make LPTP install and check cleanly on today's Prolog systems, and test it on every push

.github/workflows/ci.yml

@@ -0,0 +1,67 @@
+name: CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  proofs:
+    name: proofs (${{ matrix.prolog }})
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        prolog: [swi, gprolog]
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install SWI-Prolog
+        if: matrix.prolog == 'swi'
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends swi-prolog-nox
+
+      - name: Install GNU Prolog
+        if: matrix.prolog == 'gprolog'
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends gprolog
+
+      - name: Check the whole proof corpus
+        run: etc/run-tests.sh ${{ matrix.prolog }}
+
+      - name: Upload generated proofs
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: tmp-${{ matrix.prolog }}
+          path: tmp/
+          if-no-files-found: ignore
+
+  emacs:
+    name: emacs mode
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install Emacs
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends emacs-nox
+
+      - name: Byte-compile and exercise lptp-mode
+        run: |
+          emacs --batch --eval '
+            (progn
+              (unless (byte-compile-file "etc/lptp-mode.el")
+                (error "byte-compilation of etc/lptp-mode.el failed"))
+              (load (expand-file-name "etc/lptp-mode.el"))
+              (find-file "lib/list/list.pr")
+              (lptp-mode)
+              (unless (eq major-mode (quote lptp-mode))
+                (error "lptp-mode did not activate"))
+              ;; Guards against faces that Emacs has since removed.
+              (font-lock-mode 1)
+              (font-lock-ensure)
+              (message "lptp-mode: ok"))'

.gitignore

@@ -4,6 +4,10 @@
 # Editor backups
 *~
 
+# Local configuration: each installation writes its own, holding the
+# absolute path to this directory (see step 1 of INSTALL.md).
+/src/system.pl
+
 # Prolog compilation output (see `clean` in src/Makefile)
 *.ql
 *.qlf
@@ -14,6 +18,9 @@
 /src/*mist
 /src/mist*
 
+# Byte-compiled Emacs mode (see the Emacs section of INSTALL.md)
+*.elc
+
 # Generated HTML library and tags (see `clean` in lib/Makefile)
 /lib/html/
 TAGS
@@ -22,3 +29,7 @@ TAGS
 # The directory itself is kept; its contents are not.
 /tmp/*
 !/tmp/.gitkeep
+
+# The compiled system is moved here by step 7 of INSTALL.md.
+/bin/*
+!/bin/.gitkeep

INSTALL.md

@@ -8,17 +8,23 @@
 - Proofs are typesetted with TeX.
 - HTML files are created with Perl.
 
+**SWI-Prolog 7 and later must be started with `--traditional`.** Without that
+flag `[]` is a reserved constant rather than an atom, and every proof in the
+library that touches lists fails. All the SWI commands below pass it.
+
 
 ## How to install the LPTP - system?
 
-### (0) Unpack the tar file with the command:
+### (0) Get the sources:
 
-        `gunzip -c lptp-1.06.tar.gz | tar xf -`
+```bash
+git clone https://github.com/FredMesnard/LPTP.git
+```
 
-A directory `lptp` is created with the following subdirectories:
+The directory that is created has the following subdirectories:
 
 ```
-        bin             (empty)
+        bin             (empty, for the compiled system)
         doc             (user manual)
         etc             (Emacs mode, Perl scripts)
         examples        (examples)
@@ -29,6 +35,8 @@ A directory `lptp` is created with the following subdirectories:
         tmp             (empty, for temporary files)
 ```
 
+Below, `lptp` stands for that directory.
+
 ### (1) Creating the file `system.pl` in the `lptp/src` directory:
 
 - Goto the `lptp/src/prolog` directory.
@@ -47,6 +55,10 @@ A directory `lptp` is created with the following subdirectories:
 
 - Replace the Prolog atom '/home/staerk/lptp' with the full  pathname to your LPTP directory. LPTP must know where it is located in the file system.
 
+- `src/system.pl` holds the path of one particular installation, so it is
+  not kept under version control. Every clone starts without it, and this
+  step is what creates it.
+
 
 ### (2) A first (optional) test: 
 
@@ -110,15 +122,15 @@ This command concatenates all Prolog source files into one big file `lptp.pl`.
 - Example (SWI-Prolog):
 
 ```prolog
-    unix> pl
+    unix> swipl --traditional
         ?- qcompile('lptp.pl'). % lptp.qlf
         ?- halt.
 ```
 
 - Example (GNU Prolog):
 
 ```prolog
-    unix> gplc --global-size 16384 -o lptp lptp.pl
+    unix> gplc --global-size 65536 -o lptp lptp.pl
 ```
 
 ### (4) The real test:
@@ -136,13 +148,26 @@ This command concatenates all Prolog source files into one big file `lptp.pl`.
     ?- halt.
 ```
 
+- Example (SWI-Prolog):
+
+```prolog
+    unix> swipl --traditional
+        ?- consult('lptp.qlf').
+        ?- consult('all.pl').
+        ?- halt.
+```
+
 - Example (GNU Prolog):
 
 ```prolog
     unix> make allg
         unix> lptp < allg.pl
 ```
 
+- Alternatively, run `etc/run-tests.sh swi` or `etc/run-tests.sh gprolog`
+  from the top directory. It does all of the above and reports a summary.
+  This is what the continuous integration workflow runs.
+
 - About 45,000 lines of formal proofs are checked.
 - There should be no error messages.
 - There may, however, be some LPTP-warnings.
@@ -180,7 +205,9 @@ have to typeset the file `nat.tex` before you typeset the file `list.tex`.
 
 ### (6) Creating HTML files of the library:
 
-- Edit the string `"/usr/local/bin/perl"` in the files `pr2html.perl` and `pl2html.perl` in the `lptp/etc` directory.
+- The scripts `pr2html.perl` and `pl2html.perl` in the `lptp/etc` directory
+  find Perl through `/usr/bin/env`. If your Perl is somewhere `env` cannot
+  see, edit their first line.
 
 - Goto the `lptp/lib` directory.
 
@@ -197,12 +224,12 @@ have to typeset the file `nat.tex` before you typeset the file `list.tex`.
 
 - Remove all the temporary files in the `lptp/tmp` directory.
 
-- Read `lptp/doc/user.ps`.
+- Read `lptp/doc/user.pdf`.
 
 
 ## How to install the Emacs mode for LPTP?
 
-(The Emacs mode is described in an appendix of `lptp/doc/user.ps`.)
+(The Emacs mode is described in an appendix of `lptp/doc/user.pdf`.)
 
 
 ### (1) Setting up `lptp-mode.el`:
@@ -241,13 +268,13 @@ have to typeset the file `nat.tex` before you typeset the file `list.tex`.
 
 - Include the following into your `.emacs` file:
 
-```bash
+```lisp
         (autoload 'lptp-mode "/home/staerk/lptp/etc/lptp-mode" 
             "Major mode for editing formal proofs" t)
         (setq auto-mode-alist 
             (cons '("\\.pr$" . lptp-mode) auto-mode-alist))
         (transient-mark-mode 1)
-````
+```
 Note: You have to change the string `"/home/staerk/lptp/etc/lptp-mode"`.
 
 
@@ -284,7 +311,7 @@ Note: You have to change the string `"/home/staerk/lptp/etc/lptp-mode"`.
             (add-hook 'font-lock-mode-hook
               (lambda ()
                 (set-face-foreground font-lock-keyword-face "RoyalBlue")
-                (set-face-foreground font-lock-reference-face "ForestGreen")
+                (set-face-foreground font-lock-constant-face "ForestGreen")
                 (set-face-foreground font-lock-comment-face "OrangeRed") ))
     ```
 

README.md

@@ -1,8 +1,14 @@
 # LPTP - A Logic Program Theorem Prover
 
+[![CI](https://github.com/FredMesnard/LPTP/actions/workflows/ci.yml/badge.svg)](https://github.com/FredMesnard/LPTP/actions/workflows/ci.yml)
+
 Note that a [web-based version of LPTP](https://ciao-lang.org/playground/lptp.html) is now available. 
 Please use a modern browser such as Google Chrome.
 
+The whole proof corpus is checked on every push under both SWI-Prolog and
+GNU Prolog. To run it yourself, `etc/run-tests.sh swi` or
+`etc/run-tests.sh gprolog` from the top directory.
+
 ## How to learn LPTP?
 
 1. Install the LPTP system (see the file [INSTALL.md](INSTALL.md)).

etc/lptp-mode.el

@@ -654,20 +654,23 @@ imitating normal Unix input editing.
 
 ;; Use `M-x font-lock-mode' to fontify proofs.
 
+;; References used to be shown in `font-lock-reference-face', which Emacs
+;; has since removed in favour of `font-lock-constant-face'.
+
 (defvar lptp-font-lock-keywords
   '(("^:-[ ]*\\([a-z_]*\\)" 1 font-lock-keyword-face)
-    ("lemma(\\([^,)]+\\)" 1 font-lock-reference-face) 
-    ("corollary(\\([^,)]+\\)" 1 font-lock-reference-face) 
-    ("theorem(\\([^,)]+\\)" 1 font-lock-reference-face)
-    ("axiom(\\([^,)]+\\)" 1 font-lock-reference-face)
+    ("lemma(\\([^,)]+\\)" 1 font-lock-constant-face) 
+    ("corollary(\\([^,)]+\\)" 1 font-lock-constant-face) 
+    ("theorem(\\([^,)]+\\)" 1 font-lock-constant-face)
+    ("axiom(\\([^,)]+\\)" 1 font-lock-constant-face)
     ("definition_pred(\\([^,]+\\),\\([0-9]+\\)"
-     (1 font-lock-reference-face) (2 font-lock-reference-face))
+     (1 font-lock-constant-face) (2 font-lock-constant-face))
     ("definition_fun(\\([^,]+\\),\\([0-9]+\\)"
-     (1 font-lock-reference-face) (2 font-lock-reference-face))
+     (1 font-lock-constant-face) (2 font-lock-constant-face))
     ("elimination(\\([^,]+\\),\\([0-9]+\\)"
-     (1 font-lock-reference-face) (2 font-lock-reference-face))
+     (1 font-lock-constant-face) (2 font-lock-constant-face))
     ("introduction(\\([^,]+\\),\\([0-9]+\\)"
-     (1 font-lock-reference-face) (2 font-lock-reference-face))
+     (1 font-lock-constant-face) (2 font-lock-constant-face))
     ("by[ \n\t]+\\([a-z]*\\)" 1 font-lock-keyword-face)
     ("\\(axiom\\)(" 1 font-lock-keyword-face)
     ("\\(lemma\\)(" 1 font-lock-keyword-face)

etc/pl2html.perl

@@ -1,4 +1,4 @@
-#!/usr/local/bin/perl
+#!/usr/bin/env perl
 #   Author: Robert Staerk <staerk@saul.cis.upenn.edu>
 #  Created: Tue Feb  6 16:10:09 1996
 # Filename: pl2html.perl

etc/pr2html.perl

@@ -1,4 +1,4 @@
-#!/usr/local/bin/perl
+#!/usr/bin/env perl
 #   Author: Robert Staerk <staerk@saul.cis.upenn.edu>
 #  Created: Tue Feb  6 16:10:09 1996
 #  Changes: Fri Jun 13 18:22:25 1997

etc/run-tests.sh

@@ -0,0 +1,85 @@
+#!/bin/sh
+#  Created: 2026
+# Filename: run-tests.sh
+# Abstract: Check the whole proof corpus (src/all.pl) with one Prolog system.
+#
+# Usage: etc/run-tests.sh swi
+#        etc/run-tests.sh gprolog
+#
+# Set SWIPL or GPLC to name a specific binary. The script writes
+# `src/system.pl' for the chosen system, as step 1 of INSTALL.md describes.
+
+set -eu
+
+system=${1:-}
+case "$system" in
+    swi|gprolog) ;;
+    *) echo "usage: $0 swi|gprolog" >&2; exit 2 ;;
+esac
+
+root=$(cd "$(dirname "$0")/.." && pwd)
+out=$(mktemp)
+err=$(mktemp)
+trap 'rm -f "$out" "$err"' EXIT
+
+# Every proof file is checked against a clean tmp directory.
+rm -f "$root"/tmp/*.thm "$root"/tmp/*.tex "$root"/tmp/*.aux
+
+sed "s|io__lptp_home('[^']*')|io__lptp_home('$root')|" \
+    "$root/src/prolog/$system.pl" > "$root/src/system.pl"
+
+# `all.pl' names one `check' per proof file; each has to report `o.k.'.
+expected=$(grep -c "^:- check(" "$root/src/all.pl")
+
+cd "$root/src"
+
+case "$system" in
+    swi)
+	# --traditional: without it `[]' is not an atom and the library fails.
+	"${SWIPL:-swipl}" --traditional \
+	    -g "consult('init.pl')" -g "consult('all.pl')" -g halt \
+	    > "$out" 2> "$err" || true
+	;;
+    gprolog)
+	make gprolog GPLC="${GPLC:-gplc}" >/dev/null
+	make allg >/dev/null
+	./lptp < allg.pl > "$out" 2> "$err" || true
+	;;
+esac
+
+# A few `.pr' files write their `.thm' next to the sources instead of into
+# tmp, and those are under version control. Prolog systems disagree on how
+# to print `$(x)', so a check run would otherwise leave them rewritten.
+if git -C "$root" rev-parse --is-inside-work-tree >/dev/null 2>&1; then
+    git -C "$root" checkout -- '*.thm' 2>/dev/null || true
+fi
+
+checked=$(grep -c "LPTP-Message: .* o\.k\.$" "$out" || true)
+lptp_errors=$(grep -c "LPTP-Error" "$out" || true)
+uncaught=$(grep -c "uncaught exception" "$out" || true)
+host_errors=$(grep -c "^ERROR\|Fatal Error" "$err" || true)
+
+echo "=== $system ==="
+echo "proof files checked : $checked / $expected"
+echo "LPTP errors         : $lptp_errors"
+echo "uncaught exceptions : $uncaught"
+echo "host Prolog errors  : $host_errors"
+echo "LPTP warnings       : $(grep -c "LPTP-Warning" "$out" || true)"
+
+status=0
+if [ "$checked" -ne "$expected" ]; then
+    echo "FAIL: $((expected - checked)) proof file(s) did not report o.k." >&2
+    grep -n "uncaught exception\|LPTP-Error" "$out" | head -20 >&2 || true
+    status=1
+fi
+for n in "$lptp_errors" "$uncaught" "$host_errors"; do
+    if [ "$n" -ne 0 ]; then status=1; fi
+done
+if [ "$status" -ne 0 ]; then
+    echo "--- stderr ---" >&2
+    head -30 "$err" >&2
+    echo "FAILED" >&2
+else
+    echo "OK"
+fi
+exit $status