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