This distribution of SPASS 3.8ds, described in Blanchette, Popescu, Wand, and
Weidenbach's ITP 2012 paper "More SPASS with Isabelle", has been compiled from
sources available at https://www.cs.vu.nl/~jbe248/spass-3.8ds-src.tar.gz
via "make".

For compatibility with current Isabelle platforms, these sources have been
patched as follows:

diff -Nru src-orig/makefile src/makefile
--- src-orig/makefile	2015-01-06 12:11:07.000000000 +0100
+++ src/makefile	2026-07-14 13:06:41.166559181 +0200
@@ -77,7 +77,7 @@
 # Enables catching of some common signals (segmentation fault ...)
 
 
-WARNINGS = -pedantic -Wall -Wshadow -Wpointer-arith -Wwrite-strings -std=c99 #-Wconversion  
+WARNINGS = -Wno-error=implicit-function-declaration -pedantic -Wall -Wshadow -Wpointer-arith -Wwrite-strings -std=c99 #-Wconversion  
 # Turn off some warnings for scanner files
 SCANNERFLAGS=-Wno-implicit -Wno-uninitialized
 
diff -Nru src-orig/misc.c src/misc.c
--- src-orig/misc.c	2015-01-06 12:11:07.000000000 +0100
+++ src/misc.c	2026-07-14 12:58:56.588589600 +0200
@@ -44,7 +44,9 @@
 
 #include "misc.h"
 #include "strings.h" /* Cannot be moved to misc.h as long as there is no separate type.h, e.g. for pointers */
+#ifndef __CYGWIN__
 #include "execinfo.h" //backtrace and backtrade_symbols, for dump
+#endif
 /**************************************************************/
 /* Functions                                                  */
 /**************************************************************/
@@ -132,6 +134,7 @@
   EFFECT:  Flushes the streams then dumps a core.
 ***************************************************************/
 {
+#ifndef __CYGWIN__
 	void *array[150];
 	size_t size;
 	char **strings;
@@ -151,6 +154,7 @@
   fflush(misc_ERROROUT);
   fflush(stdout);
   fflush(stderr);
+#endif
   abort();
 }
 

Note that regular SPASS sources can be downloaded from
https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/classic-spass-theorem-prover
--- but official SPASS releases do not work with Isabelle.


        Makarius
        14-Jul-2026
