diff --git a/src/Pure/Admin/build_csdp.scala b/src/Pure/Admin/build_csdp.scala --- a/src/Pure/Admin/build_csdp.scala +++ b/src/Pure/Admin/build_csdp.scala @@ -1,217 +1,216 @@ /* Title: Pure/Admin/build_csdp.scala Author: Makarius Build Isabelle CSDP component from official downloads. */ package isabelle object Build_CSDP { // Note: version 6.2.0 does not quite work for the "sos" proof method val default_download_url = "https://github.com/coin-or/Csdp/archive/releases/6.1.1.tar.gz" /* flags */ sealed case class Flags(platform: String, CFLAGS: String = "", LIBS: String = "") { val changed: List[(String, String)] = List("CFLAGS" -> CFLAGS, "LIBS" -> LIBS).filter(p => p._2.nonEmpty) def print: String = if (changed.isEmpty) "" else " * " + platform + ":\n" + changed.map(p => " " + p._1 + "=" + p._2).mkString("\n") def change(path: Path) { def change_line(line: String, entry: (String, String)): String = line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2) File.change(path, s => split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n")) } } val build_flags: List[Flags] = List( Flags("arm64-linux", CFLAGS = "-O3 -ansi -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include", LIBS = "-static -L../lib -lsdp -llapack -lblas -lgfortran -lm"), Flags("x86_64-linux", CFLAGS = "-O3 -ansi -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include", LIBS = "-static -L../lib -lsdp -llapack -lblas -lgfortran -lquadmath -lm"), Flags("x86_64-darwin", CFLAGS = "-O3 -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include", LIBS = "-L../lib -lsdp -llapack -lblas -lm"), Flags("x86_64-windows")) /* build CSDP */ def build_csdp( download_url: String = default_download_url, verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current, - mingw_context: MinGW.Context = MinGW.none) + mingw: MinGW = MinGW.none) { - mingw_context.check + mingw.check Isabelle_System.with_tmp_dir("build")(tmp_dir => { /* component */ val Archive_Name = """^.*?([^/]+)$""".r val Version = """^[^0-9]*([0-9].*)\.tar.gz$""".r val archive_name = download_url match { case Archive_Name(name) => name case _ => error("Failed to determine source archive name from " + quote(download_url)) } val version = archive_name match { case Version(version) => version case _ => error("Failed to determine component version from " + quote(archive_name)) } val component_name = "csdp-" + version val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name)) progress.echo("Component " + component_dir) /* platform */ val platform_name = proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse error("No 64bit platform") val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download(download_url, archive_path, progress = progress) Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check val source_name = File.read_dir(tmp_dir).filter(name => (tmp_dir + Path.basic(name)).is_dir) match { case List(dir) => dir case dirs => error("Exactly one directory entry expected in archive " + quote(download_url) + "\n" + commas_quote(dirs)) } Isabelle_System.bash( "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src", cwd = component_dir.file).check /* build */ progress.echo("Building CSDP ...") val build_dir = tmp_dir + Path.basic(source_name) build_flags.find(flags => flags.platform == platform_name) match { case None => error("No build flags for platform " + quote(platform_name)) case Some(flags) => File.find_files(build_dir.file, pred = file => file.getName == "Makefile"). foreach(file => flags.change(File.path(file))) } - progress.bash(mingw_context.bash_command("make"), - cwd = build_dir.file, echo = verbose).check + progress.bash(mingw.bash_command("make"), cwd = build_dir.file, echo = verbose).check /* install */ File.copy(build_dir + Path.explode("LICENSE"), component_dir) if (!Platform.is_windows) { File.copy(build_dir + Path.explode("solver/csdp"), platform_dir) } else { File.copy(build_dir + Path.explode("solver/csdp.exe"), platform_dir) val libs = List("libblas", "liblapack", "libgfortran-5", "libgcc_s_seh-1", "libquadmath-0", "libwinpthread-1") for (name <- libs) { - File.copy(mingw_context.get_root + Path.explode("mingw64/bin") + Path.basic(name).ext("dll"), + File.copy(mingw.get_root + Path.explode("mingw64/bin") + Path.basic(name).ext("dll"), platform_dir) } } /* settings */ val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) File.write(etc_dir + Path.basic("settings"), """# -*- shell-script -*- :mode=shellscript: ISABELLE_CSDP="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/csdp" """) /* README */ File.write(component_dir + Path.basic("README"), """This is CSDP """ + version + """ from """ + download_url + """ Makefile flags have been changed for various platforms as follows: """ + build_flags.map(_.print).mkString("\n\n") + """ The distribution has been built like this: cd src && make Only the bare "solver/csdp" program is used for Isabelle. Makarius """ + Date.Format.date(Date.now()) + "\n") }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_csdp", "build prover component from official downloads", args => { var target_dir = Path.current - var mingw_context = MinGW.none + var mingw = MinGW.none var download_url = default_download_url var verbose = false val getopts = Getopts(""" Usage: isabelle build_csdp [OPTIONS] Options are: -D DIR target directory (default ".") -M DIR msys/mingw root directory (for Windows) -U URL download URL (default: """" + default_download_url + """") -v verbose Build prover component from official downloads. """, "D:" -> (arg => target_dir = Path.explode(arg)), - "M:" -> (arg => mingw_context = MinGW.context(Path.explode(arg))), + "M:" -> (arg => mingw = MinGW.root(Path.explode(arg))), "U:" -> (arg => download_url = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_csdp(download_url = download_url, verbose = verbose, progress = progress, - target_dir = target_dir, mingw_context = mingw_context) + target_dir = target_dir, mingw = mingw) }) } diff --git a/src/Pure/System/mingw.scala b/src/Pure/System/mingw.scala --- a/src/Pure/System/mingw.scala +++ b/src/Pure/System/mingw.scala @@ -1,52 +1,52 @@ /* Title: Pure/System/mingw.scala Author: Makarius Support for MSYS2/MinGW64 on Windows. */ package isabelle object MinGW { - val none: Context = new Context(None) - def context(root: Path) = new Context(Some(root)) - def environment: List[(String, String)] = List("PATH" -> "/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE" -> "/mingw64/etc/config.site") def environment_prefix: String = (for ((a, b) <- environment) yield Bash.string(a) + "=" + Bash.string(b)) .mkString("/usr/bin/env ", " ", " ") - class Context private[MinGW](val root: Option[Path]) - { - override def toString: String = - root match { - case None => "MinGW.none" - case Some(msys_root) => "MinGW.context(" + msys_root.toString + ")" - } + val none: MinGW = new MinGW(None) + def root(path: Path) = new MinGW(Some(path)) +} - def bash_command(command: String): String = - root match { - case None => command - case Some(msys_root) => - File.bash_path(msys_root + Path.explode("usr/bin/bash")) + - " -c " + Bash.string(environment_prefix + command) - } +class MinGW private(val root: Option[Path]) +{ + override def toString: String = + root match { + case None => "MinGW.none" + case Some(msys_root) => "MinGW.root(" + msys_root.toString + ")" + } - def get_root: Path = - if (!Platform.is_windows) error("Windows platform required") - else if (root.isEmpty) error("Windows platform needs specification of msys root directory") - else root.get + def bash_command(command: String): String = + root match { + case None => command + case Some(msys_root) => + File.bash_path(msys_root + Path.explode("usr/bin/bash")) + + " -c " + Bash.string(MinGW.environment_prefix + command) + } - def check - { - if (Platform.is_windows) { - get_root - val result = Isabelle_System.bash(bash_command("uname -s")).check - if (!result.out.startsWith("MSYS")) error("Bad msys installation " + get_root) - } + def get_root: Path = + if (!Platform.is_windows) error("Windows platform required") + else if (root.isEmpty) error("Windows platform needs specification of msys root directory") + else root.get + + def check + { + if (Platform.is_windows) { + get_root + val result = Isabelle_System.bash(bash_command("uname -s")).check + if (!result.out.startsWith("MSYS")) error("Bad msys installation " + get_root) } } }