 		 (sit-for 2)))
 	     (simulate-input-expression str))
     (simulate-input-expression str)))
+
+;;; ================================================================================
+
+(defun generate-compile-build-specware4 (&optional in-current-dir?)
+  (interactive "P")
+  (generate-specware4-aux in-current-dir? t nil))
+
+(defun just-generate-specware4 (&optional in-current-dir?)
+  (interactive "P")
+  (generate-specware4-aux in-current-dir? nil nil))
+
+(defun generate-specware4-aux (in-current-dir? also-compile-and-build? regenerating?)
+  (let* ((*specware4-dir      (sw::normalize-filename
+                               (if in-current-dir? 
+                                   (strip-final-slash default-directory)
+                                 (concat (getenv "SPECWARE4")))))
+         (bin-dir             (binary-directory *specware4-dir))
+         (specware-executable (concat bin-dir "/Specware4."
+                                      (if *windows-system-p* "exe"
+                                        *lisp-executable-extension*)))
+         (specware4-base-lisp (concat *specware4-dir "/Applications/Specware/Specware4-base.lisp")))
+
+    (prepare-specware-build-buffer "*Generate Specware lisp files from specs*" *specware4-dir)
+
+    (cond ((not (file-exists-p specware-executable))
+           ;; can't process Specware4.sw without a running specware, so compile, build, and come back here
+           (progn (message "No specware executable, so will first build one, then try again.") 
+                  (sit-for 4))
+           (specware-build-command "### No specware executable, so will first build one, then try again.")
+           (compile-specware4-aux in-current-dir? t t))
+          ((file-newer-than-file-p specware4-base-lisp specware-executable)
+           ;; specware executable is not up to date with current sources, so compile, build, and come back here
+           (progn (message "Previously generated specware lisp files are newer than specware executable.") 
+                  (sit-for 4)
+                  (message "So will recompile them, rebuild specware, and then try again here.") 
+                  (sit-for 4))
+           (specware-build-command "### Previously generated specware lisp files are newer than specware executable,") 
+           (specware-build-command "### so will recompile them, rebuild specware, and then try again here.") 
+           (compile-specware4-aux in-current-dir? t t))
+          (t
+           ;; we have an up-to-date specware, so generate new lisp files
+           ;; Note: (boot) processes Specware4.sw to produce new lisp files
+
+           (progn (message "Generating Specware lisp files from specs, via (cl-user::boot) ...")
+                  (sit-for 1))
+           
+           (sit-for (if regenerating? 10 2)) ; avoid race with prior build process
+           (specware-build-command "%S --dynamic-space-size %S" specware-executable *sbcl-size*)
+           (sit-for 2)  
+           (let ((print-progress-message
+		  (if also-compile-and-build?
+		      '(format t "Call back to emacs to tell it to compile and build Specware.~%")
+		    ""))
+		 (callback-to-emacs
+                  ;; if we are going to proceed on with compilation and building,
+                  ;; then have lisp generate a call back to emacs just before quiting
+                  (if also-compile-and-build?
+                      ;; First time through, make the third arg true to cause a replay after oompile and build.
+                      ;; Second time through, make it false so we don't replay yet again.
+                      (specware-build-eval-emacs-str "(progn (sit-for 5) (compile-specware4-aux %s t %s))" 
+                                                     in-current-dir?
+                                                     (not regenerating?))
+                    "")))
+             (specware-build-command "(progn (cl:time (cl-user::boot)) %S %s (cl-user::quit))" 
+				     print-progress-message
+				     callback-to-emacs))))))
+
+;;; ================================================================================
+
+(defun compile-build-specware4 (&optional in-current-dir?)
+  (interactive "P")
+  (compile-specware4-aux in-current-dir? t))
+
+(defun just-compile-specware4 (&optional in-current-dir?)
+  (interactive "P")
+  (compile-specware4-aux in-current-dir? nil))
+
+(defun compile-specware4-aux (&optional in-current-dir? also-build? also-regenerate?)
+  (interactive "P")
+  (let* ((*specware4-dir        (sw::normalize-filename
+                                 (if in-current-dir?
+                                     (strip-final-slash (if (stringp in-current-dir?)
+                                                            in-current-dir?
+                                                          default-directory))
+                                   (getenv "SPECWARE4"))))
+	 (build-dir             (concat *specware4-dir "/Applications/Specware/Handwritten/Lisp"))
+	 (lisp-dir              (concat *specware4-dir "/Applications/Specware/lisp"))
+	 (specware4-lisp        (concat lisp-dir "/Specware4.lisp"))
+	 (specware4-base-lisp   (concat *specware4-dir "/Applications/Specware/Specware4-base.lisp"))
+         (specware4-loader      (concat build-dir "/Specware4.lisp")))
+
+    ;; move any old Specware.lisp out of the way
+    (when (and (file-exists-p specware4-base-lisp)
+	       (or (not (file-exists-p specware4-lisp))
+		   (file-newer-than-file-p specware4-base-lisp specware4-lisp)))
+      (when (file-exists-p specware4-lisp)
+	(copy-file specware4-lisp (concat lisp-dir "/Specware4-saved.lisp") t))
+      (copy-file specware4-base-lisp specware4-lisp t))
+
+    (prepare-specware-build-buffer "*Compile Specware lisp files*" build-dir)
+
+    (progn (message "Compiling Specware lisp files, by loading %s" specware4-loader)
+           (sit-for 1))
+
+    ;; start lisp
+    (specware-build-command "sbcl --dynamic-space-size %S" *sbcl-size*) ; Generalize later
+    (sit-for 2)
+
+    ;; load utilities
+    (specware-build-command "(cl:load %S)" (concat *specware4-dir "/Applications/Handwritten/Lisp/exit-on-errors"))
+
+    ;; loading Specare4.lisp will cause lisp files to be compiled
+    (let ((print-progress-message
+           (if also-build?
+	       '(format t "Call back to emacs to tell it to build Specware.~%")
+	     ""))
+	  (callback-to-emacs
+           ;; If we are doing more after we compile, then prepare a form for the lisp image
+           ;; to pass back to emacs for invocation just before that lisp image dies.
+           (if also-build?
+               (specware-build-eval-emacs-str "(progn (sit-for 5) (new-build-specware4 %s %s))" 
+                                              in-current-dir? 
+                                              also-regenerate?)
+             "")))
+      (specware-build-command "(progn (cl:load %S) %S %s (terpri) (quit))" 
+                              specware4-loader 
+			      print-progress-message
+                              callback-to-emacs))))
+
+;;; ================================================================================
+
+(defun just-build-specware4 (&optional in-current-dir? regenerate?)
+  (interactive "P")
+  (new-build-specware4 in-current-dir? nil))
+
+(defun new-build-specware4 (&optional in-current-dir? regenerate?)
+  (interactive "P")
+  (let* ((*specware4-dir        (sw::normalize-filename
+                                 (if in-current-dir?
+                                     (strip-final-slash (if (stringp in-current-dir?)
+                                                            in-current-dir?
+                                                          default-directory))
+                                   (getenv "SPECWARE4"))))
+	 (build-dir             (concat *specware4-dir "/Applications/Specware/Handwritten/Lisp"))
+	 (bin-dir               (binary-directory *specware4-dir))
+	 (lisp-dir              (concat *specware4-dir "/Applications/Specware/lisp"))
+	 (specware-executable   (concat bin-dir "/Specware4." (if *windows-system-p* "exe" *lisp-executable-extension*)))
+	 (specware4-lisp        (concat lisp-dir "/Specware4.lisp"))
+         (specware4-lisp-binary (concat lisp-dir "/Specware4." *fasl-extension*))
+         (specware4-loader      (concat build-dir "/Specware4.lisp")))
+
+    (prepare-specware-build-buffer "*Build Specware executable*" build-dir)
+
+    (progn (message "Build new Specware executable after loading %s" specware4-loader)
+           (sit-for 1))
+
+    ;; start lisp
+    (specware-build-command "sbcl --dynamic-space-size %S" *sbcl-size*) ; Generalize later
+    (sit-for 2)
+
+    ;; load utilities
+    (specware-build-command "(cl:load %S)" (concat *specware4-dir "/Applications/Handwritten/Lisp/exit-on-errors"))
+
+    (cond ((not (file-exists-p specware4-lisp-binary))
+           ;; error
+           )
+          ((not (file-newer-than-file-p specware4-lisp-binary specware4-lisp))
+           ;; error
+           )
+          (t
+           (let ((print-progress-message
+		  (if regenerate? 
+		      '(format t "Call back to emacs to tell it to gnerate Specware again.~%")
+		    ""))
+		 (callback-to-emacs
+                  ;; If we are regenerating, have the lisp image tell emacs to invoke generate-compile-build-specware4 
+                  ;; just before that lisp image saved itself and dies.
+                  ;; To avoid races, have the form sent back to emacs delay for 5 seconds before proceeding,
+                  ;; to give the lisp image time to save itself before it will be invoked.
+                  (if regenerate? 
+                      (specware-build-eval-emacs-str "(progn (sit-for 10) (generate-specware4-aux %s t t))" in-current-dir?)
+                    "")))
+             (specware-build-command "(progn (cl:load %S) %S %s (force-output t) (sb-ext:save-lisp-and-die %S :executable t))"
+                                     specware4-loader
+				     print-progress-message
+                                     callback-to-emacs
+                                     specware-executable))))))
+
+;;; ================================================================================
 
 (defun build-specware4-and-then-exit (&optional in-current-dir?)
   (interactive "P")

	(accept-process-output proc (or timeout 5))))))

(defun set-socket-init-for-specware ()
  (message "set-socket-init-for-specware")
  (setq sw:common-lisp-image-arguments
    (list "-L" (getenv "SOCKET_INIT_FILE"))))


			sw:common-lisp-image-file))
      (sleep-for 2)
      (wait-for-prompt 0.5)
      (delete-other-windows)
      (set-frame-pixel-size (car (frames-of-buffer)) 1200 800)
      (sw:eval-in-lisp-no-value
       (format "(cl:namestring (Specware::change-directory %S))" sw:common-lisp-directory))
      (let ((init-form (or (getenv "SPECWARE_INIT_FORM")
