support for libgmp on x86_64-darwin;
authorwenzelm
Fri Nov 03 22:36:32 2017 +0100 (18 months ago)
changeset 669988905114fd23b
parent 66997 17eb23e43630
child 66999 c70c47dcf63e
support for libgmp on x86_64-darwin;
Admin/polyml/CHECKLIST
Admin/polyml/NOTES
src/Pure/Admin/build_polyml.scala
     1.1 --- a/Admin/polyml/CHECKLIST	Fri Nov 03 19:20:47 2017 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,8 +0,0 @@
     1.4 -Notes on building Poly/ML as Isabelle component
     1.5 -===============================================
     1.6 -
     1.7 -* component skeleton:
     1.8 -  $ isabelle build_polyml_component -s sha1 component
     1.9 -
    1.10 -* include full source (without symlink), for example:
    1.11 -  $ wget https://github.com/polyml/polyml/archive/master.zip
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/polyml/NOTES	Fri Nov 03 22:36:32 2017 +0100
     2.3 @@ -0,0 +1,19 @@
     2.4 +Notes on building Poly/ML as Isabelle component
     2.5 +===============================================
     2.6 +
     2.7 +* component skeleton:
     2.8 +  $ isabelle build_polyml_component -s sha1 component
     2.9 +
    2.10 +* include full source (without symlink), for example:
    2.11 +  $ wget https://github.com/polyml/polyml/archive/master.zip
    2.12 +
    2.13 +* libgmp on x86_64-darwin:
    2.14 +
    2.15 +  https://github.com/Homebrew/homebrew-core/blob/master/Formula/gmp.rb
    2.16 +  https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz
    2.17 +
    2.18 +  ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
    2.19 +  make check
    2.20 +  make install
    2.21 +
    2.22 +  isabelle build_polyml -m64 -s sha1 src --with-gmp LDFLAGS='-L/usr/local/lib' CPPFLAGS='-O3 -I/usr/local/include'
     3.1 --- a/src/Pure/Admin/build_polyml.scala	Fri Nov 03 19:20:47 2017 +0100
     3.2 +++ b/src/Pure/Admin/build_polyml.scala	Fri Nov 03 22:36:32 2017 +0100
     3.3 @@ -122,12 +122,18 @@
     3.4        """, redirect = true, echo = true).check
     3.5  
     3.6      val ldd_files =
     3.7 -      if (Platform.is_linux) {
     3.8 -        val libs = bash(root, "ldd target/bin/poly").check.out_lines
     3.9 -        val Pattern = """\s*libgmp.*=>\s*(\S+).*""".r
    3.10 -        for (Pattern(lib) <- libs) yield lib
    3.11 +    {
    3.12 +      val ldd_pattern =
    3.13 +        if (Platform.is_linux) Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r))
    3.14 +        else if (Platform.is_macos) Some(("otool -L", """\s*(\S+libgmp.*dylib).*""".r))
    3.15 +        else None
    3.16 +      ldd_pattern match {
    3.17 +        case Some((ldd, pattern)) =>
    3.18 +          val lines = bash(root, ldd + " target/bin/poly").check.out_lines
    3.19 +          for { line <- lines; List(lib) <- pattern.unapplySeq(line) } yield lib
    3.20 +        case None => Nil
    3.21        }
    3.22 -      else Nil
    3.23 +    }
    3.24  
    3.25  
    3.26      /* sha1 library */