Attachment #186211 for bug #257679

Lines 24-30 Link Here

(-)pvs4.2-orig/doc/user-guide/Makefile.in (-1 / +1 lines)
24	pdflatex $<	24	pdflatex $<
25		25
26	sum-nosub.tex sum-sub.tex sum-tccs.tex : sum.pvs sum.el	26	sum-nosub.tex sum-sub.tex sum-tccs.tex : sum.pvs sum.el
27	@PVSPATH@/pvs -batch -q -l sum.el -f kill-process	27	@PVSPATH@/pvs -batch -q -l sum.el \|\| echo
28		28
29	.PHONY: clean	29	.PHONY: clean
30	clean :	30	clean :




		   -load src/make-pvs-methods.lisp
endif

CMU-LISP-COMPILE-EXPR=\
       '(load "pvs.system" :verbose t) \
        (let ((*load-pvs-prelude* nil)) \
	  (mk:operate-on-system :pvs :compile)) \
        (quit)'

CMU-BUILD-IMAGE-EXPR=\
       '(load "pvs.system" :verbose t) \
        (unwind-protect \
	  (mk: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 $(CMU-LISP-COMPILE-EXPR)
                             (let ((*load-pvs-prelude* nil)) \
                               (mk:operate-on-system :pvs :compile)) \
                             (quit)'
	@echo "******* Building PVS image $@"
	$(CMULISPEXE) -eval $(CMU-BUILD-IMAGE-EXPR)
                             (unwind-protect \
                                 (mk:operate-on-system :pvs :compile) \
                               (save-lisp "$@.core" \
                                   :init-function (function startup-pvs) \
                               ))'
	-rm $(PVSPATH)BDD/$(PLATFORM)/bdd-cmu.*
	cp $(CMULISPEXE) $(subst $(SYSTEM)-cmulisp,,$@)
	cp $(PVSPATH)BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-cmulisp,,$@)

Return to bug 257679

Lines 488-509 Link Here

(-)pvs4.2-orig/Makefile.in (-10 / +14 lines)
488	-load src/make-pvs-methods.lisp	488	-load src/make-pvs-methods.lisp
489	endif	489	endif
490		490
		491	CMU-LISP-COMPILE-EXPR=\
		492	'(load "pvs.system" :verbose t) \
		493	(let ((load-pvs-prelude nil)) \
		494	(mk:operate-on-system :pvs :compile)) \
		495	(quit)'
		496
		497	CMU-BUILD-IMAGE-EXPR=\
		498	'(load "pvs.system" :verbose t) \
		499	(unwind-protect \
		500	(mk:operate-on-system :pvs :compile) \
		501	(save-lisp "$@.core" :init-function (function startup-pvs)))'
		502
491	$(cmulisp-devel) $(cmulisp-rt) : $(image-deps) \	503	$(cmulisp-devel) $(cmulisp-rt) : $(image-deps) \
492	$(pvs-make-files) $(ess) $(ff-files) \	504	$(pvs-make-files) $(ess) $(ff-files) \
493	$(lisp-files) $(cmulisp) lib/prelude.pvs lib/prelude.prf	505	$(lisp-files) $(cmulisp) lib/prelude.pvs lib/prelude.prf
494	@echo "******* Compiling PVS files in CMU Lisp"	506	@echo "******* Compiling PVS files in CMU Lisp"
495	$(MKDIR) -p $(subst $(SYSTEM)-cmulisp,,$@)	507	$(MKDIR) -p $(subst $(SYSTEM)-cmulisp,,$@)
496	$(CMULISPEXE) -eval '(load "pvs.system" :verbose t) \	508	$(CMULISPEXE) -eval $(CMU-LISP-COMPILE-EXPR)
497	(let ((load-pvs-prelude nil)) \
498	(mk:operate-on-system :pvs :compile)) \
499	(quit)'
500	@echo "******* Building PVS image $@"	509	@echo "******* Building PVS image $@"
501	$(CMULISPEXE) -eval '(load "pvs.system" :verbose t) \	510	$(CMULISPEXE) -eval $(CMU-BUILD-IMAGE-EXPR)
502	(unwind-protect \
503	(mk:operate-on-system :pvs :compile) \
504	(save-lisp "$@.core" \
505	:init-function (function startup-pvs) \
506	))'
507	-rm $(PVSPATH)BDD/$(PLATFORM)/bdd-cmu.*	511	-rm $(PVSPATH)BDD/$(PLATFORM)/bdd-cmu.*
508	cp $(CMULISPEXE) $(subst $(SYSTEM)-cmulisp,,$@)	512	cp $(CMULISPEXE) $(subst $(SYSTEM)-cmulisp,,$@)
509	cp $(PVSPATH)BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-cmulisp,,$@)	513	cp $(PVSPATH)BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-cmulisp,,$@)