Re: [PVS-Help] compilation problems under debian etch - solved

[Hendrik Tews <H.Tews@xxxxxxxx>]

The problem came from the makefile, which was not POSIX conform,
from gnu make NEWS, version 3.81

    * WARNING: Backward-incompatibility!
      In order to comply with POSIX, the way in which GNU make processes
      backslash-newline sequences in command strings has changed.  If your
      makefiles use backslash-newline sequences inside of single-quoted
      strings in command scripts you will be impacted by this change.  See
      the GNU make manual subsection "Splitting Command Lines" (node
      "Splitting Lines"), in section "Command Syntax", chapter "Writing the
      Commands in Rules", for details.

And from splitting command lines node :

    Sometimes you want to split a long line inside of single
    quotes, but you don't want the backslash-newline to appear in the
    quoted content. [...]
    One simple way of handling this is to place
    the quoted string, or even the entire command, into a `make'
    variable then use the variable in the command. In this situation
    the newline quoting rules for makefiles will be used, and the
    backslash-newline will be removed. 

see patch below.

Bye,

Hendrik

Index: Makefile.in
===================================================================
RCS file: /home/tews/Store/src/pvs/Makefile.in,v
retrieving revision 1.3
diff -u -r1.3 Makefile.in
--- Makefile.in	11 Jan 2007 13:43:53 -0000	1.3
+++ Makefile.in	13 Jan 2007 21:14:04 -0000
@@ -479,22 +479,26 @@
 		   -load src/make-pvs-methods.lisp
 endif
 
+CMU-LISP-COMPILE-EXPR=\
+	'(load "pvs.system" :verbose t) \
+	 (let ((*load-pvs-prelude* nil)) \
+	   (pvs::operate-on-system :pvs :compile)) \
+	 (quit)'
+
+CMU-BUILD-IMAGE-EXPR=\
+	'(load "pvs.system" :verbose t) \
+	 (unwind-protect \
+	   (pvs::operate-on-system :pvs :compile) \
+	   (save-lisp "$@.core" :init-function (function startup-pvs)))'
+
 $(cmulisp-devel) $(cmulisp-rt) : $(image-deps) \
            $(pvs-make-files) $(ess) $(ff-files) \
            $(lisp-files) $(cmulisp) lib/prelude.pvs lib/prelude.prf
 	@echo "******* Compiling PVS files in CMU Lisp"
 	$(MKDIR) -p $(subst $(SYSTEM)-cmulisp,,$@)
-	$(CMULISPEXE) -eval '(load "pvs.system" :verbose t) \
-                             (let ((*load-pvs-prelude* nil)) \
-                               (pvs::operate-on-system :pvs :compile)) \
-                             (quit)'
+	$(CMULISPEXE) -eval $(CMU-LISP-COMPILE-EXPR)
 	@echo "******* Building PVS image $@"
-	$(CMULISPEXE) -eval '(load "pvs.system" :verbose t) \
-                             (unwind-protect \
-                                 (pvs::operate-on-system :pvs :compile) \
-                               (save-lisp "$@.core" \
-                                   :init-function (function startup-pvs) \
-                               ))'
+	$(CMULISPEXE) -eval $(CMU-BUILD-IMAGE-EXPR)
 	-rm $(PVSPATH)BDD/$(PLATFORM)/bdd-cmu.*
 	cp $(CMULISPEXE) $(subst $(SYSTEM)-cmulisp,,$@)
 	cp $(PVSPATH)BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-cmulisp,,$@)