build sha1 library;

--- a/src/Pure/Admin/build_polyml.scala	Fri Nov 11 16:10:46 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Fri Nov 11 16:49:59 2016 +0100
@@ -58,6 +58,7 @@
 
   def build_polyml(
     root: Path,
+    sha1_root: Option[Path] = None,
     progress: Progress = Ignore_Progress,
     arch_64: Boolean = false,
     options: List[String] = Nil,
@@ -78,6 +79,14 @@
       error("Windows requires other bash (for msys)")
 
 
+    /* bash */
+
+    def bash(cwd: Path, script: String, echo: Boolean = false): Process_Result =
+      progress.bash(
+        if (other_bash == "") script else Bash.string(other_bash) + " -c " + Bash.string(script),
+        cwd = cwd.file, env = null, echo = echo)
+
+
     /* configure and make */
 
     val configure_options =
@@ -85,7 +94,7 @@
         info.options_multilib
        else info.options) ::: List("--enable-intinf-as-int") ::: options
 
-    val script =
+    bash(root,
       info.setup + "\n" +
       """
         [ -f Makefile ] && make distclean
@@ -94,23 +103,29 @@
           rm -rf target
           make compiler && make compiler && make install
         } || { echo "Build failed" >&2; exit 2; }
-      """
+      """, echo = true).check
 
-    Isabelle_System.bash(
-      if (other_bash == "") script else Bash.string(other_bash) + " -c " + Bash.string(script),
-      cwd = root.file, env = null,
-      progress_stdout = progress.echo(_),
-      progress_stderr = progress.echo(_)).check
-
-    val lib_files =
+    val ldd_files =
       if (Platform.is_linux) {
-        val libs = Isabelle_System.bash("ldd target/bin/poly", cwd = root.file).check.out_lines
+        val libs = bash(root, "ldd target/bin/poly").check.out_lines
         val Pattern = """\s*libgmp.*=>\s*(\S+).*""".r
         for (Pattern(lib) <- libs) yield lib
       }
       else Nil
 
 
+    /* sha1 library */
+
+    val sha1_files =
+      if (sha1_root.isDefined) {
+        val dir1 = sha1_root.get
+        bash(dir1, "./build " + platform, echo = true).check
+        val dir2 = dir1 + Path.explode(platform)
+        File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
+      }
+      else Nil
+
+
     /* target */
 
     val target = Path.explode(platform)
@@ -123,7 +138,7 @@
       entry <- File.read_dir(dir)
     } File.move(dir + Path.explode(entry), target)
 
-    for (file <- "~~/Admin/polyml/polyi" :: info.copy_files ::: lib_files)
+    for (file <- "~~/Admin/polyml/polyi" :: info.copy_files ::: ldd_files ::: sha1_files)
       File.copy(Path.explode(file), target)
   }
 
@@ -135,6 +150,7 @@
     Command_Line.tool0 {
       var other_bash = ""
       var arch_64 = false
+      var sha1_root: Option[Path] = None
 
       val getopts = Getopts("""
 Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
@@ -142,6 +158,7 @@
   Options are:
     -b EXE       other bash executable (notably for msys on Windows)
     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
+    -s DIR       root directory for sha1 library
 
   Build Poly/ML in its source ROOT directory of its sources, with additional
   CONFIGURE_OPTIONS (e.g. --with-gmp).
@@ -152,7 +169,8 @@
             case "32" | "x86" => arch_64 = false
             case "64" | "x86_64" => arch_64 = true
             case bad => error("Bad processor architecture: " + quote(bad))
-          })
+          },
+        "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
 
       val more_args = getopts(args)
       val (root, options) =
@@ -160,8 +178,8 @@
           case root :: options => (Path.explode(root), options)
           case Nil => getopts.usage()
         }
-      build_polyml(root, progress = new Console_Progress, arch_64 = arch_64, options = options,
-          other_bash = other_bash)
+      build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
+        arch_64 = arch_64, options = options, other_bash = other_bash)
     }
   }
 }