Makefile | 2 1 + 1 - 0 !
checker/Makefile | 2 1 + 1 - 0 !
examiner/Makefile | 2 1 + 1 - 0 !
pogs/Makefile | 2 1 + 1 - 0 !
simplifier/Makefile | 2 1 + 1 - 0 !
sparkformat/Makefile | 2 1 + 1 - 0 !
sparklalr/Makefile | 2 1 + 1 - 0 !
sparkmake/Makefile | 2 1 + 1 - 0 !
sparksimp/Makefile | 2 1 + 1 - 0 !
victor/Makefile | 2 1 + 1 - 0 !
victor_wrapper/Makefile | 2 1 + 1 - 0 !
wraputility/Makefile | 2 1 + 1 - 0 !
12 files changed, 12 insertions(+), 12 deletions(-)

 assume that target is always linux on debian
 This makes it easier to compile SPARK on systems with *BSD kernels.

examiner/Makefile | 6 1 + 5 - 0 !
1 file changed, 1 insertion(+), 5 deletions(-)

 use dpkg-architecture to detect address size

checker/Makefile | 13 7 + 6 - 0 !
1 file changed, 7 insertions(+), 6 deletions(-)

 build checker using swi prolog

checker/sicstus.pro | 8 6 + 2 - 0 !
checker/toplevel.pro | 4 2 + 2 - 0 !
2 files changed, 8 insertions(+), 4 deletions(-)

 various fixes for swi prolog

checker/utilities.pro | 12 0 + 12 - 0 !
1 file changed, 12 deletions(-)

 do not redefine predicates that are already defined by swi prolog

checker/sicstus.pro | 96 21 + 75 - 0 !
1 file changed, 21 insertions(+), 75 deletions(-)

 look for checker files under /usr/share/spark/checker

checker/loadsicstus.pro | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 add missing .pro suffix

checker/loadvc5.pro | 2 2 + 0 - 0 !
1 file changed, 2 insertions(+)

 allow to redefine system predicate flatten/2

checker/checker.pro | 10 10 + 0 - 0 !
1 file changed, 10 insertions(+)

 add swi prolog compatible save predicate

checker/checker.pro | 5 0 + 5 - 0 !
checker/getdcldat.pro | 5 0 + 5 - 0 !
checker/infer2.pro | 1 0 + 1 - 0 !
checker/loadvc5.pro | 10 0 + 10 - 0 !
checker/prooflogs.pro | 1 0 + 1 - 0 !
checker/save.pro | 1 0 + 1 - 0 !
checker/setflags.pro | 1 0 + 1 - 0 !
checker/toplevel.pro | 1 0 + 1 - 0 !
checker/utilities.pro | 2 0 + 2 - 0 !
9 files changed, 27 deletions(-)

 remove all references to close_all_streams/0 in checker
  This predicate does not exist in SWI prolog and is not needed there.

checker/toplevel.pro | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 do not use seeing(user)
  Such calls cause an exception with SWI prolog.

checker/portray.pro | 16 8 + 8 - 0 !
checker/sicstus.pro | 2 1 + 1 - 0 !
2 files changed, 9 insertions(+), 9 deletions(-)

 use portray(true) in calls to write_term

checker/sicstus.pro | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 repeat user input on syntax errors
  This makes using checker *much* easier and is the same
  thing that SICStus does.

Makefile | 2 0 + 2 - 0 !
victor/Makefile | 2 1 + 1 - 0 !
2 files changed, 1 insertion(+), 3 deletions(-)

 do not try to build and install alt-ergo
 alt-ergo is provided in a separate package in Debian.

Makefile | 4 2 + 2 - 0 !
1 file changed, 2 insertions(+), 2 deletions(-)

 fix target dependencies
 Do not clean build-tree after building. Make copyall target dependent
 on build target.

victor/Makefile | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 do not link gmp statically

simplifier/simplifier.pro | 8 4 + 4 - 0 !
1 file changed, 4 insertions(+), 4 deletions(-)

 swi compatible save goals for simplifier

simplifier/Makefile | 21 9 + 12 - 0 !
1 file changed, 9 insertions(+), 12 deletions(-)

 this is the makefile fix

simplifier/data__hyp.pro | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 import list_lo_set/2 from library lists instead of sets

simplifier/librarypredicates.pro | 1 0 + 1 - 0 !
1 file changed, 1 deletion(-)

 do not use nonexistent file_systems module

simplifier/defectreporting.pro | 2 2 + 0 - 0 !
1 file changed, 2 insertions(+)

 use module lists for member/2

simplifier/defectreporting.pro | 1 0 + 1 - 0 !
simplifier/load__switches.pro | 2 1 + 1 - 0 !
simplifier/load__vcg_dpc.pro | 15 0 + 15 - 0 !
3 files changed, 1 insertion(+), 17 deletions(-)

 various fixes

simplifier/Makefile | 1 1 + 0 - 0 !
1 file changed, 1 insertion(+)

 remove executables on clean

simplifier/portray.pro | 16 8 + 8 - 0 !
1 file changed, 8 insertions(+), 8 deletions(-)

 swi and sicstus need portray and portrayed respectively

simplifier/makelog.pro | 1 1 + 0 - 0 !
simplifier/utilities.pro | 5 3 + 2 - 0 !
2 files changed, 4 insertions(+), 2 deletions(-)

 further byte-for-byte fixes

simplifier/defectreporting.pro | 4 2 + 2 - 0 !
1 file changed, 2 insertions(+), 2 deletions(-)

 fix order of arguments in message_hook/3.

simplifier/data__vcg.pro | 2 1 + 1 - 0 !
simplifier/load__switches.pro | 2 1 + 1 - 0 !
simplifier/usage_utilities.pro | 2 1 + 1 - 0 !
3 files changed, 3 insertions(+), 3 deletions(-)

 add missing .pro suffixes

simplifier/data__conc.pro | 1 0 + 1 - 0 !
simplifier/data__pfs.pro | 4 1 + 3 - 0 !
2 files changed, 1 insertion(+), 4 deletions(-)

 do not try to export undefined predicates

simplifier/ioutilities.pro | 2 0 + 2 - 0 !
simplifier/librarypredicates.pro | 1 0 + 1 - 0 !
simplifier/main_simplifier.pro | 1 0 + 1 - 0 !
simplifier/usage_utilities.pro | 1 0 + 1 - 0 !
4 files changed, 5 deletions(-)

 do not to import library file_systems and close_all_streams/0

simplifier/ioutilities.pro | 1 0 + 1 - 0 !
simplifier/main_simplifier.pro | 3 0 + 3 - 0 !
simplifier/schedulesimplification.pro | 3 0 + 3 - 0 !
simplifier/simplifier.pro | 5 0 + 5 - 0 !
4 files changed, 12 deletions(-)

 remove all references to close_all_streams/0.

victor/vct/src/Makefile | 4 0 + 4 - 0 !
1 file changed, 4 deletions(-)

 do not set ldflags and cxxflags in victor's makefile
 Values from environment variables should be used instead. This
 allows to use noopt in DEB_BUILD_OPTIONS.

examiner/Makefile | 2 1 + 1 - 0 !
pogs/Makefile | 2 1 + 1 - 0 !
sparkformat/Makefile | 2 1 + 1 - 0 !
sparklalr/Makefile | 2 1 + 1 - 0 !
sparkmake/Makefile | 2 1 + 1 - 0 !
sparksimp/Makefile | 2 1 + 1 - 0 !
victor_wrapper/Makefile | 2 1 + 1 - 0 !
wraputility/Makefile | 2 1 + 1 - 0 !
8 files changed, 8 insertions(+), 8 deletions(-)

 use ada_opt environment variable
 ADA_OPT contains optimization switches for Ada compiller. This
 allows to use noopt in DEB_BUILD_OPTIONS

victor/vct/src/Makefile | 2 1 + 1 - 0 !
1 file changed, 1 insertion(+), 1 deletion(-)

 link to gmp libraries only when they are needed

examiner/Makefile | 2 1 + 1 - 0 !
pogs/Makefile | 2 1 + 1 - 0 !
sparkformat/Makefile | 2 1 + 1 - 0 !
sparklalr/Makefile | 2 1 + 1 - 0 !
sparkmake/Makefile | 2 1 + 1 - 0 !
sparksimp/Makefile | 2 1 + 1 - 0 !
victor_wrapper/Makefile | 2 1 + 1 - 0 !
wraputility/Makefile | 2 1 + 1 - 0 !
8 files changed, 8 insertions(+), 8 deletions(-)

 add an option to gnatmake that can be set to -jn in debian/rules

examiner/Makefile | 2 2 + 0 - 0 !
pogs/Makefile | 3 2 + 1 - 0 !
sparkformat/Makefile | 2 2 + 0 - 0 !
sparkmake/Makefile | 3 2 + 1 - 0 !
sparksimp/Makefile | 2 1 + 1 - 0 !
victor_wrapper/Makefile | 3 2 + 1 - 0 !
wraputility/Makefile | 3 2 + 1 - 0 !
7 files changed, 13 insertions(+), 5 deletions(-)

---