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