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,201 +1,200 @@ /* Title: Pure/Admin/build_csdp.scala Author: Makarius Build Isabelle CSDP component from official download. */ 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: Option[String] = if (changed.isEmpty) None else Some(" * " + platform + ":\n" + changed.map(p => " " + Properties.Eq(p)) .mkString("\n")) def change(path: Path): Unit = { def change_line(line: String, p: (String, String)): String = line.replaceAll(p._1 + "=.*", Properties.Eq(p)) File.change_lines(path) { _.map(line => changed.foldLeft(line)(change_line)) } } } 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: MinGW = MinGW.none ): Unit = { 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 = Components.Directory.create(target_dir + Path.basic(component_name), progress = progress) /* 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 + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download_file(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.get_dir(tmp_dir) + val source_dir = File.get_dir(tmp_dir, title = archive_name) Isabelle_System.bash( - "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src", + "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src", cwd = component_dir.path.file).check /* build */ progress.echo("Building CSDP for " + platform_name + " ...") - 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"). + File.find_files(source_dir.file, pred = file => file.getName == "Makefile"). foreach(file => flags.change(File.path(file))) } - progress.bash(mingw.bash_script("make"), cwd = build_dir.file, echo = verbose).check + progress.bash(mingw.bash_script("make"), cwd = source_dir.file, echo = verbose).check /* install */ - Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path) - Isabelle_System.copy_file(build_dir + Path.explode("solver/csdp").platform_exe, platform_dir) + Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path) + Isabelle_System.copy_file(source_dir + Path.explode("solver/csdp").platform_exe, platform_dir) if (Platform.is_windows) { Executable.libraries_closure(platform_dir + Path.explode("csdp.exe"), mingw = mingw, filter = Set("libblas", "liblapack", "libgfortran", "libgcc_s_seh", "libquadmath", "libwinpthread")) } /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_CSDP="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/csdp" """) /* README */ File.write(component_dir.README, """This is CSDP """ + version + """ from """ + download_url + """ Makefile flags have been changed for various platforms as follows: """ + build_flags.flatMap(_.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 download", Scala_Project.here, { args => var target_dir = Path.current 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 specification for Windows -U URL download URL (default: """" + default_download_url + """") -v verbose Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg)), "M:" -> (arg => mingw = MinGW(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 = mingw) }) } diff --git a/src/Pure/Admin/build_easychair.scala b/src/Pure/Admin/build_easychair.scala --- a/src/Pure/Admin/build_easychair.scala +++ b/src/Pure/Admin/build_easychair.scala @@ -1,108 +1,102 @@ /* Title: Pure/Admin/build_easychair.scala Author: Makarius Build Isabelle component for Easychair LaTeX style. See also https://easychair.org/publications/for_authors */ package isabelle object Build_Easychair { /* build easychair component */ val default_url = "https://easychair.org/publications/easychair.zip" def build_easychair( download_url: String = default_url, target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { Isabelle_System.require_command("unzip", test = "-h") Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => Isabelle_System.with_tmp_dir("download") { download_dir => /* download */ Isabelle_System.download_file(download_url, download_file, progress = progress) Isabelle_System.bash("unzip -x " + File.bash_path(download_file), cwd = download_dir.file).check - val easychair_dir = - File.read_dir(download_dir) match { - case List(name) => download_dir + Path.explode(name) - case bad => - error("Expected exactly one directory entry in " + download_file + - bad.mkString("\n", "\n ", "")) - } + val easychair_dir = File.get_dir(download_dir, title = download_url) /* component */ val version = Library.try_unprefix("EasyChair", easychair_dir.file_name) .getOrElse("Failed to detect version from " + quote(easychair_dir.file_name)) val component = "easychair-" + version val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) Isabelle_System.rm_tree(component_dir.path) Isabelle_System.copy_dir(easychair_dir, component_dir.path) Isabelle_System.make_directory(component_dir.etc) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_EASYCHAIR_HOME="$COMPONENT" """) /* README */ File.write(component_dir.README, """This is the Easychair style for authors from """ + download_url + """ Makarius """ + Date.Format.date(Date.now()) + "\n") } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_easychair", "build component for Easychair LaTeX style", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_url val getopts = Getopts(""" Usage: isabelle build_easychair [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") Build component for Easychair LaTeX style. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_easychair(download_url = download_url, target_dir = target_dir, progress = progress) }) } diff --git a/src/Pure/Admin/build_foiltex.scala b/src/Pure/Admin/build_foiltex.scala --- a/src/Pure/Admin/build_foiltex.scala +++ b/src/Pure/Admin/build_foiltex.scala @@ -1,117 +1,111 @@ /* Title: Pure/Admin/build_foiltex.scala Author: Makarius Build Isabelle component for FoilTeX. See also https://ctan.org/pkg/foiltex */ package isabelle object Build_Foiltex { /* build FoilTeX component */ val default_url = "https://mirrors.ctan.org/macros/latex/contrib/foiltex.zip" def build_foiltex( download_url: String = default_url, target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { Isabelle_System.require_command("unzip", test = "-h") Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => Isabelle_System.with_tmp_dir("download") { download_dir => /* download */ Isabelle_System.download_file(download_url, download_file, progress = progress) Isabelle_System.bash("unzip -x " + File.bash_path(download_file), cwd = download_dir.file).check - val foiltex_dir = - File.read_dir(download_dir) match { - case List(name) => download_dir + Path.explode(name) - case bad => - error("Expected exactly one directory entry in " + download_file + - bad.mkString("\n", "\n ", "")) - } + val foiltex_dir = File.get_dir(download_dir, title = download_url) val README = Path.explode("README") val README_flt = Path.explode("README.flt") Isabelle_System.move_file(foiltex_dir + README, foiltex_dir + README_flt) Isabelle_System.bash("pdflatex foiltex.ins", cwd = foiltex_dir.file).check /* component */ val version = { val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r split_lines(File.read(foiltex_dir + README_flt)) .collectFirst({ case Version(v) => v }) .getOrElse(error("Failed to detect version in " + README_flt)) } val component = "foiltex-" + version val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) Isabelle_System.rm_tree(component_dir.path) Isabelle_System.copy_dir(foiltex_dir, component_dir.path) Isabelle_System.make_directory(component_dir.etc) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_FOILTEX_HOME="$COMPONENT" """) /* README */ File.write(component_dir.README, """This is FoilTeX from """ + download_url + """ Makarius """ + Date.Format.date(Date.now()) + "\n") } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_foiltex", "build component for FoilTeX", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_url val getopts = Getopts(""" Usage: isabelle build_foiltex [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") Build component for FoilTeX: slides in LaTeX. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_foiltex(download_url = download_url, target_dir = target_dir, progress = progress) }) } diff --git a/src/Pure/Admin/build_jdk.scala b/src/Pure/Admin/build_jdk.scala --- a/src/Pure/Admin/build_jdk.scala +++ b/src/Pure/Admin/build_jdk.scala @@ -1,234 +1,229 @@ /* Title: Pure/Admin/build_jdk.scala Author: Makarius Build Isabelle jdk component from original platform installations. */ package isabelle import java.io.{File => JFile} import java.nio.file.Files import java.nio.file.attribute.PosixFilePermission import scala.util.matching.Regex object Build_JDK { /* platform and version information */ sealed case class JDK_Platform( platform_name: String, platform_regex: Regex, exe: String = "java", macos_home: Boolean = false, jdk_version: String = "" ) { override def toString: String = platform_name def platform_path: Path = Path.explode(platform_name) def detect(jdk_dir: Path): Option[JDK_Platform] = { val major_version = { val Major_Version = """.*jdk(\d+).*$""".r val jdk_name = jdk_dir.file.getName jdk_name match { case Major_Version(s) => s case _ => error("Cannot determine major version from " + quote(jdk_name)) } } val path = jdk_dir + Path.explode("bin") + Path.explode(exe) if (path.is_file) { val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out if (platform_regex.matches(file_descr)) { val Version = ("^(" + major_version + """[0-9.+]+)(?:-LTS)?$""").r val version_lines = Isabelle_System.bash("strings " + File.bash_path(path)).check .out_lines.flatMap({ case Version(s) => Some(s) case _ => None }) version_lines match { case List(jdk_version) => Some(copy(jdk_version = jdk_version)) case _ => error("Expected unique version within executable " + path) } } else None } else None } } val templates: List[JDK_Platform] = List( JDK_Platform("arm64-darwin", """.*Mach-O 64-bit.*arm64.*""".r, macos_home = true), JDK_Platform("arm64-linux", """.*ELF 64-bit.*ARM aarch64.*""".r), JDK_Platform("x86_64-darwin", """.*Mach-O 64-bit.*x86[-_]64.*""".r, macos_home = true), JDK_Platform("x86_64-linux", """.*ELF 64-bit.*x86[-_]64.*""".r), JDK_Platform("x86_64-windows", """.*PE32\+ executable.*x86[-_]64.*""".r, exe = "java.exe")) /* README */ def readme(jdk_version: String): String = """This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also https://www.azul.com/downloads/zulu-community/?package=jdk The main license is GPL2, but some modules are covered by other (more liberal) licenses, see legal/* for details. Linux, Windows, macOS all work uniformly, depending on platform-specific subdirectories. """ /* settings */ val settings: String = """# -*- shell-script -*- :mode=shellscript: case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; windows) ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; macos) if [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$COMPONENT/$ISABELLE_APPLE_PLATFORM64" ] then ISABELLE_JAVA_PLATFORM="$ISABELLE_APPLE_PLATFORM64" else ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" fi ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; esac """ /* extract archive */ def extract_archive(dir: Path, archive: Path): JDK_Platform = { try { val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp")) if (archive.get_ext == "zip") { Isabelle_System.bash( "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check } else { Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check } - val dir_entry = - File.read_dir(tmp_dir) match { - case List(s) => s - case _ => error("Archive contains multiple directories") - } + val jdk_dir = File.get_dir(tmp_dir, title = archive.file_name) - val jdk_dir = tmp_dir + Path.explode(dir_entry) val platform = templates.view.flatMap(_.detect(jdk_dir)) .headOption.getOrElse(error("Failed to detect JDK platform")) val platform_dir = dir + platform.platform_path if (platform_dir.is_dir) error("Directory already exists: " + platform_dir) Isabelle_System.move_file(jdk_dir, platform_dir) platform } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) } } /* build jdk */ def build_jdk( archives: List[Path], progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { if (Platform.is_windows) error("Cannot build jdk on Windows") Isabelle_System.with_tmp_dir("jdk") { dir => progress.echo("Extracting ...") val platforms = archives.map(extract_archive(dir, _)) val jdk_version = platforms.map(_.jdk_version).distinct match { case List(version) => version case Nil => error("No archives") case versions => error("Archives contain multiple JDK versions: " + commas_quote(versions)) } templates.filterNot(p1 => platforms.exists(p2 => p1.platform_name == p2.platform_name)) match { case Nil => case missing => error("Missing platforms: " + commas_quote(missing.map(_.platform_name))) } val jdk_name = "jdk-" + jdk_version val jdk_path = Path.explode(jdk_name) val component_dir = Components.Directory.create(dir + jdk_path, progress = progress) File.write(component_dir.settings, settings) File.write(component_dir.README, readme(jdk_version)) for (platform <- platforms) { Isabelle_System.move_file(dir + platform.platform_path, component_dir.path) } for (file <- File.find_files(component_dir.path.file, include_dirs = true)) { val path = file.toPath val perms = Files.getPosixFilePermissions(path) perms.add(PosixFilePermission.OWNER_READ) perms.add(PosixFilePermission.GROUP_READ) perms.add(PosixFilePermission.OTHERS_READ) perms.add(PosixFilePermission.OWNER_WRITE) if (file.isDirectory) { perms.add(PosixFilePermission.OWNER_WRITE) perms.add(PosixFilePermission.OWNER_EXECUTE) perms.add(PosixFilePermission.GROUP_EXECUTE) perms.add(PosixFilePermission.OTHERS_EXECUTE) } Files.setPosixFilePermissions(path, perms) } progress.echo("Archiving ...") Isabelle_System.gnutar( "-czf " + File.bash_path(target_dir + jdk_path.tar.gz) + " " + jdk_name, dir = dir).check } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives", Scala_Project.here, { args => var target_dir = Path.current val getopts = Getopts(""" Usage: isabelle build_jdk [OPTIONS] ARCHIVES... Options are: -D DIR target directory (default ".") Build jdk component from tar.gz archives, with original jdk archives for Linux, Windows, and macOS. """, "D:" -> (arg => target_dir = Path.explode(arg))) val more_args = getopts(args) if (more_args.isEmpty) getopts.usage() val archives = more_args.map(Path.explode) val progress = new Console_Progress() build_jdk(archives = archives, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_llncs.scala b/src/Pure/Admin/build_llncs.scala --- a/src/Pure/Admin/build_llncs.scala +++ b/src/Pure/Admin/build_llncs.scala @@ -1,117 +1,111 @@ /* Title: Pure/Admin/build_llncs.scala Author: Makarius Build Isabelle component for Springer LaTeX LNCS style. See also: - https://ctan.org/pkg/llncs?lang=en - https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines */ package isabelle object Build_LLNCS { /* build llncs component */ val default_url = "https://mirrors.ctan.org/macros/latex/contrib/llncs.zip" def build_llncs( download_url: String = default_url, target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { Isabelle_System.require_command("unzip", test = "-h") Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => Isabelle_System.with_tmp_dir("download") { download_dir => /* download */ Isabelle_System.download_file(download_url, download_file, progress = progress) Isabelle_System.bash("unzip -x " + File.bash_path(download_file), cwd = download_dir.file).check - val llncs_dir = - File.read_dir(download_dir) match { - case List(name) => download_dir + Path.explode(name) - case bad => - error("Expected exactly one directory entry in " + download_file + - bad.mkString("\n", "\n ", "")) - } + val llncs_dir = File.get_dir(download_dir, title = download_url) val readme = Path.explode("README.md") File.change(llncs_dir + readme)(_.replace(" ", "\u00a0")) /* component */ val version = { val Version = """^_.* v(.*)_$""".r split_lines(File.read(llncs_dir + readme)) .collectFirst({ case Version(v) => v }) .getOrElse(error("Failed to detect version in " + readme)) } val component = "llncs-" + version val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) Isabelle_System.rm_tree(component_dir.path) Isabelle_System.copy_dir(llncs_dir, component_dir.path) Isabelle_System.make_directory(component_dir.etc) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_LLNCS_HOME="$COMPONENT" """) /* README */ File.write(component_dir.README, """This is the Springer LaTeX LNCS style for authors from """ + download_url + """ Makarius """ + Date.Format.date(Date.now()) + "\n") } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_llncs", "build component for Springer LaTeX LNCS style", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_url val getopts = Getopts(""" Usage: isabelle build_llncs [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") Build component for Springer LaTeX LNCS style. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_llncs(download_url = download_url, target_dir = target_dir, progress = progress) }) } diff --git a/src/Pure/Admin/build_minisat.scala b/src/Pure/Admin/build_minisat.scala --- a/src/Pure/Admin/build_minisat.scala +++ b/src/Pure/Admin/build_minisat.scala @@ -1,155 +1,154 @@ /* Title: Pure/Admin/build_minisat.scala Author: Makarius Build Isabelle Minisat from sources. */ package isabelle object Build_Minisat { val default_download_url = "https://github.com/stp/minisat/archive/releases/2.2.1.tar.gz" def make_component_name(version: String): String = "minisat-" + version /* build Minisat */ def build_minisat( download_url: String = default_download_url, component_name: String = "", verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ val Archive_Name = """^.*?([^/]+)$""".r val Version = """^v?([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 = proper_string(component_name) getOrElse make_component_name(version) val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) /* platform */ val platform_name = proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse error("No 64bit platform") val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download_file(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.get_dir(tmp_dir) + val source_dir = File.get_dir(tmp_dir, title = download_url) Isabelle_System.bash( - "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src", + "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src", cwd = component_dir.path.file).check /* build */ progress.echo("Building Minisat for " + platform_name + " ...") - val build_dir = tmp_dir + Path.basic(source_name) - Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path) + Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path) if (Platform.is_macos) { - File.change(build_dir + Path.explode("Makefile")) { + File.change(source_dir + Path.explode("Makefile")) { _.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "") } } - progress.bash("make r", build_dir.file, echo = verbose).check + progress.bash("make r", source_dir.file, echo = verbose).check Isabelle_System.copy_file( - build_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir) + source_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir) if (Platform.is_windows) { Isabelle_System.copy_file(Path.explode("/bin/cygwin1.dll"), platform_dir) } /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: MINISAT_HOME="$COMPONENT/$ISABELLE_PLATFORM64" ISABELLE_MINISAT="$MINISAT_HOME/minisat" """) /* README */ File.write(component_dir.README, "This Isabelle component provides Minisat " + version + """ using the sources from """.stripMargin + download_url + """ The executables have been built via "make r"; macOS requires to remove options "--static" and "-Wl,-soname,..." from the Makefile. Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_minisat", "build prover component from sources", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_download_url var component_name = "" var verbose = false val getopts = Getopts(""" Usage: isabelle build_minisat [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_download_url + """") -n NAME component name (default: """" + make_component_name("VERSION") + """") -v verbose Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg), "n:" -> (arg => component_name = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_minisat(download_url = download_url, component_name = component_name, verbose = verbose, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_vampire.scala b/src/Pure/Admin/build_vampire.scala --- a/src/Pure/Admin/build_vampire.scala +++ b/src/Pure/Admin/build_vampire.scala @@ -1,164 +1,163 @@ /* Title: Pure/Admin/build_vampire.scala Author: Makarius Build Isabelle Vampire component from official download. */ package isabelle object Build_Vampire { val default_download_url = "https://github.com/vprover/vampire/archive/refs/tags/v4.6.tar.gz" val default_jobs = 1 def make_component_name(version: String): String = "vampire-" + Library.try_unprefix("v", version).getOrElse(version) /* build Vampire */ def build_vampire( download_url: String = default_download_url, jobs: Int = default_jobs, component_name: String = "", verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { Isabelle_System.require_command("cmake") Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ val Archive_Name = """^.*?([^/]+)$""".r val Version = """^v?([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 = proper_string(component_name) getOrElse make_component_name(version) val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) /* platform */ val platform_name = proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse error("No 64bit platform") val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download_file(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.get_dir(tmp_dir) + val source_dir = File.get_dir(tmp_dir, title = download_url) Isabelle_System.bash( - "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src", + "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src", cwd = component_dir.path.file).check /* build */ progress.echo("Building Vampire for " + platform_name + " ...") - val build_dir = tmp_dir + Path.basic(source_name) - Isabelle_System.copy_file(build_dir + Path.explode("LICENCE"), component_dir.path) + Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir.path) val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else "" val cmake_out = progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""", - cwd = build_dir.file, echo = verbose).check.out + cwd = source_dir.file, echo = verbose).check.out val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r val binary = split_lines(cmake_out).collectFirst({ case Pattern(name) => name }) .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out)) - progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check + progress.bash("make -j" + jobs, cwd = source_dir.file, echo = verbose).check - Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe, + Isabelle_System.copy_file(source_dir + Path.basic("bin") + Path.basic(binary).platform_exe, platform_dir + Path.basic("vampire").platform_exe) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64" ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire" """) /* README */ File.write(component_dir.README, "This Isabelle component provides Vampire " + version + """using the original sources from """.stripMargin + download_url + """ The executables have been built via "cmake . && make" Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_vampire", "build prover component from official download", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_download_url var jobs = default_jobs var component_name = "" var verbose = false val getopts = Getopts(""" Usage: isabelle build_vampire [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_download_url + """") -j NUMBER parallel jobs for make (default: """ + default_jobs + """) -n NAME component name (default: """" + make_component_name("VERSION") + """") -v verbose Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg), "j:" -> (arg => jobs = Value.Nat.parse(arg)), "n:" -> (arg => component_name = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_vampire(download_url = download_url, component_name = component_name, jobs = jobs, verbose = verbose, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_verit.scala b/src/Pure/Admin/build_verit.scala --- a/src/Pure/Admin/build_verit.scala +++ b/src/Pure/Admin/build_verit.scala @@ -1,157 +1,156 @@ /* Title: Pure/Admin/build_csdp.scala Author: Makarius Build Isabelle veriT component from official download. */ package isabelle object Build_VeriT { val default_download_url = "https://verit.loria.fr/rmx/2021.06.2/verit-2021.06.2-rmx.tar.gz" /* build veriT */ def build_verit( download_url: String = default_download_url, verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current, mingw: MinGW = MinGW.none ): Unit = { mingw.check Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ val Archive_Name = """^.*?([^/]+)$""".r val Version = """^[^-]+-(.+)\.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 = "verit-" + version val component_dir = Components.Directory.create(target_dir + Path.basic(component_name), progress = progress) /* 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 + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download_file(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.get_dir(tmp_dir) + val source_dir = File.get_dir(tmp_dir, title = download_url) Isabelle_System.bash( - "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src", + "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src", cwd = component_dir.path.file).check /* build */ progress.echo("Building veriT for " + platform_name + " ...") val configure_options = if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else "" - val build_dir = tmp_dir + Path.basic(source_name) progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"), - cwd = build_dir.file, echo = verbose).check + cwd = source_dir.file, echo = verbose).check /* install */ - Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path) + Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path) val exe_path = Path.basic("veriT").platform_exe - Isabelle_System.copy_file(build_dir + exe_path, platform_dir) + Isabelle_System.copy_file(source_dir + exe_path, platform_dir) Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_VERIT="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/veriT" """) /* README */ File.write(component_dir.README, """This is veriT """ + version + """ from """ + download_url + """ It has been built from sources like this: cd src ./configure make Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_verit", "build prover component from official download", Scala_Project.here, { args => var target_dir = Path.current var mingw = MinGW.none var download_url = default_download_url var verbose = false val getopts = Getopts(""" Usage: isabelle build_verit [OPTIONS] Options are: -D DIR target directory (default ".") -M DIR msys/mingw root specification for Windows -U URL download URL (default: """" + default_download_url + """") -v verbose Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg)), "M:" -> (arg => mingw = MinGW(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_verit(download_url = download_url, verbose = verbose, progress = progress, target_dir = target_dir, mingw = mingw) }) } diff --git a/src/Pure/General/file.scala b/src/Pure/General/file.scala --- a/src/Pure/General/file.scala +++ b/src/Pure/General/file.scala @@ -1,364 +1,377 @@ /* Title: Pure/General/file.scala Author: Makarius File-system operations. */ package isabelle import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, File => JFile, IOException} import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor, FileVisitOption, FileVisitResult} import java.nio.file.attribute.BasicFileAttributes import java.net.{URI, URL, MalformedURLException} import java.util.zip.{GZIPInputStream, GZIPOutputStream} import java.util.EnumSet import org.tukaani.xz import com.github.luben.zstd import scala.collection.mutable object File { /* standard path (Cygwin or Posix) */ def standard_path(path: Path): String = path.expand.implode def standard_path(platform_path: String): String = isabelle.setup.Environment.standard_path(platform_path) def standard_path(file: JFile): String = standard_path(file.getPath) def standard_url(name: String): String = try { val url = new URL(name) if (url.getProtocol == "file" && Url.is_wellformed_file(name)) standard_path(Url.parse_file(name)) else name } catch { case _: MalformedURLException => standard_path(name) } /* platform path (Windows or Posix) */ def platform_path(standard_path: String): String = isabelle.setup.Environment.platform_path(standard_path) def platform_path(path: Path): String = platform_path(standard_path(path)) def platform_file(path: Path): JFile = new JFile(platform_path(path)) /* platform files */ def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile def absolute_name(file: JFile): String = absolute(file).getPath def canonical(file: JFile): JFile = file.getCanonicalFile def canonical_name(file: JFile): String = canonical(file).getPath def path(file: JFile): Path = Path.explode(standard_path(file)) def pwd(): Path = path(Path.current.absolute_file) def uri(file: JFile): URI = file.toURI def uri(path: Path): URI = path.file.toURI def url(file: JFile): URL = uri(file).toURL def url(path: Path): URL = url(path.file) /* adhoc file types */ def is_ML(s: String): Boolean = s.endsWith(".ML") def is_bib(s: String): Boolean = s.endsWith(".bib") def is_dll(s: String): Boolean = s.endsWith(".dll") def is_exe(s: String): Boolean = s.endsWith(".exe") def is_gz(s: String): Boolean = s.endsWith(".gz") def is_html(s: String): Boolean = s.endsWith(".html") def is_jar(s: String): Boolean = s.endsWith(".jar") def is_java(s: String): Boolean = s.endsWith(".java") def is_node(s: String): Boolean = s.endsWith(".node") def is_pdf(s: String): Boolean = s.endsWith(".pdf") def is_png(s: String): Boolean = s.endsWith(".png") def is_thy(s: String): Boolean = s.endsWith(".thy") def is_xz(s: String): Boolean = s.endsWith(".xz") def is_zip(s: String): Boolean = s.endsWith(".zip") def is_zst(s: String): Boolean = s.endsWith(".zst") def is_backup(s: String): Boolean = s.endsWith("~") || s.endsWith(".orig") /* relative paths */ def relative_path(base: Path, other: Path): Option[Path] = { val base_path = base.java_path val other_path = other.java_path if (other_path.startsWith(base_path)) Some(path(base_path.relativize(other_path).toFile)) else None } /* bash path */ def bash_path(path: Path): String = Bash.string(standard_path(path)) def bash_path(file: JFile): String = Bash.string(standard_path(file)) def bash_platform_path(path: Path): String = Bash.string(platform_path(path)) /* directory entries */ def check_dir(path: Path): Path = if (path.is_dir) path else error("No such directory: " + path) def check_file(path: Path): Path = if (path.is_file) path else error("No such file: " + path) /* directory content */ def read_dir(dir: Path): List[String] = { if (!dir.is_dir) error("No such directory: " + dir.toString) val files = dir.file.listFiles if (files == null) Nil else files.toList.map(_.getName).sorted } - def get_dir(dir: Path): String = - read_dir(dir).filter(name => (dir + Path.basic(name)).is_dir) match { - case List(entry) => entry - case dirs => - error("Exactly one directory entry expected: " + commas_quote(dirs.sorted)) + def get_entry( + dir: Path, + pred: Path => Boolean = _ => true, + title: String = "" + ): Path = + read_dir(dir).filter(name => pred(dir + Path.basic(name))) match { + case List(entry) => dir + Path.basic(entry) + case bad => + error("Bad directory content in " + (if (title.nonEmpty) title else dir.toString) + + "\nexpected a single entry, but found" + + (if (bad.isEmpty) " nothing" + else bad.sorted.map(quote).mkString(":\n ", "\n ", ""))) } + def get_file(dir: Path, title: String = ""): Path = + get_entry(dir, pred = _.is_file, title = title) + + def get_dir(dir: Path, title: String = ""): Path = + get_entry(dir, pred = _.is_dir, title = title) + def find_files( start: JFile, pred: JFile => Boolean = _ => true, include_dirs: Boolean = false, follow_links: Boolean = false ): List[JFile] = { val result = new mutable.ListBuffer[JFile] def check(file: JFile): Unit = if (pred(file)) result += file if (start.isFile) check(start) else if (start.isDirectory) { val options = if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS) else EnumSet.noneOf(classOf[FileVisitOption]) Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE, new SimpleFileVisitor[JPath] { override def preVisitDirectory( path: JPath, attrs: BasicFileAttributes ): FileVisitResult = { if (include_dirs) check(path.toFile) FileVisitResult.CONTINUE } override def visitFile( path: JPath, attrs: BasicFileAttributes ): FileVisitResult = { val file = path.toFile if (include_dirs || !file.isDirectory) check(file) FileVisitResult.CONTINUE } } ) } result.toList } /* read */ def read(file: JFile): String = Bytes.read(file).text def read(path: Path): String = read(path.file) def read_stream(reader: BufferedReader): String = { val output = new StringBuilder(100) var c = -1 while ({ c = reader.read; c != -1 }) output += c.toChar reader.close() output.toString } def read_stream(stream: InputStream): String = read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) def read_gzip(file: JFile): String = read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_gzip(path: Path): String = read_gzip(path.file) def read_xz(file: JFile): String = read_stream(new xz.XZInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_xz(path: Path): String = read_xz(path.file) def read_zstd(file: JFile): String = { Zstd.init() read_stream(new zstd.ZstdInputStream(new BufferedInputStream(new FileInputStream(file)))) } def read_zstd(path: Path): String = read_zstd(path.file) /* read lines */ def read_line(reader: BufferedReader): Option[String] = { val line = try { reader.readLine} catch { case _: IOException => null } Option(line).map(Library.trim_line) } def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = { val result = new mutable.ListBuffer[String] var line: Option[String] = None while ({ line = read_line(reader); line.isDefined }) { progress(line.get) result += line.get } reader.close() result.toList } /* write */ def writer(file: JFile): BufferedWriter = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset)) def write_file( file: JFile, text: String, make_stream: OutputStream => OutputStream ): Unit = { val stream = make_stream(new FileOutputStream(file)) using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text)) } def write(file: JFile, text: String): Unit = write_file(file, text, s => s) def write(path: Path, text: String): Unit = write(path.file, text) def write_gzip(file: JFile, text: String): Unit = write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) def write_gzip(path: Path, text: String): Unit = write_gzip(path.file, text) def write_xz(file: JFile, text: String, options: Compress.Options_XZ): Unit = File.write_file(file, text, s => new xz.XZOutputStream(new BufferedOutputStream(s), options.make)) def write_xz(file: JFile, text: String): Unit = write_xz(file, text, Compress.Options_XZ()) def write_xz(path: Path, text: String, options: Compress.Options_XZ): Unit = write_xz(path.file, text, options) def write_xz(path: Path, text: String): Unit = write_xz(path, text, Compress.Options_XZ()) def write_zstd(file: JFile, text: String, options: Compress.Options_Zstd): Unit = { Zstd.init() File.write_file(file, text, s => new zstd.ZstdOutputStream(new BufferedOutputStream(s), options.level)) } def write_zstd(file: JFile, text: String): Unit = write_zstd(file, text, Compress.Options_Zstd()) def write_zstd(path: Path, text: String, options: Compress.Options_Zstd): Unit = write_zstd(path.file, text, options) def write_zstd(path: Path, text: String): Unit = write_zstd(path, text, Compress.Options_Zstd()) def write_backup(path: Path, text: String): Unit = { if (path.is_file) Isabelle_System.move_file(path, path.backup) write(path, text) } def write_backup2(path: Path, text: String): Unit = { if (path.is_file) Isabelle_System.move_file(path, path.backup2) write(path, text) } /* append */ def append(file: JFile, text: String): Unit = Files.write(file.toPath, UTF8.bytes(text), StandardOpenOption.APPEND, StandardOpenOption.CREATE) def append(path: Path, text: String): Unit = append(path.file, text) /* change */ def change( path: Path, init: Boolean = false, strict: Boolean = false )(f: String => String): Unit = { if (!path.is_file && init) write(path, "") val x = read(path) val y = f(x) if (x != y) write(path, y) else if (strict) error("Unchanged file: " + path) } def change_lines(path: Path, init: Boolean = false, strict: Boolean = false)( f: List[String] => List[String]): Unit = change(path, init = init, strict = strict)(text => cat_lines(f(split_lines(text)))) /* eq */ def eq(file1: JFile, file2: JFile): Boolean = try { Files.isSameFile(file1.toPath, file2.toPath) } catch { case ERROR(_) => false } def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) /* eq_content */ def eq_content(file1: JFile, file2: JFile): Boolean = if (eq(file1, file2)) true else if (file1.length != file2.length) false else Bytes.read(file1) == Bytes.read(file2) def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) /* permissions */ def is_executable(path: Path): Boolean = { if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok else path.file.canExecute } def set_executable(path: Path, flag: Boolean): Unit = { if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path) else if (Platform.is_windows) Isabelle_System.chmod("a-x", path) else path.file.setExecutable(flag, false) } /* content */ def content(path: Path, content: Bytes): Content = new Content(path, content) def content(path: Path, content: String): Content = new Content(path, Bytes(content)) def content(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content) final class Content private[File](val path: Path, val content: Bytes) { override def toString: String = path.toString def write(dir: Path): Unit = { val full_path = dir + path Isabelle_System.make_directory(full_path.expand.dir) Bytes.write(full_path, content) } } final class Content_XML private[File](val path: Path, val content: XML.Body) { override def toString: String = path.toString def output(out: XML.Body => String): Content = new Content(path, Bytes(out(content))) } } diff --git a/src/Pure/General/sql.scala b/src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala +++ b/src/Pure/General/sql.scala @@ -1,487 +1,484 @@ /* Title: Pure/General/sql.scala Author: Makarius Support for SQL databases: SQLite and PostgreSQL. */ package isabelle import java.time.OffsetDateTime import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet} import scala.collection.mutable object SQL { /** SQL language **/ type Source = String /* concrete syntax */ def escape_char(c: Char): String = c match { case '\u0000' => "\\0" case '\'' => "\\'" case '\"' => "\\\"" case '\b' => "\\b" case '\n' => "\\n" case '\r' => "\\r" case '\t' => "\\t" case '\u001a' => "\\Z" case '\\' => "\\\\" case _ => c.toString } def string(s: String): Source = s.iterator.map(escape_char).mkString("'", "", "'") def ident(s: String): Source = Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\"")))) def enclose(s: Source): Source = "(" + s + ")" def enclosure(ss: Iterable[Source]): Source = ss.mkString("(", ", ", ")") def select(columns: List[Column] = Nil, distinct: Boolean = false): Source = "SELECT " + (if (distinct) "DISTINCT " else "") + (if (columns.isEmpty) "*" else commas(columns.map(_.ident))) + " FROM " val join_outer: Source = " LEFT OUTER JOIN " val join_inner: Source = " INNER JOIN " def join(outer: Boolean): Source = if (outer) join_outer else join_inner def member(x: Source, set: Iterable[String]): Source = set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")") /* types */ object Type extends Enumeration { val Boolean = Value("BOOLEAN") val Int = Value("INTEGER") val Long = Value("BIGINT") val Double = Value("DOUBLE PRECISION") val String = Value("TEXT") val Bytes = Value("BLOB") val Date = Value("TIMESTAMP WITH TIME ZONE") } def sql_type_default(T: Type.Value): Source = T.toString def sql_type_sqlite(T: Type.Value): Source = if (T == Type.Boolean) "INTEGER" else if (T == Type.Date) "TEXT" else sql_type_default(T) def sql_type_postgresql(T: Type.Value): Source = if (T == Type.Bytes) "BYTEA" else sql_type_default(T) /* columns */ object Column { def bool(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = Column(name, Type.Boolean, strict, primary_key) def int(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = Column(name, Type.Int, strict, primary_key) def long(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = Column(name, Type.Long, strict, primary_key) def double(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = Column(name, Type.Double, strict, primary_key) def string(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = Column(name, Type.String, strict, primary_key) def bytes(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = Column(name, Type.Bytes, strict, primary_key) def date(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = Column(name, Type.Date, strict, primary_key) } sealed case class Column( name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false, expr: SQL.Source = "" ) { def make_primary_key: Column = copy(primary_key = true) def apply(table: Table): Column = Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key) def ident: Source = if (expr == "") SQL.ident(name) else enclose(expr) + " AS " + SQL.ident(name) def decl(sql_type: Type.Value => Source): Source = ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "") def defined: String = ident + " IS NOT NULL" def undefined: String = ident + " IS NULL" def equal(s: String): Source = ident + " = " + string(s) def where_equal(s: String): Source = "WHERE " + equal(s) override def toString: Source = ident } /* tables */ sealed case class Table(name: String, columns: List[Column], body: Source = "") { Library.duplicates(columns.map(_.name)) match { case Nil => case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name)) } def ident: Source = SQL.ident(name) def query: Source = if (body == "") error("Missing SQL body for table " + quote(name)) else SQL.enclose(body) def query_named: Source = query + " AS " + SQL.ident(name) def create(strict: Boolean, sql_type: Type.Value => Source): Source = { val primary_key = columns.filter(_.primary_key).map(_.name) match { case Nil => Nil case keys => List("PRIMARY KEY " + enclosure(keys)) } "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") + ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key) } def create_index(index_name: String, index_columns: List[Column], strict: Boolean = false, unique: Boolean = false): Source = "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " + (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " + ident + " " + enclosure(index_columns.map(_.name)) def insert_cmd(cmd: Source, sql: Source = ""): Source = cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) + (if (sql == "") "" else " " + sql) def insert(sql: Source = ""): Source = insert_cmd("INSERT", sql) def delete(sql: Source = ""): Source = "DELETE FROM " + ident + (if (sql == "") "" else " " + sql) def select( select_columns: List[Column] = Nil, sql: Source = "", distinct: Boolean = false): Source = SQL.select(select_columns, distinct = distinct) + ident + (if (sql == "") "" else " " + sql) override def toString: Source = ident } /** SQL database operations **/ /* statements */ class Statement private[SQL](val db: Database, val rep: PreparedStatement) extends AutoCloseable { stmt => object bool { def update(i: Int, x: Boolean): Unit = rep.setBoolean(i, x) def update(i: Int, x: Option[Boolean]): Unit = { if (x.isDefined) update(i, x.get) else rep.setNull(i, java.sql.Types.BOOLEAN) } } object int { def update(i: Int, x: Int): Unit = rep.setInt(i, x) def update(i: Int, x: Option[Int]): Unit = { if (x.isDefined) update(i, x.get) else rep.setNull(i, java.sql.Types.INTEGER) } } object long { def update(i: Int, x: Long): Unit = rep.setLong(i, x) def update(i: Int, x: Option[Long]): Unit = { if (x.isDefined) update(i, x.get) else rep.setNull(i, java.sql.Types.BIGINT) } } object double { def update(i: Int, x: Double): Unit = rep.setDouble(i, x) def update(i: Int, x: Option[Double]): Unit = { if (x.isDefined) update(i, x.get) else rep.setNull(i, java.sql.Types.DOUBLE) } } object string { def update(i: Int, x: String): Unit = rep.setString(i, x) def update(i: Int, x: Option[String]): Unit = update(i, x.orNull) } object bytes { def update(i: Int, bytes: Bytes): Unit = { if (bytes == null) rep.setBytes(i, null) else rep.setBinaryStream(i, bytes.stream(), bytes.length) } def update(i: Int, bytes: Option[Bytes]): Unit = update(i, bytes.orNull) } object date { def update(i: Int, date: Date): Unit = db.update_date(stmt, i, date) def update(i: Int, date: Option[Date]): Unit = update(i, date.orNull) } def execute(): Boolean = rep.execute() def execute_query(): Result = new Result(this, rep.executeQuery()) def close(): Unit = rep.close() } /* results */ class Result private[SQL](val stmt: Statement, val rep: ResultSet) { res => def next(): Boolean = rep.next() def iterator[A](get: Result => A): Iterator[A] = new Iterator[A] { private var _next: Boolean = res.next() def hasNext: Boolean = _next def next(): A = { val x = get(res); _next = res.next(); x } } def bool(column: Column): Boolean = rep.getBoolean(column.name) def int(column: Column): Int = rep.getInt(column.name) def long(column: Column): Long = rep.getLong(column.name) def double(column: Column): Double = rep.getDouble(column.name) def string(column: Column): String = { val s = rep.getString(column.name) if (s == null) "" else s } def bytes(column: Column): Bytes = { val bs = rep.getBytes(column.name) if (bs == null) Bytes.empty else Bytes(bs) } def date(column: Column): Date = stmt.db.date(res, column) def timing(c1: Column, c2: Column, c3: Column): Timing = Timing(Time.ms(long(c1)), Time.ms(long(c2)), Time.ms(long(c3))) def get[A](column: Column, f: Column => A): Option[A] = { val x = f(column) if (rep.wasNull) None else Some(x) } def get_bool(column: Column): Option[Boolean] = get(column, bool) def get_int(column: Column): Option[Int] = get(column, int) def get_long(column: Column): Option[Long] = get(column, long) def get_double(column: Column): Option[Double] = get(column, double) def get_string(column: Column): Option[String] = get(column, string) def get_bytes(column: Column): Option[Bytes] = get(column, bytes) def get_date(column: Column): Option[Date] = get(column, date) } /* database */ trait Database extends AutoCloseable { db => def is_server: Boolean /* types */ def sql_type(T: Type.Value): Source /* connection */ def connection: Connection def close(): Unit = connection.close() def transaction[A](body: => A): A = { val auto_commit = connection.getAutoCommit() try { connection.setAutoCommit(false) val savepoint = connection.setSavepoint() try { val result = body connection.commit() result } catch { case exn: Throwable => connection.rollback(savepoint); throw exn } } finally { connection.setAutoCommit(auto_commit) } } /* statements and results */ def statement(sql: Source): Statement = new Statement(db, connection.prepareStatement(sql)) def using_statement[A](sql: Source)(f: Statement => A): A = using(statement(sql))(f) def update_date(stmt: Statement, i: Int, date: Date): Unit def date(res: Result, column: Column): Date def insert_permissive(table: Table, sql: Source = ""): Source /* tables and views */ def tables: List[String] = { val result = new mutable.ListBuffer[String] val rs = connection.getMetaData.getTables(null, null, "%", null) while (rs.next) { result += rs.getString(3) } result.toList } def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit = using_statement( table.create(strict, sql_type) + (if (sql == "") "" else " " + sql))(_.execute()) def create_index(table: Table, name: String, columns: List[Column], strict: Boolean = false, unique: Boolean = false): Unit = using_statement(table.create_index(name, columns, strict, unique))(_.execute()) def create_view(table: Table, strict: Boolean = false): Unit = { if (strict || !tables.contains(table.name)) { val sql = "CREATE VIEW " + table + " AS " + { table.query; table.body } using_statement(sql)(_.execute()) } } } } /** SQLite **/ object SQLite { // see https://www.sqlite.org/lang_datefunc.html val date_format: Date.Format = Date.Format("uuuu-MM-dd HH:mm:ss.SSS x") lazy val init_jdbc: Unit = { val lib_path = Path.explode("$ISABELLE_SQLITE_HOME/" + Platform.jvm_platform) - val lib_name = - File.find_files(lib_path.file) match { - case List(file) => file.getName - case _ => error("Exactly one file expected in directory " + lib_path.expand) - } + val lib_name = File.get_file(lib_path).file_name + System.setProperty("org.sqlite.lib.path", File.platform_path(lib_path)) System.setProperty("org.sqlite.lib.name", lib_name) Class.forName("org.sqlite.JDBC") } def open_database(path: Path): Database = { init_jdbc val path0 = path.expand val s0 = File.platform_path(path0) val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0 val connection = DriverManager.getConnection("jdbc:sqlite:" + s1) new Database(path0.toString, connection) } class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database { override def toString: String = name override def is_server: Boolean = false def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T) def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit = if (date == null) stmt.string(i) = (null: String) else stmt.string(i) = date_format(date) def date(res: SQL.Result, column: SQL.Column): Date = date_format.parse(res.string(column)) def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source = table.insert_cmd("INSERT OR IGNORE", sql = sql) def rebuild(): Unit = using_statement("VACUUM")(_.execute()) } } /** PostgreSQL **/ object PostgreSQL { type Source = SQL.Source val default_port = 5432 lazy val init_jdbc: Unit = Class.forName("org.postgresql.Driver") def open_database( user: String, password: String, database: String = "", host: String = "", port: Int = 0, ssh: Option[SSH.Session] = None, ssh_close: Boolean = false ): Database = { init_jdbc if (user == "") error("Undefined database user") val db_host = proper_string(host) getOrElse "localhost" val db_port = if (port > 0 && port != default_port) ":" + port else "" val db_name = "/" + (proper_string(database) getOrElse user) val (url, name, port_forwarding) = ssh match { case None => val spec = db_host + db_port + db_name val url = "jdbc:postgresql://" + spec val name = user + "@" + spec (url, name, None) case Some(ssh) => val fw = ssh.port_forwarding(remote_host = db_host, remote_port = if (port > 0) port else default_port, ssh_close = ssh_close) val url = "jdbc:postgresql://localhost:" + fw.port + db_name val name = user + "@" + fw + db_name + " via ssh " + ssh (url, name, Some(fw)) } try { val connection = DriverManager.getConnection(url, user, password) new Database(name, connection, port_forwarding) } catch { case exn: Throwable => port_forwarding.foreach(_.close()); throw exn } } class Database private[PostgreSQL]( name: String, val connection: Connection, port_forwarding: Option[SSH.Port_Forwarding] ) extends SQL.Database { override def toString: String = name override def is_server: Boolean = true def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T) // see https://jdbc.postgresql.org/documentation/head/8-date-time.html def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit = if (date == null) stmt.rep.setObject(i, null) else stmt.rep.setObject(i, OffsetDateTime.from(date.to(Date.timezone_utc).rep)) def date(res: SQL.Result, column: SQL.Column): Date = { val obj = res.rep.getObject(column.name, classOf[OffsetDateTime]) if (obj == null) null else Date.instant(obj.toInstant) } def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source = table.insert_cmd("INSERT", sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING") override def close(): Unit = { super.close(); port_forwarding.foreach(_.close()) } } } diff --git a/src/Pure/General/zstd.scala b/src/Pure/General/zstd.scala --- a/src/Pure/General/zstd.scala +++ b/src/Pure/General/zstd.scala @@ -1,32 +1,29 @@ /* Title: Pure/General/xz.scala Author: Makarius Support for Zstd data compression. */ package isabelle import com.github.luben.zstd object Zstd { def init(): Unit = init_jni private lazy val init_jni: Unit = { require(!zstd.util.Native.isLoaded(), "Zstd library already initialized by other means than isabelle.Zstd.init()") val lib_dir = Path.explode("$ISABELLE_ZSTD_HOME/" + Platform.jvm_platform) - val lib_file = - File.find_files(lib_dir.file) match { - case List(file) => file - case _ => error("Exactly one file expected in directory " + lib_dir.expand) - } - System.load(File.platform_path(lib_file.getAbsolutePath)) + val lib_file = File.get_file(lib_dir) + + System.load(lib_file.absolute_file.getPath) zstd.util.Native.assumeLoaded() assert(zstd.util.Native.isLoaded()) Class.forName("com.github.luben.zstd.Zstd") } } diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala +++ b/src/Pure/Tools/phabricator.scala @@ -1,1050 +1,1050 @@ /* Title: Pure/Tools/phabricator.scala Author: Makarius Support for Phabricator server, notably for Ubuntu 20.04 LTS. See also: - https://www.phacility.com/phabricator - https://secure.phabricator.com/book/phabricator */ package isabelle import scala.collection.mutable import scala.util.matching.Regex object Phabricator { /** defaults **/ /* required packages */ val packages_ubuntu_20_04: List[String] = Build_Docker.packages ::: List( // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages "php-xml", "php-zip", "python3-pygments", "ssh", "subversion", "python-pygments", // mercurial build packages "make", "gcc", "python", "python2-dev", "python-docutils", "python-openssl") def packages: List[String] = { val release = Linux.Release() if (release.is_ubuntu_20_04) packages_ubuntu_20_04 else error("Bad Linux version: expected Ubuntu 20.04 LTS") } /* global system resources */ val www_user = "www-data" val daemon_user = "phabricator" val sshd_config: Path = Path.explode("/etc/ssh/sshd_config") /* installation parameters */ val default_name = "vcs" def phabricator_name(name: String = "", ext: String = ""): String = "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext) def isabelle_phabricator_name(name: String = "", ext: String = ""): String = "isabelle-" + phabricator_name(name = name, ext = ext) def default_root(name: String): Path = Path.explode("/var/www") + Path.basic(phabricator_name(name = name)) def default_repo(name: String): Path = default_root(name) + Path.basic("repo") val default_mailers: Path = Path.explode("mailers.json") val default_system_port: Int = 22 val alternative_system_port = 222 val default_server_port = 2222 val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz" /** global configuration **/ val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf")) def global_config_script( init: String = "", body: String = "", exit: String = ""): String = { """#!/bin/bash """ + (if (init.nonEmpty) "\n" + init else "") + """ { while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } do NAME="$(echo "$REPLY" | cut -d: -f1)" ROOT="$(echo "$REPLY" | cut -d: -f2)" { """ + Library.indent_lines(6, body) + """ } < /dev/null done } < """ + File.bash_path(global_config) + "\n" + (if (exit.nonEmpty) "\n" + exit + "\n" else "") } sealed case class Config(name: String, root: Path) { def home: Path = root + Path.explode(phabricator_name()) def execute(command: String): Process_Result = Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check } def read_config(): List[Config] = { if (global_config.is_file) { for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty) yield { space_explode(':', entry) match { case List(name, root) => Config(name, Path.explode(root)) case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry)) } } } else Nil } def write_config(configs: List[Config]): Unit = { File.write(global_config, configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n")) } def get_config(name: String): Config = read_config().find(config => config.name == name) getOrElse error("Bad Isabelle/Phabricator installation " + quote(name)) /** administrative tools **/ /* Isabelle tool wrapper */ val isabelle_tool1 = Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", Scala_Project.here, { args => var list = false var name = default_name val getopts = Getopts(""" Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] Options are: -l list available Phabricator installations -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Invoke a command-line tool within the home directory of the named Phabricator installation. """, "l" -> (_ => list = true), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.isEmpty && !list) getopts.usage() val progress = new Console_Progress if (list) { for (config <- read_config()) { progress.echo("phabricator " + quote(config.name) + " root " + config.root) } } else { val config = get_config(name) val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true) if (!result.ok) error(result.print_return_code) } }) /** setup **/ def user_setup(name: String, description: String, ssh_setup: Boolean = false): Unit = { if (!Linux.user_exists(name)) { Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup) } else if (Linux.user_description(name) != description) { error("User " + quote(name) + " already exists --" + " for Phabricator it should have the description:\n " + quote(description)) } } def command_setup(name: String, init: String = "", body: String = "", exit: String = "" ): Path = { val command = Path.explode("/usr/local/bin") + Path.basic(name) File.write(command, global_config_script(init = init, body = body, exit = exit)) Isabelle_System.chmod("755", command) Isabelle_System.chown("root:root", command) command } def mercurial_setup(mercurial_source: String, progress: Progress = new Progress): Unit = { progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...") Isabelle_System.with_tmp_dir("mercurial") { tmp_dir => val archive = if (Url.is_wellformed(mercurial_source)) { val archive = tmp_dir + Path.basic("mercurial.tar.gz") Isabelle_System.download_file(mercurial_source, archive) archive } else Path.explode(mercurial_source) Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check - val build_dir = tmp_dir + Path.basic(File.get_dir(tmp_dir)) + val build_dir = File.get_dir(tmp_dir, title = mercurial_source) progress.bash("make all && make install", cwd = build_dir.file, echo = true).check } } def phabricator_setup( options: Options, name: String = default_name, root: String = "", repo: String = "", package_update: Boolean = false, mercurial_source: String = "", progress: Progress = new Progress ): Unit = { /* system environment */ Linux.check_system_root() progress.echo("System packages ...") if (package_update) { Linux.package_update(progress = progress) Linux.check_reboot_required() } Linux.package_install(packages, progress = progress) Linux.check_reboot_required() if (mercurial_source.nonEmpty) { for { name <- List("mercurial", "mercurial-common") if Linux.package_installed(name) } { error("Cannot install Mercurial from source:\n" + "package package " + quote(name) + " already installed") } mercurial_setup(mercurial_source, progress = progress) } /* users */ if (name.exists((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) || Set("", "ssh", "phd", "dump", daemon_user).contains(name)) { error("Bad installation name: " + quote(name)) } user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true) user_setup(name, "Phabricator SSH User") /* basic installation */ progress.echo("\nPhabricator installation ...") val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name) val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name) val configs = read_config() for (config <- configs if config.name == name) { error("Duplicate Phabricator installation " + quote(name) + " in " + config.root) } if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) { error("Failed to create root directory " + root_path) } Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path) Isabelle_System.chmod("755", root_path) progress.bash(cwd = root_path.file, echo = true, script = """ set -e echo "Cloning distribution repositories:" git clone --branch stable https://github.com/phacility/arcanist.git git -C arcanist reset --hard """ + Bash.string(options.string("phabricator_version_arcanist")) + """ git clone --branch stable https://github.com/phacility/phabricator.git git -C phabricator reset --hard """ + Bash.string(options.string("phabricator_version_phabricator")) + """ """).check val config = Config(name, root_path) write_config(configs ::: List(config)) config.execute("config set pygments.enabled true") /* local repository directory */ progress.echo("\nRepository hosting setup ...") if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) { error("Failed to create local repository directory " + repo_path) } Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path) Isabelle_System.chmod("755", repo_path) config.execute("config set repository.default-local-path " + File.bash_path(repo_path)) val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name(name = name)) File.write(sudoers_file, www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" + name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n") Isabelle_System.chmod("440", sudoers_file) config.execute("config set diffusion.ssh-user " + Bash.string(config.name)) /* MySQL setup */ progress.echo("\nMySQL setup ...") File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")), """[mysqld] max_allowed_packet = 32M innodb_buffer_pool_size = 1600M local_infile = 0 """) Linux.service_restart("mysql") def mysql_conf(R: Regex, which: String): String = { val conf = Path.explode("/etc/mysql/debian.cnf") split_lines(File.read(conf)).collectFirst({ case R(a) => a }) match { case Some(res) => res case None => error("Cannot determine " + which + " from " + conf) } } val mysql_root_user = mysql_conf("""^user\s*=\s*(\S*)\s*$""".r, "superuser name") val mysql_root_password = mysql_conf("""^password\s*=\s*(\S*)\s*$""".r, "superuser password") val mysql_name = phabricator_name(name = name).replace("-", "_") val mysql_user_string = SQL.string(mysql_name) + "@'localhost'" val mysql_password = Linux.generate_password() Isabelle_System.bash("mysql --user=" + Bash.string(mysql_root_user) + " --password=" + Bash.string(mysql_root_password) + " --execute=" + Bash.string( """DROP USER IF EXISTS """ + mysql_user_string + "; " + """CREATE USER """ + mysql_user_string + """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ + """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") + """`.* TO """ + mysql_user_string + ";" + """GRANT PROCESS ON *.* TO """ + mysql_user_string + ";")).check config.execute("config set mysql.user " + Bash.string(mysql_name)) config.execute("config set mysql.pass " + Bash.string(mysql_password)) config.execute("config set phabricator.cache-namespace " + Bash.string(mysql_name)) config.execute("config set storage.default-namespace " + Bash.string(mysql_name)) config.execute("config set storage.mysql-engine.max-size 8388608") progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check /* database dump */ val dump_name = isabelle_phabricator_name(name = "dump") command_setup(dump_name, body = """mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database" [ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz" echo -n "Creating $ROOT/database/dump.sql.gz ..." "$ROOT/phabricator/bin/storage" dump --compress --output "$ROOT/database/dump.sql.gz" 2>&1 | fgrep -v '[Warning] Using a password on the command line interface can be insecure' echo " $(ls -hs "$ROOT/database/dump.sql.gz" | cut -d" " -f1)" """) /* Phabricator upgrade */ command_setup(isabelle_phabricator_name(name = "upgrade"), init = """BRANCH="${1:-stable}" if [ "$BRANCH" != "master" -a "$BRANCH" != "stable" ] then echo "Bad branch: \"$BRANCH\"" exit 1 fi systemctl stop isabelle-phabricator-phd systemctl stop apache2 """, body = """echo -e "\nUpgrading phabricator \"$NAME\" root \"$ROOT\" ..." for REPO in arcanist phabricator do cd "$ROOT/$REPO" echo -e "\nUpdating \"$REPO\" ..." git checkout "$BRANCH" git pull done echo -e "\nUpgrading storage ..." "$ROOT/phabricator/bin/storage" upgrade --force """, exit = """systemctl start apache2 systemctl start isabelle-phabricator-phd""") /* PHP setup */ val php_version = Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""") .check.out val php_conf = Path.explode("/etc/php") + Path.basic(php_version) + // educated guess Path.explode("apache2/conf.d") + Path.basic(isabelle_phabricator_name(ext = "ini")) File.write(php_conf, "post_max_size = 32M\n" + "opcache.validate_timestamps = 0\n" + "memory_limit = 512M\n" + "max_execution_time = 120\n") /* Apache setup */ progress.echo("Apache setup ...") val apache_root = Path.explode("/etc/apache2") val apache_sites = apache_root + Path.explode("sites-available") if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites) val server_name = phabricator_name(name = name, ext = "lvh.me") // alias for "localhost" for testing val server_url = "http://" + server_name File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")), """ ServerName """ + server_name + """ ServerAdmin webmaster@localhost DocumentRoot """ + config.home.implode + """/webroot ErrorLog ${APACHE_LOG_DIR}/error.log CustomLog ${APACHE_LOG_DIR}/access.log combined RewriteEngine on RewriteRule ^(.*)$ /index.php?__path__=$1 [B,L,QSA] # vim: syntax=apache ts=4 sw=4 sts=4 sr noet """) Isabelle_System.bash( """ set -e a2enmod rewrite a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check config.execute("config set phabricator.base-uri " + Bash.string(server_url)) Linux.service_restart("apache2") progress.echo("\nFurther manual configuration via " + server_url) /* PHP daemon */ progress.echo("\nPHP daemon setup ...") val phd_log_path = Isabelle_System.make_directory(Path.explode("/var/tmp/phd")) Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path) Isabelle_System.chmod("755", phd_log_path) config.execute("config set phd.user " + Bash.string(daemon_user)) config.execute("config set phd.log-directory /var/tmp/phd/" + isabelle_phabricator_name(name = name) + "/log") val phd_name = isabelle_phabricator_name(name = "phd") Linux.service_shutdown(phd_name) val phd_command = command_setup(phd_name, body = """"$ROOT/phabricator/bin/phd" "$@" """) try { Linux.service_install(phd_name, """[Unit] Description=PHP daemon manager for Isabelle/Phabricator After=syslog.target network.target apache2.service mysql.service [Service] Type=oneshot User=""" + daemon_user + """ Group=""" + daemon_user + """ Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin ExecStart=""" + phd_command.implode + """ start --force ExecStop=""" + phd_command.implode + """ stop RemainAfterExit=yes [Install] WantedBy=multi-user.target """) } catch { case ERROR(msg) => progress.bash("bin/phd status", cwd = config.home.file, echo = true).check error(msg) } } /* Isabelle tool wrapper */ val isabelle_tool2 = Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", Scala_Project.here, { args => var mercurial_source = "" var repo = "" var package_update = false var name = default_name var options = Options.init() var root = "" val getopts = Getopts(""" Usage: isabelle phabricator_setup [OPTIONS] Options are: -M SOURCE install Mercurial from source: local PATH, or URL, or ":" for """ + standard_mercurial_source + """ -R DIR repository directory (default: """ + default_repo("NAME") + """) -U full update of system packages before installation -n NAME Phabricator installation name (default: """ + quote(default_name) + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -r DIR installation root directory (default: """ + default_root("NAME") + """) Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). The installation name (default: """ + quote(default_name) + """) is mapped to a regular Unix user; this is relevant for public SSH access. """, "M:" -> (arg => mercurial_source = (if (arg == ":") standard_mercurial_source else arg)), "R:" -> (arg => repo = arg), "U" -> (_ => package_update = true), "n:" -> (arg => name = arg), "o:" -> (arg => options = options + arg), "r:" -> (arg => root = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup(options, name = name, root = root, repo = repo, package_update = package_update, mercurial_source = mercurial_source, progress = progress) }) /** setup mail **/ val mailers_template: String = """[ { "key": "example.org", "type": "smtp", "options": { "host": "mail.example.org", "port": 465, "user": "phabricator@example.org", "password": "********", "protocol": "ssl", "message-id": true } } ]""" def phabricator_setup_mail( name: String = default_name, config_file: Option[Path] = None, test_user: String = "", progress: Progress = new Progress ): Unit = { Linux.check_system_root() val config = get_config(name) val default_config_file = config.root + default_mailers val mail_config = config_file getOrElse default_config_file def setup_mail: Unit = { progress.echo("Using mail configuration from " + mail_config) config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config)) if (test_user.nonEmpty) { progress.echo("Sending test mail to " + quote(test_user)) progress.bash(cwd = config.home.file, echo = true, script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ + Bash.string(test_user)).check } } if (config_file.isEmpty) { if (!default_config_file.is_file) { File.write(default_config_file, mailers_template) Isabelle_System.chmod("600", default_config_file) } if (File.read(default_config_file) == mailers_template) { progress.echo("Please invoke the tool again, after providing details in\n " + default_config_file.implode + "\n") } else setup_mail } else setup_mail } /* Isabelle tool wrapper */ val isabelle_tool3 = Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation", Scala_Project.here, { args => var test_user = "" var name = default_name var config_file: Option[Path] = None val getopts = Getopts(""" Usage: isabelle phabricator_setup_mail [OPTIONS] Options are: -T USER send test mail to Phabricator user -f FILE config file (default: """ + default_mailers + """ within Phabricator root) -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Provide mail configuration for existing Phabricator installation. """, "T:" -> (arg => test_user = arg), "f:" -> (arg => config_file = Some(Path.explode(arg))), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_mail(name = name, config_file = config_file, test_user = test_user, progress = progress) }) /** setup ssh **/ /* sshd config */ private val Port = """^\s*Port\s+(\d+)\s*$""".r private val No_Port = """^#\s*Port\b.*$""".r private val Any_Port = """^#?\s*Port\b.*$""".r def conf_ssh_port(port: Int): String = if (port == default_system_port) "#Port " + default_system_port else "Port " + port def read_ssh_port(conf: Path): Int = { val lines = split_lines(File.read(conf)) val ports = lines.flatMap({ case Port(Value.Int(p)) => Some(p) case No_Port() => Some(default_system_port) case _ => None }) ports match { case List(port) => port case Nil => error("Missing Port specification in " + conf) case _ => error("Multiple Port specifications in " + conf) } } def write_ssh_port(conf: Path, port: Int): Boolean = { val old_port = read_ssh_port(conf) if (old_port == port) false else { val lines = split_lines(File.read(conf)) val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line }) File.write(conf, cat_lines(lines1)) true } } /* phabricator_setup_ssh */ def phabricator_setup_ssh( server_port: Int = default_server_port, system_port: Int = default_system_port, progress: Progress = new Progress ): Unit = { Linux.check_system_root() val configs = read_config() if (server_port == system_port) { error("Port for Phabricator sshd coincides with system port: " + system_port) } val sshd_conf_system = Path.explode("/etc/ssh/sshd_config") val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name()) val ssh_name = isabelle_phabricator_name(name = "ssh") Linux.service_shutdown(ssh_name) val old_system_port = read_ssh_port(sshd_conf_system) if (old_system_port != system_port) { progress.echo("Reconfigurig system ssh service") Linux.service_shutdown("ssh") write_ssh_port(sshd_conf_system, system_port) Linux.service_start("ssh") } progress.echo("Configuring " + ssh_name + " service") val ssh_command = command_setup(ssh_name, body = """if [ "$1" = "$NAME" ] then exec "$ROOT/phabricator/bin/ssh-auth" "$@" fi""", exit = "exit 1") File.write(sshd_conf_server, """# OpenBSD Secure Shell server for Isabelle/Phabricator AuthorizedKeysCommand """ + ssh_command.implode + """ AuthorizedKeysCommandUser """ + daemon_user + """ AuthorizedKeysFile none AllowUsers """ + configs.map(_.name).mkString(" ") + """ Port """ + server_port + """ Protocol 2 PermitRootLogin no AllowAgentForwarding no AllowTcpForwarding no PrintMotd no PrintLastLog no PasswordAuthentication no ChallengeResponseAuthentication no PidFile /var/run/""" + ssh_name + """.pid """) Linux.service_install(ssh_name, """[Unit] Description=OpenBSD Secure Shell server for Isabelle/Phabricator After=network.target auditd.service ConditionPathExists=!/etc/ssh/sshd_not_to_be_run [Service] EnvironmentFile=-/etc/default/ssh ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecReload=/bin/kill -HUP $MAINPID KillMode=process Restart=on-failure RestartPreventExitStatus=255 Type=notify RuntimeDirectory=sshd-phabricator RuntimeDirectoryMode=0755 [Install] WantedBy=multi-user.target Alias=""" + ssh_name + """.service """) for (config <- configs) { progress.echo("phabricator " + quote(config.name) + " port " + server_port) config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString)) if (server_port == default_system_port) config.execute("config delete diffusion.ssh-port") } } /* Isabelle tool wrapper */ val isabelle_tool4 = Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations", Scala_Project.here, { args => var server_port = default_server_port var system_port = default_system_port val getopts = Getopts(""" Usage: isabelle phabricator_setup_ssh [OPTIONS] Options are: -p PORT sshd port for Phabricator servers (default: """ + default_server_port + """) -q PORT sshd port for the operating system (default: """ + default_system_port + """) Configure ssh service for all Phabricator installations: a separate sshd is run in addition to the one of the operating system, and ports need to be distinct. A particular Phabricator installation is addressed by using its name as the ssh user; the actual Phabricator user is determined via stored ssh keys. """, "p:" -> (arg => server_port = Value.Int.parse(arg)), "q:" -> (arg => system_port = Value.Int.parse(arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_ssh( server_port = server_port, system_port = system_port, progress = progress) }) /** conduit API **/ object API { /* user information */ sealed case class User( id: Long, phid: String, name: String, real_name: String, roles: List[String] ) { def is_valid: Boolean = roles.contains("verified") && roles.contains("approved") && roles.contains("activated") def is_admin: Boolean = roles.contains("admin") def is_regular: Boolean = !(roles.contains("bot") || roles.contains("list")) } /* repository information */ sealed case class Repository( vcs: VCS.Value, id: Long, phid: String, name: String, callsign: String, short_name: String, importing: Boolean, ssh_url: String ) { def is_hg: Boolean = vcs == VCS.hg } object VCS extends Enumeration { val hg, git, svn = Value def read(s: String): Value = try { withName(s) } catch { case _: java.util.NoSuchElementException => error("Unknown vcs type " + quote(s)) } } def edits(typ: String, value: JSON.T): List[JSON.Object.T] = List(JSON.Object("type" -> typ, "value" -> value)) def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] = value.toList.flatMap(edits(typ, _)) /* result with optional error */ sealed case class Result(result: JSON.T, error: Option[String]) { def ok: Boolean = error.isEmpty def get: JSON.T = if (ok) result else Exn.error(error.get) def get_value[A](unapply: JSON.T => Option[A]): A = unapply(get) getOrElse Exn.error("Bad JSON result: " + JSON.Format(result)) def get_string: String = get_value(JSON.Value.String.unapply) } def make_result(json: JSON.T): Result = { val result = JSON.value(json, "result").getOrElse(JSON.Object.empty) val error_info = JSON.string(json, "error_info") val error_code = JSON.string(json, "error_code") Result(result, error_info orElse error_code) } /* context for operations */ def apply(server: String, port: Int = 0): API = new API(server, port) } final class API private(server: String, port: Int) { /* connection */ private def port_suffix: String = if (port > 0) ":" + port else "" override def toString: String = server + port_suffix def hg_url: String = "ssh://" + server + port_suffix /* execute methods */ def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T = { Isabelle_System.with_tmp_file("params", "json") { params_file => File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params)))) val result = Isabelle_System.bash( SSH.client_command(port = port) + " -- " + Bash.string(server) + " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check JSON.parse(result.out, strict = false) } } def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result = API.make_result(execute_raw(method, params = params)) def execute_search[A]( method: String, params: JSON.Object.T, unapply: JSON.T => Option[A] ): List[A] = { val results = new mutable.ListBuffer[A] var after = "" var cont = true while (cont) { val result = execute(method, params = params ++ JSON.optional("after" -> proper_string(after))) results ++= result.get_value(JSON.list(_, "data", unapply)) after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after"))) cont = after.nonEmpty } results.toList } def ping(): String = execute("conduit.ping").get_string /* users */ lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid")) lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName")) def get_users( all: Boolean = false, phid: String = "", name: String = "" ): List[API.User] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "usernames" -> name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("user.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "username") real_name <- JSON.string0(fields, "realName") roles <- JSON.strings(fields, "roles") } yield API.User(id, phid, name, real_name, roles))) } def the_user(phid: String): API.User = get_users(phid = phid) match { case List(user) => user case _ => error("Bad user PHID " + quote(phid)) } /* repositories */ def get_repositories( all: Boolean = false, phid: String = "", callsign: String = "", short_name: String = "" ): List[API.Repository] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "callsigns" -> callsign, "shortNames" -> short_name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("diffusion.repository.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { vcs_name <- JSON.string(fields, "vcs") id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "name") callsign <- JSON.string0(fields, "callsign") short_name <- JSON.string0(fields, "shortName") importing <- JSON.bool(fields, "isImporting") } yield { val vcs = API.VCS.read(vcs_name) val url_path = if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name val ssh_url = vcs match { case API.VCS.hg => hg_url + url_path case API.VCS.git => hg_url + url_path + ".git" case API.VCS.svn => "" } API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url) })) } def the_repository(phid: String): API.Repository = get_repositories(phid = phid) match { case List(repo) => repo case _ => error("Bad repository PHID " + quote(phid)) } def create_repository( name: String, callsign: String = "", // unique name, UPPERCASE short_name: String = "", // unique name description: String = "", public: Boolean = false, vcs: API.VCS.Value = API.VCS.hg ): API.Repository = { require(name.nonEmpty, "bad repository name") val transactions = API.edits("vcs", vcs.toString) ::: API.edits("name", name) ::: API.opt_edits("callsign", proper_string(callsign)) ::: API.opt_edits("shortName", proper_string(short_name)) ::: API.opt_edits("description", proper_string(description)) ::: (if (public) Nil else API.edits("view", user_phid) ::: API.edits("policy.push", user_phid)) ::: API.edits("status", "active") val phid = execute("diffusion.repository.edit", params = JSON.Object("transactions" -> transactions)) .get_value(JSON.value(_, "object", JSON.string(_, "phid"))) execute("diffusion.looksoon", params = JSON.Object("repositories" -> List(phid))).get the_repository(phid) } } }