src/Pure/Admin/component_polyml.scala
changeset 83138 c66d77fb729e
parent 82720 956ecf2c07a0
equal deleted inserted replaced
83136:b6e117b5d0f0 83138:c66d77fb729e
    68 
    68 
    69     val root = dir.absolute
    69     val root = dir.absolute
    70     val target_dir = root + Path.explode("target")
    70     val target_dir = root + Path.explode("target")
    71 
    71 
    72     progress.echo("Building GMP library ...")
    72     progress.echo("Building GMP library ...")
    73     platform_context.execute(root,
    73     platform_context.bash(
    74       "[ -f Makefile ] && make distclean",
    74       Library.make_lines(
    75       "./configure --disable-static --enable-shared --enable-cxx" +
    75         "set -e",
    76         " --build=" + platform_arch + "-" + platform_os +
    76         "[ -f Makefile ] && make distclean",
    77         """ --prefix="$PWD/target" """ + Bash.strings(options),
    77         "./configure --disable-static --enable-shared --enable-cxx" +
    78       "rm -rf target",
    78           " --build=" + platform_arch + "-" + platform_os +
    79       "make",
    79           """ --prefix="$PWD/target" """ + Bash.strings(options),
    80       "make check",
    80         "rm -rf target",
    81       "make install")
    81         "make",
       
    82         "make check",
       
    83         "make install"), cwd = root).check
    82 
    84 
    83     if (platform.is_windows) {
    85     if (platform.is_windows) {
    84       val bin_dir = target_dir + Path.explode("bin")
    86       val bin_dir = target_dir + Path.explode("bin")
    85       val lib_dir = target_dir + Path.explode("lib")
    87       val lib_dir = target_dir + Path.explode("lib")
    86       Isabelle_System.copy_dir(bin_dir, lib_dir, direct = true)
    88       Isabelle_System.copy_dir(bin_dir, lib_dir, direct = true)
   141           val s = platform_context.standard_path(dir.absolute) + "/lib"
   143           val s = platform_context.standard_path(dir.absolute) + "/lib"
   142           "export " + v + "=" + quote(s + ":" + "$" + v)
   144           "export " + v + "=" + quote(s + ":" + "$" + v)
   143         case None => ""
   145         case None => ""
   144       }
   146       }
   145 
   147 
   146     platform_context.execute(root,
   148     platform_context.bash(
   147       platform_info.setup,
   149       Library.make_lines(
   148       gmp_setup,
   150         "set -e",
   149       "[ -f Makefile ] && make distclean",
   151         platform_info.setup,
   150       """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
   152         gmp_setup,
   151       "rm -rf target",
   153         "[ -f Makefile ] && make distclean",
   152       "make",
   154         """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
   153       "make install")
   155         "rm -rf target",
       
   156         "make",
       
   157         "make install"), cwd = root).check
   154 
   158 
   155 
   159 
   156     /* sha1 library */
   160     /* sha1 library */
   157 
   161 
   158     val sha1_files =
   162     val sha1_files =
   159       sha1_root match {
   163       sha1_root match {
   160         case Some(dir) =>
   164         case Some(dir) =>
   161           val platform_path = Path.explode(platform.ISABELLE_PLATFORM(windows = true, apple = true))
   165           val platform_path = Path.explode(platform.ISABELLE_PLATFORM(windows = true, apple = true))
   162           val platform_dir = dir + platform_path
   166           val platform_dir = dir + platform_path
   163           platform_context.execute(dir, "./build " + File.bash_path(platform_path))
   167           platform_context.bash("./build " + File.bash_path(platform_path), cwd = dir).check
   164           File.read_dir(platform_dir).map(entry => platform_dir + Path.basic(entry))
   168           File.read_dir(platform_dir).map(entry => platform_dir + Path.basic(entry))
   165         case None => Nil
   169         case None => Nil
   166       }
   170       }
   167 
   171 
   168 
   172