1/*  Title:      Pure/Admin/build_polyml.scala
2    Author:     Makarius
3
4Build Poly/ML from sources.
5*/
6
7package isabelle
8
9
10import scala.util.matching.Regex
11
12
13object Build_PolyML
14{
15  /** platform-specific build **/
16
17  sealed case class Platform_Info(
18    options: List[String] = Nil,
19    setup: String = "",
20    copy_files: List[String] = Nil,
21    ldd_pattern: Option[(String, Regex)] = None)
22
23  private val platform_info = Map(
24    "linux" ->
25      Platform_Info(
26        options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
27        ldd_pattern = Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r))),
28    "darwin" ->
29      Platform_Info(
30        options =
31          List("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include",
32            "CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64",
33            "LDFLAGS=-segprot POLY rwx rwx"),
34        setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
35        ldd_pattern = Some(("otool -L", """\s*(\S+lib(?:polyml|gmp).*dylib).*""".r))),
36    "windows" ->
37      Platform_Info(
38        options =
39          List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
40        setup =
41          """PATH=/usr/bin:/bin:/mingw64/bin
42            export CONFIG_SITE=/mingw64/etc/config.site""",
43        copy_files =
44          List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll",
45            "$MSYS/mingw64/bin/libgmp-10.dll",
46            "$MSYS/mingw64/bin/libstdc++-6.dll",
47            "$MSYS/mingw64/bin/libwinpthread-1.dll")))
48
49  def build_polyml(
50    root: Path,
51    sha1_root: Option[Path] = None,
52    progress: Progress = No_Progress,
53    arch_64: Boolean = false,
54    options: List[String] = Nil,
55    msys_root: Option[Path] = None)
56  {
57    if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
58      error("Bad Poly/ML root directory: " + root)
59
60    val platform_arch = if (arch_64) "x86_64" else "x86_64_32"
61    val platform_os = Platform.os_name
62
63    val platform = platform_arch + "-" + platform_os
64    val platform_64 = "x86_64-" + platform_os
65
66    val info =
67      platform_info.get(platform_os) getOrElse
68        error("Bad OS platform: " + quote(platform_os))
69
70    val settings =
71      msys_root match {
72        case None if Platform.is_windows =>
73          error("Windows requires specification of msys root directory")
74        case None => Isabelle_System.settings()
75        case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode)
76      }
77
78    if (Platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) {
79      error("""Missing "chrpath" executable on Linux""")
80    }
81
82
83    /* bash */
84
85    def bash(
86      cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
87    {
88      val script1 =
89        msys_root match {
90          case None => script
91          case Some(msys) =>
92            File.bash_path(msys + Path.explode("usr/bin/bash")) + " -c " + Bash.string(script)
93        }
94      progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo)
95    }
96
97
98    /* configure and make */
99
100    val configure_options =
101      List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") :::
102        info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit"))
103
104    bash(root,
105      info.setup + "\n" +
106      """
107        [ -f Makefile ] && make distclean
108        {
109          ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
110          rm -rf target
111          make compiler && make compiler && make install
112        } || { echo "Build failed" >&2; exit 2; }
113      """, redirect = true, echo = true).check
114
115    val ldd_files =
116    {
117      info.ldd_pattern match {
118        case Some((ldd, pattern)) =>
119          val lines = bash(root, ldd + " target/bin/poly").check.out_lines
120          for { line <- lines; List(lib) <- pattern.unapplySeq(line) } yield lib
121        case None => Nil
122      }
123    }
124
125
126    /* sha1 library */
127
128    val sha1_files =
129      if (sha1_root.isDefined) {
130        val dir1 = sha1_root.get
131        bash(dir1, "./build " + platform_64, redirect = true, echo = true).check
132
133        val dir2 = dir1 + Path.explode(platform_64)
134        File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
135      }
136      else Nil
137
138
139    /* target */
140
141    val target = Path.explode(platform)
142    Isabelle_System.rm_tree(target)
143    Isabelle_System.mkdirs(target)
144
145    for (file <- info.copy_files ::: ldd_files ::: sha1_files)
146      File.copy(Path.explode(file).expand_env(settings), target)
147
148    for {
149      d <- List("target/bin", "target/lib")
150      dir = root + Path.explode(d)
151      entry <- File.read_dir(dir)
152    } File.move(dir + Path.explode(entry), target)
153
154
155    /* poly: library path */
156
157    if (Platform.is_linux) {
158      bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check
159    }
160    else if (Platform.is_macos) {
161      for (file <- ldd_files) {
162        bash(target,
163          """install_name_tool -change """ + Bash.string(file) + " " +
164            Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check
165      }
166    }
167
168
169    /* polyc: directory prefix */
170
171    {
172      val polyc_path = target + Path.explode("polyc")
173
174      val Header = "#! */bin/sh".r
175      val polyc_patched =
176        split_lines(File.read(polyc_path)) match {
177          case Header() :: lines =>
178            val lines1 =
179              lines.map(line =>
180                if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
181                else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
182                else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
183                else line)
184            cat_lines("#!/usr/bin/env bash" ::lines1)
185          case lines =>
186            error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
187        }
188      File.write(polyc_path, polyc_patched)
189    }
190  }
191
192
193
194  /** skeleton for component **/
195
196  private def extract_sources(source_archive: Path, component_dir: Path) =
197  {
198    if (source_archive.get_ext == "zip") {
199      Isabelle_System.bash(
200        "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check
201    }
202    else {
203      Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
204    }
205
206    val src_dir = component_dir + Path.explode("src")
207    File.read_dir(component_dir) match {
208      case List(s) => File.move(component_dir + Path.basic(s), src_dir)
209      case _ => error("Source archive contains multiple directories")
210    }
211
212    val lines = split_lines(File.read(src_dir + Path.explode("RootX86.ML")))
213    val ml_files =
214      for {
215        line <- lines
216        rest <- Library.try_unprefix("use", line)
217      } yield "ML_file" + rest
218
219    File.write(src_dir + Path.explode("ROOT.ML"),
220"""(* Poly/ML Compiler root file.
221
222When this file is open in the Prover IDE, the ML files of the Poly/ML
223compiler can be explored interactively. This is a separate copy: it does
224not affect the running ML session. *)
225""" + ml_files.mkString("\n", "\n", "\n"))
226  }
227
228  def build_polyml_component(
229    source_archive: Path,
230    component_dir: Path,
231    sha1_root: Option[Path] = None)
232  {
233    if (component_dir.is_file || component_dir.is_dir)
234      error("Component directory already exists: " + component_dir)
235
236    Isabelle_System.mkdirs(component_dir)
237    extract_sources(source_archive, component_dir)
238
239    File.copy(Path.explode("~~/Admin/polyml/README"), component_dir)
240
241    val etc_dir = component_dir + Path.explode("etc")
242    Isabelle_System.mkdirs(etc_dir)
243    File.copy(Path.explode("~~/Admin/polyml/settings"), etc_dir)
244
245    sha1_root match {
246      case Some(dir) =>
247        Mercurial.repository(dir).archive(File.standard_path(component_dir + Path.explode("sha1")))
248      case None =>
249    }
250  }
251
252
253
254  /** Isabelle tool wrappers **/
255
256  val isabelle_tool1 =
257    Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
258    {
259      Command_Line.tool0 {
260        var msys_root: Option[Path] = None
261        var arch_64 = false
262        var sha1_root: Option[Path] = None
263
264        val getopts = Getopts("""
265Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
266
267  Options are:
268    -M DIR       msys root directory (for Windows)
269    -m ARCH      processor architecture (32=x86_64_32, 64=x86_64, default: 32)
270    -s DIR       sha1 sources, see https://isabelle.sketis.net/repos/sha1
271
272  Build Poly/ML in the ROOT directory of its sources, with additional
273  CONFIGURE_OPTIONS (e.g. --without-gmp).
274""",
275          "M:" -> (arg => msys_root = Some(Path.explode(arg))),
276          "m:" ->
277            {
278              case "32" | "x86_64_32" => arch_64 = false
279              case "64" | "x86_64" => arch_64 = true
280              case bad => error("Bad processor architecture: " + quote(bad))
281            },
282          "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
283
284        val more_args = getopts(args)
285        val (root, options) =
286          more_args match {
287            case root :: options => (Path.explode(root), options)
288            case Nil => getopts.usage()
289          }
290        build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
291          arch_64 = arch_64, options = options, msys_root = msys_root)
292      }
293    })
294
295  val isabelle_tool2 =
296    Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args =>
297    {
298      Command_Line.tool0 {
299        var sha1_root: Option[Path] = None
300
301        val getopts = Getopts("""
302Usage: isabelle build_polyml_component [OPTIONS] SOURCE_ARCHIVE COMPONENT_DIR
303
304  Options are:
305    -s DIR       sha1 sources, see https://isabelle.sketis.net/repos/sha1
306
307  Make skeleton for Poly/ML component, based on official source archive
308  (zip or tar.gz).
309""",
310          "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
311
312        val more_args = getopts(args)
313
314        val (source_archive, component_dir) =
315          more_args match {
316            case List(archive, dir) => (Path.explode(archive), Path.explode(dir))
317            case _ => getopts.usage()
318          }
319        build_polyml_component(source_archive, component_dir, sha1_root = sha1_root)
320      }
321    })
322}
323