# HG changeset patch
# User wenzelm
# Date 1509744992 -3600
# Node ID 8905114fd23b85f5afaaa2ee7bcb6de06966abbb
# Parent  17eb23e4363051bba83f857bea26fa363cb5694e
support for libgmp on x86_64-darwin;

diff -r 17eb23e43630 -r 8905114fd23b Admin/polyml/CHECKLIST
--- a/Admin/polyml/CHECKLIST	Fri Nov 03 19:20:47 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-Notes on building Poly/ML as Isabelle component
-===============================================
-
-* component skeleton:
-  $ isabelle build_polyml_component -s sha1 component
-
-* include full source (without symlink), for example:
-  $ wget https://github.com/polyml/polyml/archive/master.zip
diff -r 17eb23e43630 -r 8905114fd23b Admin/polyml/NOTES
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/polyml/NOTES	Fri Nov 03 22:36:32 2017 +0100
@@ -0,0 +1,19 @@
+Notes on building Poly/ML as Isabelle component
+===============================================
+
+* component skeleton:
+  $ isabelle build_polyml_component -s sha1 component
+
+* include full source (without symlink), for example:
+  $ wget https://github.com/polyml/polyml/archive/master.zip
+
+* libgmp on x86_64-darwin:
+
+  https://github.com/Homebrew/homebrew-core/blob/master/Formula/gmp.rb
+  https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz
+
+  ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
+  make check
+  make install
+
+  isabelle build_polyml -m64 -s sha1 src --with-gmp LDFLAGS='-L/usr/local/lib' CPPFLAGS='-O3 -I/usr/local/include'
diff -r 17eb23e43630 -r 8905114fd23b src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Fri Nov 03 19:20:47 2017 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Fri Nov 03 22:36:32 2017 +0100
@@ -122,12 +122,18 @@
       """, redirect = true, echo = true).check
 
     val ldd_files =
-      if (Platform.is_linux) {
-        val libs = bash(root, "ldd target/bin/poly").check.out_lines
-        val Pattern = """\s*libgmp.*=>\s*(\S+).*""".r
-        for (Pattern(lib) <- libs) yield lib
+    {
+      val ldd_pattern =
+        if (Platform.is_linux) Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r))
+        else if (Platform.is_macos) Some(("otool -L", """\s*(\S+libgmp.*dylib).*""".r))
+        else None
+      ldd_pattern match {
+        case Some((ldd, pattern)) =>
+          val lines = bash(root, ldd + " target/bin/poly").check.out_lines
+          for { line <- lines; List(lib) <- pattern.unapplySeq(line) } yield lib
+        case None => Nil
       }
-      else Nil
+    }
 
 
     /* sha1 library */