Put src/system.pl back under version control

.github/workflows/ci.yml

@@ -31,6 +31,17 @@ jobs:
       - name: Check the whole proof corpus
         run: etc/run-tests.sh ${{ matrix.prolog }}
 
+      # src/system.pl and some .thm files are version-controlled yet rewritten
+      # by a run, so the script puts them back. This is what says it worked.
+      - name: The run must leave the working tree untouched
+        run: |
+          if [ -n "$(git status --porcelain)" ]; then
+            echo "the check run left the working tree dirty:"
+            git status --porcelain
+            git diff
+            exit 1
+          fi
+
       - name: Upload generated proofs
         if: always()
         uses: actions/upload-artifact@v7

.gitignore

@@ -4,10 +4,6 @@
 # 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

INSTALL.md

@@ -55,9 +55,9 @@ Below, `lptp` stands for that directory.
 
 - 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.
+- The `src/system.pl` in the repository is a copy of `sicstus.pl` naming
+  someone else's directory, so this step has to be done even though the
+  file is already there.
 
 
 ### (2) A first (optional) test: 

etc/run-tests.sh

@@ -47,11 +47,13 @@ case "$system" in
 	;;
 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.
+# Put back the version-controlled files the run rewrites, so that checking
+# the corpus leaves no trace: src/system.pl, which was configured above, and
+# the `.thm' files a few `.pr' files write next to the sources rather than
+# into tmp -- Prolog systems disagree on how to print `$(x)'.
 if git -C "$root" rev-parse --is-inside-work-tree >/dev/null 2>&1; then
     git -C "$root" checkout -- '*.thm' 2>/dev/null || true
+    git -C "$root" checkout -- src/system.pl 2>/dev/null || true
 fi
 
 checked=$(grep -c "LPTP-Message: .* o\.k\.$" "$out" || true)

src/system.pl

@@ -0,0 +1,79 @@
+/*   Author: Robert Staerk <staerk@math.stanford.edu> */
+/*  Created: Fri Dec  2 15:49:51 1994 */
+% Updated: Wed Jul 21 17:10:49 1999
+/* Filename: sicstus.pl */
+/* Abstract: System predicates for SICStus 3, SunOS. */
+
+% Compiling with SICStus Prolog:
+%
+%	?- prolog_flag(compiling,_,fastcode). 
+% 	?- consult('op.pl').
+% 	?- fcompile('lptp.pl').
+% 	?- halt.
+
+%%d io__lptp_home(gr::out)
+
+io__lptp_home('/home/staerk/lptp12').
+
+%%d io__path_sep(gr::out)
+
+io__path_sep(/).
+
+%%d once(gr::in)
+
+once(Goal) :- call(Goal), !.
+
+%%d concat_atom(grL::in,gr::out)
+
+concat_atom(AtomL,Atom) :-
+	concat_atomL(AtomL,CharL),
+	name(Atom,CharL).
+
+%%d concat_atomL(grL::in,grL::out)
+
+concat_atomL([],[]).
+concat_atomL([Atom|AtomL],Char3L) :-
+	concat_atomL(AtomL,Char1L),
+	name(Atom,Char2L),
+	lst__concat(Char2L,Char1L,Char3L).
+
+%%d atomic_length(gr::in,int::out)
+
+atomic_length(Atom,N) :-
+	name(Atom,CharL),
+	length(CharL,N).
+
+%%d io__get_stream(gr::in,gr::in,gr::out)
+
+io__get_stream(File,Mode,Stream) :-
+	open(File,Mode,Stream).
+
+%%d io__set_output(gr::in)
+
+io__set_output(Stream) :- set_output(Stream).
+
+%%d io__set_input(gr::in)
+
+io__set_input(Stream) :- set_input(Stream).
+
+%%d db__user_stream(gr::out)
+
+:- dynamic db__user_stream/1.
+
+db__user_stream(user).
+
+%%d io__original_user(gr::out)
+
+io__original_user(user).
+
+%%d read_with_variables(any,any)
+
+read_with_variables(Term,VarL) :-
+	read_term(Term,[variable_names(VarL)]).
+
+%%d io__exec_file(gr::in)
+
+io__exec_file(File) :- consult(File).
+
+% sicstus.pl ends here
+