# HG changeset patch
# User wenzelm
# Date 1478814886 -3600
# Node ID 784e28e4dc57a1c7ba21b6f2848e84055ae18783
# Parent  bba1d341bdf6e13c1abd802473911e568335b3f2
proper options;
simplified command-line;
tuned;

diff -r bba1d341bdf6 -r 784e28e4dc57 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Thu Nov 10 22:06:36 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Thu Nov 10 22:54:46 2016 +0100
@@ -19,24 +19,24 @@
     "x86-linux" ->
       Platform_Info(
         options_multilib =
-          List("--build=i386", "CFLAGS='-m32 -O3'", "CXXFLAGS='-m32 -O3'", "CCASFLAGS='-m32'")),
+          List("--build=i386", "CFLAGS=-m32 -O3", "CXXFLAGS=-m32 -O3", "CCASFLAGS=-m32")),
     "x86_64-linux" -> Platform_Info(),
     "x86-darwin" ->
       Platform_Info(
         options =
-          List("--build=i686-darwin", "CFLAGS='-arch i686 -O3 -I../libffi/include'",
-            "CXXFLAGS='-arch i686 -O3", "-I../libffi/include'", "CCASFLAGS='-arch i686 -O3'",
-            "LDFLAGS='-segprot POLY rwx rwx'")),
+          List("--build=i686-darwin", "CFLAGS=-arch i686 -O3 -I../libffi/include",
+            "CXXFLAGS=-arch i686 -O3 -I../libffi/include", "CCASFLAGS=-arch i686 -O3",
+            "LDFLAGS=-segprot POLY rwx rwx")),
     "x86_64-darwin" ->
       Platform_Info(
         options =
-          List("--build=x86_64-darwin", "CFLAGS='-arch x86_64 -O3 -I../libffi/include'",
-            "CXXFLAGS='-arch x86_64 -O3 -I../libffi/include'", "CCASFLAGS='-arch x86_64'",
-            "LDFLAGS='-segprot POLY rwx rwx'")),
+          List("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include",
+            "CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64",
+            "LDFLAGS=-segprot POLY rwx rwx")),
     "x86-windows" ->
       Platform_Info(
         options =
-          List("--host=i686-w32-mingw32", "CPPFLAGS='-I/mingw32/include'", "--disable-windows-gui"),
+          List("--host=i686-w32-mingw32", "CPPFLAGS=-I/mingw32/include", "--disable-windows-gui"),
         shell_path = "/mingw32/bin",
         copy_files =
           List("/mingw32/bin/libgcc_s_dw2-1.dll",
@@ -45,7 +45,7 @@
     "x86_64-windows" ->
       Platform_Info(
         options =
-          List("--host=x86_64-w64-mingw32", "CPPFLAGS='-I/mingw64/include'", "--disable-windows-gui"),
+          List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
         shell_path = "/mingw64/bin",
         copy_files =
           List("/mingw64/bin/libgcc_s_seh-1.dll",
@@ -58,7 +58,6 @@
     source: Path,
     progress: Progress = Ignore_Progress,
     platform: String = default_platform,
-    multilib: Boolean = false,
     options: List[String] = Nil)
   {
     source.is_dir || error("Bad source directory: " + source)
@@ -67,24 +66,29 @@
       platform_info.get(platform) getOrElse
         error("Bad platform identifier: " + quote(platform))
 
-    val target = Path.explode(platform)
+    val multilib =
+      platform == "x86-linux" && Isabelle_System.getenv("ISABELLE_PLATFORM64") == "x86_64-linux"
 
     val configure_options =
-      info.options ::: List("--enable-intinf-as-int") ::: options :::
-      (if (multilib) info.options_multilib else info.options)
+      (if (multilib) info.options_multilib else info.options) :::
+        List("--enable-intinf-as-int") ::: options
 
     Isabelle_System.bash(cwd = source.file,
       script =
         (if (info.shell_path == "") "" else "export PATH=\"" + info.shell_path + ":$PATH\"\n") +
         """
-          make distclean
+          [ -f Makefile ] && make distclean
           {
-            ./configure """ + quote("--prefix=$PWD/" + platform) + " " + Bash.strings(options) + """
+            ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
+            rm -rf target
             make compiler && make compiler && make install
           } || { echo "Build failed" >&2; exit 2; }
         """,
-        progress_stdout = progress.echo(_),
-        progress_stderr = progress.echo(_)).check
+      progress_stdout = progress.echo(_),
+      progress_stderr = progress.echo(_)).check
+
+
+    val target = Path.explode(platform)
 
     if (target.file.exists) {
       if (target.backup.file.exists) Isabelle_System.rm_tree(target.backup)
@@ -93,8 +97,8 @@
     Isabelle_System.mkdirs(target)
 
     for {
-      d <- List("bin", "lib")
-      dir = source + Path.explode(platform) + Path.explode(d)
+      d <- List("target/bin", "target/lib")
+      dir = source + Path.explode(d)
       entry <- File.read_dir(dir)
     } File.move(dir + Path.explode(entry), target)
 
@@ -109,31 +113,31 @@
     Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
     {
       Command_Line.tool0 {
-        var multilib = false
         var options = List.empty[String]
         var platform = default_platform
 
         val getopts = Getopts("""
-Usage: isabelle build_polyml [OPTIONS] SOURCE
+Usage: isabelle build_polyml [OPTIONS] [SOURCE]
 
   Options are:
-    -M           compile for 32bit multilib (for x86-linux on x86_64-linux)
     -O OPTS...   additional options ./configure (e.g. --with-gmp)
     -p PLATFORM  platform identifier and target directory
 
-  Build Poly/ML in SOURCE directory for given PLATFORM (default: """ + default_platform + """).
+  Build Poly/ML in SOURCE directory (default: .) for
+  given PLATFORM (default: """ + default_platform + """).
 """,
-          "M" -> (_ => multilib = true),
           "O:" -> (arg => options = options ::: List(arg)),
           "p:" -> (arg => platform = arg))
 
         val more_args = getopts(args)
-        more_args match {
-          case List(source) =>
-            build_polyml(Path.explode(source), progress = new Console_Progress,
-              platform = platform, multilib = multilib, options = options)
-          case _ => getopts.usage()
-        }
+        val source =
+          more_args match {
+            case Nil => Path.current
+            case List(source) => Path.explode(source)
+            case _ => getopts.usage()
+          }
+        build_polyml(source,
+          progress = new Console_Progress, platform = platform, options = options)
       }
     }, admin = true)
 }