--- a/src/Pure/Admin/build_csdp.scala Sat Oct 10 13:32:27 2020 +0200
+++ b/src/Pure/Admin/build_csdp.scala Sat Oct 10 13:45:04 2020 +0200
@@ -9,88 +9,99 @@
object Build_CSDP
{
- /* 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"
- val component_name = "csdp-6.2.0"
- val source_url = "https://github.com/coin-or/Csdp/archive/releases/6.2.0.tar.gz"
- val windows_url = "https://github.com/coin-or/Csdp/files/2485584/csdp6.2.0win64.zip"
+ /* 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 =
- " * " + platform + ":\n" +
- List("CFLAGS=" + CFLAGS, "LIBS=" + LIBS).map(" " + _).mkString("\n")
+ 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 =>
- (for (line <- split_lines(s))
- yield {
- line.replaceAll("CFLAGS=.*", "CFLAGS=" + CFLAGS)
- .replaceAll("LIBS=.*", "LIBS=" + LIBS)
- }).mkString("\n"))
+ split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n"))
}
}
val build_flags: List[Flags] =
List(
Flags("arm64-linux",
- CFLAGS = "-march=native -mtune=native -Ofast -ansi -Wall -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include",
+ CFLAGS = "-O3 -ansi -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include",
LIBS = "-static -L../lib -lsdp -llapack -lblas -lgfortran -lm"),
- Flags("x86_64-linux", // Ubuntu 16.04 LTS
- CFLAGS = "-march=native -mtune=native -Ofast -ansi -Wall -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include",
+ 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 = "-m64 -Ofast -ansi -Wall -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include",
- LIBS = "-L../lib -lsdp -llapack -lblas -lm"))
+ 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(
- pretend_windows: Boolean = false,
+ download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current)
{
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 is_windows = Platform.is_windows || pretend_windows
-
- val (platform_name, windows_name) =
- if (is_windows) {
- val Windows_Name = """^.*?([^/]+)\.zip$""".r
- val windows_name =
- windows_url match {
- case Windows_Name(name) => name
- case _ => error("Failed to determine base name from " + quote(windows_url))
- }
- ("x86_64-windows", windows_name)
- }
- else {
- val name =
- proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
- .getOrElse(error("No 64bit platform"))
- (name, "")
- }
+ 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 */
+ /* download source */
- val archive_path = tmp_dir + Path.basic("src.tar.gz")
- Isabelle_System.download(source_url, archive_path, progress = progress)
+ 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
- Isabelle_System.bash("tar xzf src.tar.gz", cwd = tmp_dir.file).check
val source_name =
- File.read_dir(tmp_dir).filterNot(_ == "src.tar.gz") match {
- case List(name) => name
- case _ => error("Exactly one entry expected in archive " + quote(source_url))
+ 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",
@@ -99,30 +110,22 @@
/* build */
- if (is_windows) {
- Isabelle_System.download(windows_url, tmp_dir + Path.basic("windows.zip"),
- progress = progress)
- Isabelle_System.bash("unzip -x windows", cwd = tmp_dir.file).check
+ progress.echo("Building CSDP ...")
- val windows_dir = tmp_dir + Path.explode(windows_name)
- File.copy(windows_dir + Path.explode("LICENSE"), component_dir)
- File.copy(windows_dir + Path.explode("bin/csdp.exe"), platform_dir)
- File.set_executable(platform_dir + Path.basic("csdp.exe"), true)
+ 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)))
}
- else {
- progress.echo("Building CSDP ...")
+ Isabelle_System.bash("make",
+ cwd = build_dir.file,
+ progress_stdout = progress.echo_if(verbose, _),
+ progress_stderr = progress.echo_if(verbose, _)).check
- 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) => flags.change(build_dir + Path.basic("Makefile"))
- }
- Isabelle_System.bash("make",
- cwd = build_dir.file,
- progress_stdout = progress.echo_if(verbose, _),
- progress_stderr = progress.echo_if(verbose, _)).check
- File.copy(build_dir + Path.explode("solver/csdp"), platform_dir)
- }
+ File.copy(build_dir + Path.explode("LICENSE"), component_dir)
+ File.copy(build_dir + Path.explode("solver/csdp"), platform_dir)
/* settings */
@@ -138,18 +141,17 @@
/* README */
File.write(component_dir + Path.basic("README"),
-"""This distribution of CSDP is based on the official downloads:
-""" + source_url + """
-""" + windows_url + """
+"""This is CSDP """ + version + """ from
+""" + download_url + """
-For Linux and macOS, it has been built from sources using the following
-options in the Makefile:
+Makefile flags have been changed for various platforms as follows:
""" + build_flags.map(_.print).mkString("\n\n") + """
+The distribution has been built like this:
-For Windows, the existing binary distribution has been used.
+ cd src && make
-Only the bare "csdp" program is required for Isabelle.
+Only the bare "solver/csdp" program is used for Isabelle.
Makarius
@@ -165,7 +167,7 @@
args =>
{
var target_dir = Path.current
- var pretend_windows = false
+ var download_url = default_download_url
var verbose = false
val getopts = Getopts("""
@@ -173,13 +175,14 @@
Options are:
-D DIR target directory (default ".")
- -W pretend that platform is Windows: download binary, no build
+ -U URL download URL
+ (default: """" + default_download_url + """")
-v verbose
Build prover component from official downloads.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
- "W" -> (_ => pretend_windows = true),
+ "U:" -> (arg => download_url = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -187,7 +190,7 @@
val progress = new Console_Progress()
- build_csdp(pretend_windows = pretend_windows, verbose = verbose, progress = progress,
+ build_csdp(download_url = download_url, verbose = verbose, progress = progress,
target_dir = target_dir)
})
}