Make Z3 install failures more obvious on unsupported platforms

Previously, when installing on platforms that don't have a prebuilt Z3 binary available from GitHub, we'd silently install an x86 Linux binary anyway, and then things would mysteriously fail at run time. So let's make two changes: (1) explicitly check the architecture and only install for x86_64 systems, since there are no prebuilt Z3 binaries for other architectures on the version of Z3 we use; and (2) provide more visible feedback if the install script fails to install a Z3 binary, by moving it to be a post-install rather than pre-install phase.
vcanumalla · Aug 14, 2022 · 426ffbf · 426ffbf
1 parent 096430e
commit 426ffbf
Show file tree

Hide file tree

Showing 2 changed files with 40 additions and 15 deletions.
diff --git a/rosette/info.rkt b/rosette/info.rkt
@@ -14,8 +14,9 @@
      (experimental))))
      ;; Documentation category. On Racket 6.3+ this can be any string.
 
-;; Runs the code in `private/install.rkt` before installing this collection.
+;; Runs the code in `private/install.rkt` before and after installing this collection.
 (define pre-install-collection "private/install.rkt")
+(define post-install-collection "private/install.rkt")
 (define compile-omit-files '("private/install.rkt"
                              "lib/trace/report/node_modules"))
 

diff --git a/rosette/private/install.rkt b/rosette/private/install.rkt
@@ -4,25 +4,49 @@
 ;; If missing, builds & links a z3 binary.
 
 
-(provide pre-installer)
+(provide pre-installer post-installer)
 
 (require racket/match
          racket/file
          racket/port
          net/url
          file/unzip)
 
+; We need to run the Z3 installer as a pre-install step, because building the
+; documentation relies on Z3 being available. But pre-install is so early in
+; the build that its output gets pushed off screen by the later steps. So we
+; use this little hack to repeat the failure message as a post-install step,
+; which happens at the very end of the install and so makes the error message
+; far more obvious.
+(define z3-install-failure #f)
+
+(define z3-version "4.8.8")
+
 (define (print-failure path msg)
   (printf "\n\n********** Failed to install Z3 **********\n\n")
-  (printf "You'll need to manually install a Z3 binary\n")
-  (printf "to this location: ~a\n\n" path)
-  (printf "The problem was:\n~a\n\n" msg)
-  (printf "*********\n\n\n"))
+  (printf "Rosette installed successfully, but wasn't able to install the Z3 SMT solver.\n\n")
+  (printf "You'll need to manually install a Z3 binary at this location:\n")
+  (printf "    ~a\n" path)
+  (printf "or anywhere that is on your PATH. Alternatively, in your programs, you can\n")
+  (printf "construct a solver object manually:\n")
+  (printf "    (current-solver (z3 #:path \"/path/to/z3\"))\n\n")
+  (printf "Note that Rosette ships with a specific release of Z3 (v~a). Installing a\n" z3-version)
+  (printf "different version of Z3 may change the performance of Rosette programs.\n\n")
+  (printf "The problem was:\n    ~a\n\n" msg)
+  (printf "**********\n\n\n"))
+
+(define (post-installer collections-top-path)
+  (match z3-install-failure
+    [(cons z3-path msg) (print-failure z3-path msg)]
+    [_ (void)]))
 
 (define (pre-installer collections-top-path racl-path)
   (define bin-path (simplify-path (build-path racl-path ".." "bin")))
   (define z3-path (build-path bin-path "z3"))
-  (with-handlers ([exn:fail? (lambda (e) (print-failure z3-path (exn-message e)))])
+  (with-handlers ([exn:fail? (lambda (e)
+                               (set! z3-install-failure (cons z3-path (exn-message e)))
+                               (print-failure z3-path (exn-message e))
+                               (raise e))])
     (unless (custom-z3-symlink? z3-path)
       (define-values (z3-url z3-path-in-zip) (get-z3-url))
       (define z3-port (get-pure-port (string->url z3-url) #:redirections 10))  
@@ -44,16 +68,16 @@
 
 (define (get-z3-url)
   (define site "https://github.com/Z3Prover/z3/releases/download")
-  (define version "z3-4.8.8")
   (define-values (os exe)
-    (match (list (system-type) (system-type 'word))
-      ['(unix 64)    (values "x64-ubuntu-16.04" "z3")]
-      [`(macosx ,_)  (values "x64-osx-10.14.6" "z3")]
-      ['(windows 64) (values "x64-win" "z3.exe")]
-      [any           (raise-user-error 'get-z3-url "Unknown system type '~a'" any)]))
-  (define name (format "~a-~a" version os))
+    (match (list (system-type 'os*) (system-type 'arch))
+      ['(linux x86_64)   (values "x64-ubuntu-16.04" "z3")]
+      ; TODO: use a native aarch64 Z3 build on macOS when we upgrade to a newer Z3
+      [`(macosx ,_)      (values "x64-osx-10.14.6" "z3")]
+      ['(windows x86_64) (values "x64-win" "z3.exe")]
+      [any               (raise-user-error 'get-z3-url "No Z3 binary available for system type '~a" any)]))
+  (define name (format "z3-~a-~a" z3-version os))
   (values
-   (format "~a/~a/~a.zip" site version name)
+   (format "~a/z3-~a/~a.zip" site z3-version name)
    (format "~a/bin/~a" name exe)))