src/Pure/Admin/build_polyml.scala
author wenzelm
Thu, 10 Nov 2016 22:06:36 +0100
changeset 64483 bba1d341bdf6
child 64484 784e28e4dc57
permissions -rw-r--r--
build_polyml in Scala;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64483
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/build_polyml.scala
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
     3
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
     4
Build Poly/ML from sources.
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
     5
*/
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
     6
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
     8
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
     9
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    10
object Build_PolyML
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    11
{
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    12
  sealed case class Platform_Info(
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    13
    options: List[String] = Nil,
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    14
    options_multilib: List[String] = Nil,
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    15
    shell_path: String = "",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    16
    copy_files: List[String] = Nil)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    17
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    18
  private val platform_info = Map(
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    19
    "x86-linux" ->
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    20
      Platform_Info(
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    21
        options_multilib =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    22
          List("--build=i386", "CFLAGS='-m32 -O3'", "CXXFLAGS='-m32 -O3'", "CCASFLAGS='-m32'")),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    23
    "x86_64-linux" -> Platform_Info(),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    24
    "x86-darwin" ->
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    25
      Platform_Info(
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    26
        options =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    27
          List("--build=i686-darwin", "CFLAGS='-arch i686 -O3 -I../libffi/include'",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    28
            "CXXFLAGS='-arch i686 -O3", "-I../libffi/include'", "CCASFLAGS='-arch i686 -O3'",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    29
            "LDFLAGS='-segprot POLY rwx rwx'")),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    30
    "x86_64-darwin" ->
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    31
      Platform_Info(
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    32
        options =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    33
          List("--build=x86_64-darwin", "CFLAGS='-arch x86_64 -O3 -I../libffi/include'",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    34
            "CXXFLAGS='-arch x86_64 -O3 -I../libffi/include'", "CCASFLAGS='-arch x86_64'",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    35
            "LDFLAGS='-segprot POLY rwx rwx'")),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    36
    "x86-windows" ->
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    37
      Platform_Info(
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    38
        options =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    39
          List("--host=i686-w32-mingw32", "CPPFLAGS='-I/mingw32/include'", "--disable-windows-gui"),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    40
        shell_path = "/mingw32/bin",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    41
        copy_files =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    42
          List("/mingw32/bin/libgcc_s_dw2-1.dll",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    43
            "/mingw32/bin/libgmp-10.dll",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    44
            "/mingw32/bin/libstdc++-6.dll")),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    45
    "x86_64-windows" ->
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    46
      Platform_Info(
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    47
        options =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    48
          List("--host=x86_64-w64-mingw32", "CPPFLAGS='-I/mingw64/include'", "--disable-windows-gui"),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    49
        shell_path = "/mingw64/bin",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    50
        copy_files =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    51
          List("/mingw64/bin/libgcc_s_seh-1.dll",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    52
            "/mingw64/bin/libgmp-10.dll",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    53
            "/mingw64/bin/libstdc++-6.dll")))
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    54
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    55
  lazy val default_platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM32")
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    56
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    57
  def build_polyml(
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    58
    source: Path,
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    59
    progress: Progress = Ignore_Progress,
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    60
    platform: String = default_platform,
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    61
    multilib: Boolean = false,
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    62
    options: List[String] = Nil)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    63
  {
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    64
    source.is_dir || error("Bad source directory: " + source)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    65
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    66
    val info =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    67
      platform_info.get(platform) getOrElse
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    68
        error("Bad platform identifier: " + quote(platform))
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    69
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    70
    val target = Path.explode(platform)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    71
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    72
    val configure_options =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    73
      info.options ::: List("--enable-intinf-as-int") ::: options :::
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    74
      (if (multilib) info.options_multilib else info.options)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    75
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    76
    Isabelle_System.bash(cwd = source.file,
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    77
      script =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    78
        (if (info.shell_path == "") "" else "export PATH=\"" + info.shell_path + ":$PATH\"\n") +
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    79
        """
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    80
          make distclean
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    81
          {
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    82
            ./configure """ + quote("--prefix=$PWD/" + platform) + " " + Bash.strings(options) + """
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    83
            make compiler && make compiler && make install
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    84
          } || { echo "Build failed" >&2; exit 2; }
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    85
        """,
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    86
        progress_stdout = progress.echo(_),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    87
        progress_stderr = progress.echo(_)).check
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    88
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    89
    if (target.file.exists) {
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    90
      if (target.backup.file.exists) Isabelle_System.rm_tree(target.backup)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    91
      File.move(target, target.backup)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    92
    }
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    93
    Isabelle_System.mkdirs(target)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    94
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    95
    for {
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    96
      d <- List("bin", "lib")
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    97
      dir = source + Path.explode(platform) + Path.explode(d)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    98
      entry <- File.read_dir(dir)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
    99
    } File.move(dir + Path.explode(entry), target)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   100
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   101
    for (file <- "~~/Admin/polyml/polyi" :: info.copy_files)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   102
      File.copy(Path.explode(file), target)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   103
  }
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   104
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   105
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   106
  /* Isabelle tool wrapper */
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   107
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   108
  val isabelle_tool =
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   109
    Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   110
    {
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   111
      Command_Line.tool0 {
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   112
        var multilib = false
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   113
        var options = List.empty[String]
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   114
        var platform = default_platform
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   115
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   116
        val getopts = Getopts("""
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   117
Usage: isabelle build_polyml [OPTIONS] SOURCE
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   118
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   119
  Options are:
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   120
    -M           compile for 32bit multilib (for x86-linux on x86_64-linux)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   121
    -O OPTS...   additional options ./configure (e.g. --with-gmp)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   122
    -p PLATFORM  platform identifier and target directory
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   123
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   124
  Build Poly/ML in SOURCE directory for given PLATFORM (default: """ + default_platform + """).
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   125
""",
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   126
          "M" -> (_ => multilib = true),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   127
          "O:" -> (arg => options = options ::: List(arg)),
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   128
          "p:" -> (arg => platform = arg))
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   129
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   130
        val more_args = getopts(args)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   131
        more_args match {
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   132
          case List(source) =>
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   133
            build_polyml(Path.explode(source), progress = new Console_Progress,
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   134
              platform = platform, multilib = multilib, options = options)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   135
          case _ => getopts.usage()
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   136
        }
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   137
      }
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   138
    }, admin = true)
bba1d341bdf6 build_polyml in Scala;
wenzelm
parents:
diff changeset
   139
}