--- 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
--- /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'
--- 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 */