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,200 +1,199 @@
/* 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_dir = File.get_dir(tmp_dir, title = archive_name)
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
progress.echo("Building CSDP for " + platform_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(source_dir.file, pred = file => file.getName == "Makefile").
foreach(file => flags.change(File.path(file)))
}
progress.bash(mingw.bash_script("make"), cwd = source_dir.file, echo = verbose).check
/* install */
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_e.scala b/src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala
+++ b/src/Pure/Admin/build_e.scala
@@ -1,141 +1,141 @@
/* Title: Pure/Admin/build_e.scala
Author: Makarius
Build Isabelle E prover component from official downloads.
*/
package isabelle
object Build_E {
/* build E prover */
val default_version = "2.6"
val default_download_url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD"
def build_e(
version: String = default_version,
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val component_name = "e-" + version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
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_url = download_url + "/V_" + version + "/E.tgz"
val archive_path = tmp_dir + Path.explode("E.tgz")
Isabelle_System.download_file(archive_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
- Isabelle_System.bash("tar xzf " + archive_path + " && mv E src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = archive_url)
+
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
progress.echo("Building E prover for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic("E")
val build_options = {
- val result = Isabelle_System.bash("./configure --help", cwd = build_dir.file)
+ val result = Isabelle_System.bash("./configure --help", cwd = source_dir.file)
if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else ""
}
val build_script = "./configure" + build_options + " && make"
- Isabelle_System.bash(build_script,
- cwd = build_dir.file,
+ Isabelle_System.bash(build_script, cwd = source_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.basic("COPYING"), component_dir.LICENSE)
+ Isabelle_System.copy_file(source_dir + Path.basic("COPYING"), component_dir.LICENSE)
val install_files = List("epclextract", "eprover", "eprover-ho")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
- val path = build_dir + Path.basic("PROVER") + Path.basic(name)
+ val path = source_dir + Path.basic("PROVER") + Path.basic(name)
if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
}
Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi",
cwd = platform_dir.file).check
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
E_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
E_VERSION=""" + quote(version) + """
""")
/* README */
File.write(component_dir.README,
"This is E prover " + version + " from\n" + archive_url + """
The distribution has been built like this:
cd src && """ + build_script + """
Only a few executables from PROVERS/ have been moved to the platform-specific
Isabelle component directory: x86_64-linux etc.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_e", "build prover component from source distribution", Scala_Project.here,
{ args =>
var target_dir = Path.current
var version = default_version
var download_url = default_download_url
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_e [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL
(default: """" + default_download_url + """")
-V VERSION version (default: """ + default_version + """)
-v verbose
Build prover component from the specified source distribution.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg),
"V:" -> (arg => version = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_e(version = version, download_url = download_url,
verbose = verbose, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_jedit.scala b/src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala
+++ b/src/Pure/Admin/build_jedit.scala
@@ -1,543 +1,543 @@
/* Title: Pure/Admin/build_jedit.scala
Author: Makarius
Build component for jEdit text-editor.
*/
package isabelle
import java.nio.charset.Charset
import scala.jdk.CollectionConverters._
object Build_JEdit {
/* modes */
object Mode {
val empty: Mode = new Mode("", "", Nil)
val init: Mode =
empty +
("noWordSep" -> """_'?⇩\^<>""") +
("unalignedOpenBrackets" -> "{[(«‹⟨⌈⌊⦇⟦⦃⦉") +
("unalignedCloseBrackets" -> "⦊⦄⟧⦈⌋⌉⟩›»)]}") +
("tabSize" -> "2") +
("indentSize" -> "2")
val list: List[Mode] = {
val isabelle_news: Mode = init.define("isabelle-news", "Isabelle NEWS")
val isabelle: Mode =
init.define("isabelle", "Isabelle theory") +
("commentStart" -> "(*") +
("commentEnd" -> "*)")
val isabelle_ml: Mode = isabelle.define("isabelle-ml", "Isabelle/ML")
val isabelle_root: Mode = isabelle.define("isabelle-root", "Isabelle session root")
val isabelle_options: Mode = isabelle.define("isabelle-options", "Isabelle options")
val sml: Mode =
init.define("sml", "Standard ML") +
("commentStart" -> "(*") +
("commentEnd" -> "*)") +
("noWordSep" -> "_'")
List(isabelle_news, isabelle, isabelle_ml, isabelle_root, isabelle_options, sml)
}
}
final case class Mode private(name: String, description: String, rev_props: Properties.T) {
override def toString: String = name
def define(a: String, b: String): Mode = new Mode(a, b, rev_props)
def + (entry: Properties.Entry): Mode =
new Mode(name, description, Properties.put(rev_props, entry))
def write(dir: Path): Unit = {
require(name.nonEmpty && description.nonEmpty, "Bad Isabelle/jEdit mode content")
val properties =
rev_props.reverse.map(p =>
Symbol.spaces(4) +
XML.string_of_tree(XML.elem(Markup("PROPERTY", List("NAME" -> p._1, "VALUE" -> p._2)))))
File.write(dir + Path.basic(name).xml,
"""
""" + properties.mkString("\n", "\n", "") + """
""")
}
}
/* build jEdit component */
private val download_jars: List[(String, String)] =
List(
"https://repo1.maven.org/maven2/com/google/code/findbugs/jsr305/3.0.2/jsr305-3.0.2.jar" ->
"jsr305-3.0.2.jar")
private val download_plugins: List[(String, String)] =
List(
"Code2HTML" -> "0.7",
"CommonControls" -> "1.7.4",
"Console" -> "5.1.4",
"ErrorList" -> "2.4.0",
"Highlight" -> "2.5",
"Navigator" -> "2.7",
"SideKick" -> "1.8")
private def exclude_package(name: String): Boolean =
name.startsWith("de.masters_of_disaster.ant") ||
name == "doclet" ||
name == "installer"
def build_jedit(
component_path: Path,
version: String,
original: Boolean = false,
java_home: Path = default_java_home,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("ant", test = "-version")
Isabelle_System.require_command("patch")
val component_dir = Components.Directory.create(component_path, progress = progress)
/* jEdit directory */
val jedit = "jedit" + version
val jedit_patched = jedit + "-patched"
val jedit_dir = Isabelle_System.make_directory(component_path + Path.basic(jedit))
val jedit_patched_dir = component_path + Path.basic(jedit_patched)
def download_jedit(dir: Path, name: String, target_name: String = ""): Path = {
val jedit_name = jedit + name
val url =
"https://sourceforge.net/projects/jedit/files/jedit/" +
version + "/" + jedit_name + "/download"
val path = dir + Path.basic(proper_string(target_name) getOrElse jedit_name)
Isabelle_System.download_file(url, path, progress = progress)
path
}
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* original version */
val install_path = download_jedit(tmp_dir, "install.jar")
Isabelle_System.bash("""export CLASSPATH=""
isabelle_java java -Duser.home=""" + File.bash_platform_path(tmp_dir) +
" -jar " + File.bash_platform_path(install_path) + " auto " +
File.bash_platform_path(jedit_dir) + " unix-script=off unix-man=off").check
val source_path = download_jedit(tmp_dir, "source.tar.bz2")
- Isabelle_System.gnutar("-xjf " + File.bash_path(source_path), dir = jedit_dir).check
+ Isabelle_System.extract(source_path, jedit_dir)
/* patched version */
Isabelle_System.copy_dir(jedit_dir, jedit_patched_dir)
val source_dir = jedit_patched_dir + Path.basic("jEdit")
val org_source_dir = source_dir + Path.basic("org")
val tmp_source_dir = tmp_dir + Path.basic("jEdit")
progress.echo("Patching jEdit sources ...")
for {
file <- File.find_files(Path.explode("~~/src/Tools/jEdit/patches").file).sortBy(_.getName)
name = file.getName
if !File.is_backup(name)
} {
progress.bash("patch -p2 < " + File.bash_path(File.path(file)),
cwd = source_dir.file, echo = true).check
}
for { theme <- List("classic", "tango") } {
val path = Path.explode("org/gjt/sp/jedit/icons/themes/" + theme + "/32x32/apps/isabelle.gif")
Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle_transparent-32.gif"),
source_dir + path)
}
progress.echo("Building jEdit ...")
Isabelle_System.copy_dir(source_dir, tmp_source_dir)
progress.bash("env JAVA_HOME=" + File.bash_platform_path(java_home) + " ant",
cwd = tmp_source_dir.file, echo = true).check
Isabelle_System.copy_file(tmp_source_dir + Path.explode("build/jedit.jar"), jedit_patched_dir)
val java_sources =
(for {
file <- File.find_files(org_source_dir.file, file => File.is_java(file.getName))
package_name <- Scala_Project.package_name(File.path(file))
if !exclude_package(package_name)
} yield File.path(component_path.java_path.relativize(file.toPath).toFile).implode).sorted
File.write(component_dir.build_props,
"module = " + jedit_patched + "/jedit.jar\n" +
"no_build = true\n" +
"requirements = env:JEDIT_JARS\n" +
("sources =" :: java_sources.sorted.map(" " + _)).mkString("", " \\\n", "\n"))
}
/* jars */
val jars_dir = Isabelle_System.make_directory(jedit_patched_dir + Path.basic("jars"))
for { (url, name) <- download_jars } {
Isabelle_System.download_file(url, jars_dir + Path.basic(name), progress = progress)
}
for { (name, vers) <- download_plugins } {
Isabelle_System.with_tmp_file("tmp", ext = "zip") { zip_path =>
val url =
"https://sourceforge.net/projects/jedit-plugins/files/" + name + "/" + vers + "/" +
name + "-" + vers + "-bin.zip/download"
Isabelle_System.download_file(url, zip_path, progress = progress)
Isabelle_System.extract(zip_path, jars_dir)
}
}
/* resources */
val keep_encodings = List("ISO-8859-1", "ISO-8859-15", "US-ASCII", "UTF-8", "windows-1252")
val drop_encodings =
Charset.availableCharsets().keySet().asScala.toList.sorted.filterNot(keep_encodings.contains)
File.write(jedit_patched_dir + Path.explode("properties/jEdit.props"),
"""#jEdit properties
autoReloadDialog=false
buffer.deepIndent=false
buffer.encoding=UTF-8-Isabelle
buffer.indentSize=2
buffer.lineSeparator=\n
buffer.maxLineLen=100
buffer.noTabs=true
buffer.sidekick.keystroke-parse=false
buffer.tabSize=2
buffer.undoCount=1000
close-docking-area.shortcut2=C+e C+CIRCUMFLEX
complete-word.shortcut=
console.dock-position=floating
console.encoding=UTF-8
console.font=Isabelle DejaVu Sans Mono
console.fontsize=14
delete-line.shortcut=A+d
delete.shortcut2=C+d
""" + drop_encodings.map(a => "encoding.opt-out." + a + "=true").mkString("\n") + """
encodingDetectors=BOM XML-PI buffer-local-property
end.shortcut=
expand-abbrev.shortcut2=CA+SPACE
expand-folds.shortcut=
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
foldPainter=Circle
gatchan.highlight.overview=false
helpviewer.font=Isabelle DejaVu Serif
helpviewer.fontsize=12
home.shortcut=
hypersearch-results.dock-position=right
insert-newline-indent.shortcut=
insert-newline.shortcut=
isabelle-debugger.dock-position=floating
isabelle-documentation.dock-position=left
isabelle-export-browser.label=Browse theory exports
isabelle-output.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
isabelle-query.dock-position=bottom
isabelle-session-browser.label=Browse session information
isabelle-simplifier-trace.dock-position=floating
isabelle-sledgehammer.dock-position=bottom
isabelle-state.dock-position=right
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
isabelle.complete-word.label=Complete word
isabelle.complete.label=Complete Isabelle text
isabelle.complete.shortcut2=C+b
isabelle.control-bold.label=Control bold
isabelle.control-bold.shortcut=C+e RIGHT
isabelle.control-emph.label=Control emphasized
isabelle.control-emph.shortcut=C+e LEFT
isabelle.control-reset.label=Control reset
isabelle.control-reset.shortcut=C+e BACK_SPACE
isabelle.control-sub.label=Control subscript
isabelle.control-sub.shortcut=C+e DOWN
isabelle.control-sup.label=Control superscript
isabelle.control-sup.shortcut=C+e UP
isabelle.decrease-font-size.label=Decrease font size
isabelle.decrease-font-size.shortcut2=C+SUBTRACT
isabelle.decrease-font-size.shortcut=C+MINUS
isabelle.decrease-font-size2.label=Decrease font size (clone)
isabelle.draft.label=Show draft in browser
isabelle.exclude-word-permanently.label=Exclude word permanently
isabelle.exclude-word.label=Exclude word
isabelle.first-error.label=Go to first error
isabelle.first-error.shortcut=CS+a
isabelle.goto-entity.label=Go to definition of formal entity at caret
isabelle.goto-entity.shortcut=CS+d
isabelle.include-word-permanently.label=Include word permanently
isabelle.include-word.label=Include word
isabelle.increase-font-size.label=Increase font size
isabelle.increase-font-size.shortcut2=C+ADD
isabelle.increase-font-size.shortcut=C+PLUS
isabelle.increase-font-size2.label=Increase font size (clone)
isabelle.increase-font-size2.shortcut=C+EQUALS
isabelle.java-monitor.label=Java/VM monitor
isabelle.last-error.label=Go to last error
isabelle.last-error.shortcut=CS+z
isabelle.message.label=Show message
isabelle.message.shortcut=CS+m
isabelle.newline.label=Newline with indentation of Isabelle keywords
isabelle.newline.shortcut=ENTER
isabelle.next-error.label=Go to next error
isabelle.next-error.shortcut=CS+n
isabelle.options.label=Isabelle options
isabelle.prev-error.label=Go to previous error
isabelle.prev-error.shortcut=CS+p
isabelle.preview.label=Show preview in browser
isabelle.reset-continuous-checking.label=Reset continuous checking
isabelle.reset-font-size.label=Reset font size
isabelle.reset-node-required.label=Reset node required
isabelle.reset-words.label=Reset non-permanent words
isabelle.select-entity.label=Select all occurences of formal entity at caret
isabelle.select-entity.shortcut=CS+ENTER
isabelle.set-continuous-checking.label=Set continuous checking
isabelle.set-node-required.label=Set node required
isabelle.toggle-breakpoint.label=Toggle Breakpoint
isabelle.toggle-continuous-checking.label=Toggle continuous checking
isabelle.toggle-continuous-checking.shortcut=C+e ENTER
isabelle.toggle-node-required.label=Toggle node required
isabelle.toggle-node-required.shortcut=C+e SPACE
isabelle.tooltip.label=Show tooltip
isabelle.tooltip.shortcut=CS+b
isabelle.update-state.label=Update state output
isabelle.update-state.shortcut=S+ENTER
lang.usedefaultlocale=false
largefilemode=full
line-end.shortcut=END
line-home.shortcut=HOME
logo.icon.medium=32x32/apps/isabelle.gif
lookAndFeel=com.formdev.flatlaf.FlatLightLaf
match-bracket.shortcut2=C+9
metal.primary.font=Isabelle DejaVu Sans
metal.primary.fontsize=12
metal.secondary.font=Isabelle DejaVu Sans
metal.secondary.fontsize=12
navigator.showOnToolbar=true
new-file-in-mode.shortcut=
next-bracket.shortcut2=C+e C+9
options.shortcuts.deletekeymap.label=Delete
options.shortcuts.duplicatekeymap.dialog.title=Keymap name
options.shortcuts.duplicatekeymap.label=Duplicate
options.shortcuts.resetkeymap.dialog.title=Reset keymap
options.shortcuts.resetkeymap.label=Reset
options.textarea.lineSpacing=1
plugin-blacklist.MacOSX.jar=true
plugin.MacOSXPlugin.altDispatcher=false
plugin.MacOSXPlugin.disableOption=true
prev-bracket.shortcut2=C+e C+8
print.font=Isabelle DejaVu Sans Mono
print.glyphVector=true
recent-buffer.shortcut2=C+CIRCUMFLEX
restore.remote=false
restore=false
search.subdirs.toggle=true
select-block.shortcut2=C+8
sidekick-tree.dock-position=right
sidekick.auto-complete-popup-get-focus=true
sidekick.buffer-save-parse=true
sidekick.complete-delay=0
sidekick.complete-instant.toggle=false
sidekick.complete-popup.accept-characters=\\t
sidekick.complete-popup.insert-characters=
sidekick.persistentFilter=true
sidekick.showFilter=true
sidekick.splitter.location=721
systrayicon=false
tip.show=false
toggle-full-screen.shortcut2=S+F11
toggle-multi-select.shortcut2=C+NUMBER_SIGN
toggle-rect-select.shortcut2=A+NUMBER_SIGN
twoStageSave=false
vfs.browser.dock-position=left
vfs.favorite.0.type=1
vfs.favorite.0=$ISABELLE_HOME
vfs.favorite.1.type=1
vfs.favorite.1=$ISABELLE_HOME_USER
vfs.favorite.2.type=1
vfs.favorite.2=$JEDIT_HOME
vfs.favorite.3.type=1
vfs.favorite.3=$JEDIT_SETTINGS
vfs.favorite.4.type=1
vfs.favorite.4=isabelle-export:
vfs.favorite.5.type=1
vfs.favorite.5=isabelle-session:
view.antiAlias=subpixel HRGB
view.blockCaret=true
view.caretBlink=false
view.docking.framework=PIDE
view.eolMarkers=false
view.extendedState=0
view.font=Isabelle DejaVu Sans Mono
view.fontsize=18
view.fracFontMetrics=false
view.gutter.font=Isabelle DejaVu Sans Mono
view.gutter.fontsize=12
view.gutter.lineNumbers=false
view.gutter.selectionAreaWidth=18
view.height=850
view.middleMousePaste=true
view.showToolbar=true
view.status.memory.background=#666699
view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
view.thickCaret=true
view.width=1200
xml-insert-closing-tag.shortcut=
""")
val modes_dir = jedit_patched_dir + Path.basic("modes")
Mode.list.foreach(_.write(modes_dir))
File.change_lines(modes_dir + Path.basic("catalog")) { _.flatMap(line =>
if (line.containsSlice("FILE=\"ml.xml\"") ||
line.containsSlice("FILE_NAME_GLOB=\"*.{sml,ml}\"") ||
line.containsSlice("FILE_NAME_GLOB=\"*.ftl\"")) Nil
else if (line.containsSlice("NAME=\"jamon\"")) {
List(
"""""",
"",
"""""",
"",
"""""",
"",
"""""",
"",
"""""",
"",
line)
}
else if (line.containsSlice("NAME=\"sqr\"")) {
List(
"""""",
"",
line)
}
else List(line))
}
/* doc */
val doc_dir = jedit_patched_dir + Path.basic("doc")
download_jedit(doc_dir, "manual-a4.pdf", target_name = "jedit-manual.pdf")
Isabelle_System.copy_file(
doc_dir + Path.basic("CHANGES.txt"), doc_dir + Path.basic("jedit-changes"))
File.write(doc_dir + Path.basic("Contents"),
"""Original jEdit Documentation
jedit-manual jEdit User's Guide
jedit-changes jEdit Version History
""")
/* make patch */
File.write(component_path + Path.basic(jedit).patch,
Isabelle_System.make_patch(component_path, Path.basic(jedit), Path.basic(jedit_patched)))
if (!original) Isabelle_System.rm_tree(jedit_dir)
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
JEDIT_HOME="$COMPONENT/""" + jedit_patched + """"
JEDIT_JARS=""" + quote(File.read_dir(jars_dir).map("$JEDIT_HOME/jars/" + _).mkString(":")) + """
JEDIT_JAR="$JEDIT_HOME/jedit.jar"
classpath "$JEDIT_JAR"
JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9"
JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4g -Xss16m"
JEDIT_JAVA_SYSTEM_OPTIONS="-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/doc"
""")
/* README */
File.write(component_dir.README,
"""This is a slightly patched version of jEdit """ + version + """ from
https://sourceforge.net/projects/jedit/files/jedit with some
additional plugins jars from
https://sourceforge.net/projects/jedit-plugins/files
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/** Isabelle tool wrappers **/
val default_version = "5.6.0"
def default_java_home: Path = Path.explode("$JAVA_HOME").expand
val isabelle_tool =
Isabelle_Tool("build_jedit", "build Isabelle component from the jEdit text-editor",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var java_home = default_java_home
var original = false
var version = default_version
val getopts = Getopts("""
Usage: isabelle build_jedit [OPTIONS]
Options are:
-D DIR target directory (default ".")
-J JAVA_HOME Java version for building jedit.jar (e.g. version 11)
-O retain copy of original jEdit directory
-V VERSION jEdit version (default: """ + quote(default_version) + """)
Build auxiliary jEdit component from original sources, with some patches.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"J:" -> (arg => java_home = Path.explode(arg)),
"O" -> (_ => original = true),
"V:" -> (arg => version = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val component_dir = target_dir + Path.basic("jedit-" + Date.Format.alt_date(Date.now()))
val progress = new Console_Progress()
build_jedit(component_dir, version, original = original,
java_home = java_home, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_lipics.scala b/src/Pure/Admin/build_lipics.scala
--- a/src/Pure/Admin/build_lipics.scala
+++ b/src/Pure/Admin/build_lipics.scala
@@ -1,113 +1,112 @@
/* Title: Pure/Admin/build_lipics.scala
Author: Makarius
Build Isabelle component for Dagstuhl LIPIcs style.
See also:
- https://github.com/dagstuhl-publishing/styles
- https://submission.dagstuhl.de/documentation/authors
- https://www.dagstuhl.de/en/publications/lipics
*/
package isabelle
object Build_LIPIcs {
/* files for document preparation */
val document_files: List[Path] =
for (name <- List("cc-by.pdf", "lipics-logo-bw.pdf", "lipics-v2021.cls"))
yield Path.explode("$ISABELLE_LIPICS_HOME/" + name)
/* build lipics component */
val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.2.tar.gz"
def build_lipics(
download_url: String = default_url,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
Isabelle_System.with_tmp_file("download", ext = "tar.gz") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.gnutar("-xzf " + File.bash_path(download_file),
- dir = download_dir, strip = 1).check
+ Isabelle_System.extract(download_file, download_dir, strip = true)
val lipics_dir = download_dir + Path.explode("LIPIcs/authors")
/* component */
val version = {
val Version = """^*.* v(.*)$""".r
val changelog = Path.explode("CHANGELOG.md")
split_lines(File.read(lipics_dir + changelog))
.collectFirst({ case Version(v) => v })
.getOrElse(error("Failed to detect version in " + changelog))
}
val component = "lipics-" + version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component), progress = progress)
Isabelle_System.copy_dir(lipics_dir, component_dir.path)
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_LIPICS_HOME="$COMPONENT/authors"
""")
/* README */
File.write(component_dir.README,
"""This is the Dagstuhl LIPIcs style for authors from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_lipics", "build component for Dagstuhl LIPIcs style",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_url
val getopts = Getopts("""
Usage: isabelle build_lipics [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
Build component for Dagstuhl LIPIcs 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_lipics(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,154 +1,153 @@
/* 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
+ Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
progress.echo("Building Minisat for " + platform_name + " ...")
Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
if (Platform.is_macos) {
File.change(source_dir + Path.explode("Makefile")) {
_.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "")
}
}
progress.bash("make r", source_dir.file, echo = verbose).check
Isabelle_System.copy_file(
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_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,948 +1,948 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release {
/** release context **/
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
- private def execute_tar(dir: Path, args: String, strip: Int = 0): Process_Result =
+ private def execute_tar(dir: Path, args: String, strip: Boolean = false): Process_Result =
Isabelle_System.gnutar(args, dir = dir, strip = strip).check
private def bash_java_opens(args: String*): String =
Bash.strings(args.toList.flatMap(arg => List("--add-opens", arg + "=ALL-UNNAMED")))
object Release_Context {
def apply(
target_dir: Path,
release_name: String = "",
components_base: Path = Components.default_components_base,
progress: Progress = new Progress
): Release_Context = {
val date = Date.now()
val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
new Release_Context(release_name, dist_name, dist_dir, components_base, progress)
}
}
class Release_Context private[Build_Release](
val release_name: String,
val dist_name: String,
val dist_dir: Path,
val components_base: Path,
val progress: Progress
) {
override def toString: String = dist_name
val isabelle: Path = Path.explode(dist_name)
val isabelle_dir: Path = dist_dir + isabelle
val isabelle_archive: Path = dist_dir + isabelle.tar.gz
val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
def other_isabelle(dir: Path): Other_Isabelle =
Other_Isabelle(dir + isabelle,
isabelle_identifier = dist_name + "-build",
progress = progress)
def make_announce(id: String): Unit = {
if (release_name.isEmpty) {
File.write(isabelle_dir + Path.explode("ANNOUNCE"),
"""
IMPORTANT NOTE
==============
This is a snapshot of Isabelle/""" + id + """ from the repository.
""")
}
}
def make_contrib(): Unit = {
Isabelle_System.make_directory(Components.contrib(isabelle_dir))
File.write(Components.contrib(isabelle_dir, name = "README"),
"""This directory contains add-on components that contribute to the main
Isabelle distribution. Separate licensing conditions apply, see each
directory individually.
""")
}
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
case Platform.Family.linux_arm =>
Bundle_Info(platform, "Linux (ARM)", dist_name + "_linux_arm.tar.gz")
case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
}
}
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
name: String
) {
def path: Path = Path.explode(name)
}
/** release archive **/
val ISABELLE: Path = Path.basic("Isabelle")
val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID")
val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS")
val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER")
object Release_Archive {
def make(bytes: Bytes, rename: String = ""): Release_Archive = {
Isabelle_System.with_tmp_dir("build_release")(dir =>
Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path =>
val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
Bytes.write(archive_path, bytes)
- execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
+ execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = true)
val id = File.read(isabelle_dir + ISABELLE_ID)
val tags = File.read(isabelle_dir + ISABELLE_TAGS)
val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER)
val (bytes1, identifier1) =
if (rename.isEmpty || rename == identifier) (bytes, identifier)
else {
File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename)
Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename))
execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename))
(Bytes.read(archive_path), rename)
}
new Release_Archive(bytes1, id, tags, identifier1)
}
)
}
def read(path: Path, rename: String = ""): Release_Archive =
make(Bytes.read(path), rename = rename)
def get(
url: String,
rename: String = "",
progress: Progress = new Progress
): Release_Archive = {
val bytes =
if (Path.is_wellformed(url)) Bytes.read(Path.explode(url))
else Isabelle_System.download(url, progress = progress).bytes
make(bytes, rename = rename)
}
}
case class Release_Archive private[Build_Release](
bytes: Bytes, id: String, tags: String, identifier: String) {
override def toString: String = identifier
}
/** generated content **/
/* bundled components */
class Bundled(platform: Option[Platform.Family.Value] = None) {
def detect(s: String): Boolean =
s.startsWith("#bundled") && !s.startsWith("#bundled ")
def apply(name: String): String =
"#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
private val Pattern1 = ("""^#bundled:(.*)$""").r
private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
def unapply(s: String): Option[String] =
s match {
case Pattern1(name) => Some(name)
case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
case _ => None
}
}
def record_bundled_components(dir: Path): Unit = {
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
Platform.Family.list.flatMap(platform =>
List(platform.toString, "bundled-" + platform.toString).
map((_, new Bundled(platform = Some(platform)))))
File.append(Components.Directory(dir).components,
terminate_lines("#bundled components" ::
(for {
(catalog, bundled) <- catalogs.iterator
path = Components.admin(dir) + Path.basic(catalog)
if path.is_file
line <- split_lines(File.read(path))
if line.nonEmpty && !line.startsWith("#")
} yield bundled(line)).toList))
}
def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = {
val Bundled = new Bundled(platform = Some(platform))
val components =
for { Bundled(name) <- Components.Directory(dir).read_components() } yield name
val jdk_component =
components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
(components, jdk_component)
}
def activate_components(
dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit = {
def contrib_name(name: String): String =
Components.contrib(name = name).implode
val Bundled = new Bundled(platform = Some(platform))
val component_dir = Components.Directory(dir)
component_dir.write_components(
component_dir.read_components().flatMap(line =>
line match {
case Bundled(name) =>
if (Components.Directory(Components.contrib(dir, name)).check) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
}) ::: more_names.map(contrib_name))
}
/** build release **/
/* build heaps */
private def build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path,
progress: Progress = new Progress,
): Unit = {
val server_option = "build_host_" + platform.toString
val server = options.string(server_option)
progress.echo("Building heaps for " + commas_quote(build_sessions) +
" (" + server_option + " = " + quote(server) + ") ...")
val ssh =
if (server.nonEmpty) SSH.open_session(options, server)
else if (Platform.family == platform) SSH.Local
else error("Undefined option " + server_option + ": cannot build heaps")
try {
Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar =>
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
ssh.with_tmp_dir { remote_dir =>
val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val build_command =
"bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions)
def system_apple(b: Boolean): String =
"""{ echo "ML_system_apple = """ + b + """" > "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc/preferences"; }"""
val build_script =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
"""mkdir -p "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc" """,
system_apple(false),
build_command,
system_apple(true),
build_command,
"tar -cf tmp.tar heaps")
ssh.execute(build_script.mkString(" && "), settings = false).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
}
execute_tar(local_dir, "-xvf " + File.bash_path(local_tmp_tar))
.out_lines.sorted.foreach(progress.echo)
}
}
finally { ssh.close() }
}
/* Isabelle application */
def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit = {
val title = "# Java runtime options"
File.write(path, (title :: options).map(_ + line_ending).mkString)
}
def make_isabelle_app(
platform: Platform.Family.Value,
isabelle_target: Path,
isabelle_name: String,
jdk_component: String,
classpath: List[Path],
dock_icon: Boolean = false): Unit = {
val script = """#!/usr/bin/env bash
#
# Author: Makarius
#
# Main Isabelle application script.
# minimal Isabelle environment
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
unset "JAVA_TOOL_OPTIONS"
#paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
unset XMODIFIERS
COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """"
source "$COMPONENT/etc/settings"
# main
declare -a JAVA_OPTIONS=($(grep -v '^#' "$ISABELLE_HOME/Isabelle.options"))
"$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup"
exec "$ISABELLE_JDK_HOME/bin/java" \
"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
-classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \
"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
""" + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \
""" else "") + """isabelle.jedit.JEdit_Main "$@"
"""
val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
File.write(script_path, script)
File.set_executable(script_path, true)
val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app")
Isabelle_System.move_file(
component_dir + Path.explode(Platform.Family.standard(platform)) + Path.explode("Isabelle"),
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(component_dir)
}
def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit = {
File.write(path, """
CFBundleDevelopmentRegion
English
CFBundleIconFile
isabelle.icns
CFBundleIdentifier
de.tum.in.isabelle
CFBundleDisplayName
""" + isabelle_name + """
CFBundleInfoDictionaryVersion
6.0
CFBundleName
""" + isabelle_name + """
CFBundlePackageType
APPL
CFBundleShortVersionString
""" + isabelle_name + """
CFBundleSignature
????
CFBundleVersion
""" + isabelle_rev + """
NSHumanReadableCopyright
LSMinimumSystemVersion
10.11
LSApplicationCategoryType
public.app-category.developer-tools
NSHighResolutionCapable
true
NSSupportsAutomaticGraphicsSwitching
true
CFBundleDocumentTypes
CFBundleTypeExtensions
thy
CFBundleTypeIconFile
theory.icns
CFBundleTypeName
Isabelle theory file
CFBundleTypeRole
Editor
LSTypeIsPackage
""")
}
/* main */
def use_release_archive(
context: Release_Context,
archive: Release_Archive,
id: String = ""
): Unit = {
if (id.nonEmpty && id != archive.id) {
error("Mismatch of release identification " + id + " vs. archive " + archive.id)
}
if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) {
Bytes.write(context.isabelle_archive, archive.bytes)
}
}
def build_release_archive(
context: Release_Context,
version: String,
parallel_jobs: Int = 1
): Unit = {
val progress = context.progress
val hg = Mercurial.self_repository()
val id =
try { hg.id(version) }
catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
if (context.isabelle_archive.is_file) {
progress.echo_warning("Found existing release archive: " + context.isabelle_archive)
use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id)
}
else {
progress.echo_warning("Preparing release " + context.dist_name + " ...")
Isabelle_System.new_directory(context.dist_dir)
hg.archive(context.isabelle_dir.expand.implode, rev = id)
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
(context.isabelle_dir + Path.explode(name)).file.delete
}
File.write(context.isabelle_dir + ISABELLE_ID, id)
File.write(context.isabelle_dir + ISABELLE_TAGS, hg.tags(rev = id))
File.write(context.isabelle_dir + ISABELLE_IDENTIFIER, context.dist_name)
context.make_announce(id)
context.make_contrib()
execute(context.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(context.isabelle_dir)
/* build tools and documentation */
val other_isabelle = context.other_isabelle(context.dist_dir)
other_isabelle.init_settings(
other_isabelle.init_components(
components_base = context.components_base, catalogs = List("main")))
other_isabelle.resolve_components(echo = true)
try {
other_isabelle.bash(
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" +
"bin/isabelle jedit -b", echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
try {
other_isabelle.bash(
"bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
other_isabelle.make_news()
for (name <- List("Admin", "browser_info", "heaps")) {
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
}
other_isabelle.cleanup()
progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...")
execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""")
execute(context.dist_dir,
"""find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
execute_tar(context.dist_dir, "-czf " +
File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
}
}
def default_platform_families: List[Platform.Family.Value] = Platform.Family.list0
def build_release(
options: Options,
context: Release_Context,
afp_rev: String = "",
platform_families: List[Platform.Family.Value] = default_platform_families,
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_sessions: List[String] = Nil,
build_library: Boolean = false,
parallel_jobs: Int = 1
): Unit = {
val progress = context.progress
/* release directory */
val archive = Release_Archive.read(context.isabelle_archive)
for (path <- List(context.isabelle, ISABELLE)) {
Isabelle_System.rm_tree(context.dist_dir + path)
}
Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path =>
Bytes.write(archive_path, archive.bytes)
val extract =
List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
map(name => context.dist_name + "/" + name)
execute_tar(context.dist_dir,
"-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
}
Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE)
/* make application bundles */
val bundle_infos = platform_families.map(context.bundle_info)
for (bundle_info <- bundle_infos) {
val isabelle_name = context.dist_name
val platform = bundle_info.platform
progress.echo("\nApplication bundle for " + platform)
Isabelle_System.with_tmp_dir("build_release") { tmp_dir =>
// release archive
execute_tar(tmp_dir, "-xzf " + File.bash_path(context.isabelle_archive))
val other_isabelle = context.other_isabelle(tmp_dir)
val isabelle_target = other_isabelle.isabelle_home
// bundled components
progress.echo("Bundled components:")
val contrib_dir = Components.contrib(isabelle_target)
val (bundled_components, jdk_component) =
get_bundled_components(isabelle_target, platform)
Components.resolve(context.components_base, bundled_components,
target_dir = Some(contrib_dir),
copy_dir = Some(context.dist_dir + Path.explode("contrib")),
progress = progress)
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
activate_components(isabelle_target, platform, more_components_names)
// Java parameters
val java_options: List[String] =
(for {
variable <-
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_OPTIONS")
opt <- Word.explode(other_isabelle.getenv(variable))
}
yield {
val s = "-Dapple.awt.application.name="
if (opt.startsWith(s)) s + isabelle_name else opt
}) ::: List("-Disabelle.jedit_server=" + isabelle_name)
val classpath: List[Path] = {
val base = isabelle_target.absolute
val classpath1 = Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH"))
val classpath2 = Path.split(other_isabelle.getenv("ISABELLE_SETUP_CLASSPATH"))
(classpath1 ::: classpath2).map { path =>
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
case None => error("Bad classpath element: " + abs_path)
}
}
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props =
Path.explode(other_isabelle.getenv("JEDIT_HOME") + "/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
build_heaps(options, platform, build_sessions, isabelle_target, progress = progress)
}
// application bundling
Components.purge(contrib_dir, platform)
platform match {
case Platform.Family.linux_arm | Platform.Family.linux =>
File.change(isabelle_target + jedit_options) {
_.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24")
}
File.change(isabelle_target + jedit_props) {
_.replaceAll("console.fontsize=.*", "console.fontsize=18")
.replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
.replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
.replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
.replaceAll("view.fontsize=.*", "view.fontsize=24")
.replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16")
}
make_isabelle_options(
isabelle_target + Path.explode("Isabelle.options"), java_options)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath)
progress.echo("Packaging " + bundle_info.name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " +
Bash.string(isabelle_name))
case Platform.Family.macos =>
File.change(isabelle_target + jedit_props) {
_.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
.replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
}
// macOS application bundle
val app_contents = isabelle_target + Path.explode("Contents")
for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
Isabelle_System.copy_file(isabelle_target + Path.explode(icon),
Isabelle_System.make_directory(app_contents + Path.explode("Resources")))
}
make_isabelle_plist(
app_contents + Path.explode("Info.plist"), isabelle_name, archive.id)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
classpath, dock_icon = true)
val isabelle_options = Path.explode("Isabelle.options")
make_isabelle_options(
isabelle_target + isabelle_options,
java_options ::: List("-Disabelle.app=true"))
// application archive
progress.echo("Packaging " + bundle_info.name + " ...")
val isabelle_app = Path.explode(isabelle_name + ".app")
Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name),
tmp_dir + isabelle_app)
execute_tar(tmp_dir,
"-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " +
File.bash_path(isabelle_app))
case Platform.Family.windows =>
File.change(isabelle_target + jedit_props) {
_.replaceAll("foldPainter=.*", "foldPainter=Square")
}
// application launcher
Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
val app_template = Path.explode("~~/Admin/Windows/launch4j")
make_isabelle_options(
isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
java_options, line_ending = "\r\n")
val isabelle_xml = Path.explode("isabelle.xml")
val isabelle_exe = bundle_info.path
File.write(tmp_dir + isabelle_xml,
File.read(app_template + isabelle_xml)
.replace("{ISABELLE_NAME}", isabelle_name)
.replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
.replace("{ICON}",
File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
.replace("{SPLASH}",
File.platform_path(app_template + Path.explode("isabelle.bmp")))
.replace("{CLASSPATH}",
cat_lines(classpath.map(cp =>
" %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
.replace("\\jdk\\", "\\" + jdk_component + "\\"))
val java_opts =
bash_java_opens(
"java.base/java.io",
"java.base/java.lang",
"java.base/java.lang.reflect",
"java.base/java.text",
"java.base/java.util",
"java.desktop/java.awt.font")
val launch4j_jar =
Path.explode("windows_app/launch4j-" + Platform.family + "/launch4j.jar")
execute(tmp_dir,
cat_lines(List(
"export LAUNCH4J=" + File.bash_platform_path(launch4j_jar),
"isabelle java " + java_opts + " -jar \"$LAUNCH4J\" isabelle.xml")))
Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
isabelle_target + isabelle_exe.ext("manifest"))
// Cygwin setup
val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"),
isabelle_target)
val cygwin_mirror =
File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
val cygwin_bat = Path.explode("Cygwin-Setup.bat")
File.write(isabelle_target + cygwin_bat,
File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror))
File.set_executable(isabelle_target + cygwin_bat, true)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
Isabelle_System.copy_file(cygwin_template + path,
isabelle_target + Path.explode("contrib/cygwin") + path)
}
execute(isabelle_target,
"""find . -type f -not -name "*.exe" -not -name "*.dll" """ +
(if (Platform.is_macos) "-perm +100" else "-executable") +
" -print0 > contrib/cygwin/isabelle/executables")
execute(isabelle_target,
"""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
"""> contrib/cygwin/isabelle/symlinks""")
execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
// executable archive (self-extracting 7z)
val archive_name = isabelle_name + ".7z"
val exe_archive = tmp_dir + Path.explode(archive_name)
exe_archive.file.delete
progress.echo("Packaging " + archive_name + " ...")
execute(tmp_dir,
"7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
val sfx_txt =
File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt"))
.replace("{ISABELLE_NAME}", isabelle_name)
Bytes.write(context.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.set_executable(context.dist_dir + isabelle_exe, true)
}
}
progress.echo("DONE")
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
if (context.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id),
HTML.text("Isabelle/" + archive.id))
val afp_link =
HTML.link(Isabelle_System.afp_repository.changeset(afp_rev),
HTML.text("AFP/" + afp_rev))
HTML.write_document(dir, "index.html",
List(HTML.title(context.dist_name)),
List(
HTML.section(context.dist_name),
HTML.subsection("Downloads"),
HTML.itemize(
List(HTML.link(context.dist_name + ".tar.gz", HTML.text("Source archive"))) ::
website_platform_bundles.map({ case (bundle, bundle_info) =>
List(HTML.link(bundle, HTML.text(bundle_info.platform_description + " bundle"))) })),
HTML.subsection("Repositories"),
HTML.itemize(
List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
Isabelle_System.copy_file(context.isabelle_archive, dir)
for ((bundle, _) <- website_platform_bundles) {
Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir)
}
}
/* HTML library */
if (build_library) {
if (context.isabelle_library_archive.is_file) {
progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
}
else {
Isabelle_System.with_tmp_dir("build_release") { tmp_dir =>
val bundle =
context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle = context.other_isabelle(tmp_dir)
Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n")
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
other_isabelle.isabelle_home_user.file.delete
execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name))
execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
" " + Bash.string(context.dist_name + "/browser_info"))
}
}
}
}
/** command line entry point **/
def main(args: Array[String]): Unit = {
Command_Line.tool {
var afp_rev = ""
var components_base: Path = Components.default_components_base
var target_dir = Path.current
var release_name = ""
var source_archive = ""
var website: Option[Path] = None
var build_sessions: List[String] = Nil
var more_components: List[Path] = Nil
var parallel_jobs = 1
var build_library = false
var options = Options.init()
var platform_families = default_platform_families
var rev = ""
val getopts = Getopts("""
Usage: Admin/build_release [OPTIONS]
Options are:
-A REV corresponding AFP changeset id
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-D DIR target directory (default ".")
-R RELEASE explicit release name
-S ARCHIVE use existing source archive (file or URL)
-W WEBSITE produce minimal website in given directory
-b SESSIONS build platform-specific session images (separated by commas)
-c ARCHIVE clean bundling with additional component .tar.gz archive
-j INT maximum number of parallel jobs (default 1)
-l build library
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NAMES platform families (default: """ + default_platform_families.mkString(",") + """)
-r REV Mercurial changeset id (default: ARCHIVE or RELEASE or tip)
Build Isabelle release in base directory, using the local repository clone.
""",
"A:" -> (arg => afp_rev = arg),
"C:" -> (arg => components_base = Path.explode(arg)),
"D:" -> (arg => target_dir = Path.explode(arg)),
"R:" -> (arg => release_name = arg),
"S:" -> (arg => source_archive = arg),
"W:" -> (arg => website = Some(Path.explode(arg))),
"b:" -> (arg => build_sessions = space_explode(',', arg)),
"c:" -> (arg =>
{
val path = Path.explode(arg)
Components.Archive.get_name(path.file_name)
more_components = more_components ::: List(path)
}),
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
"l" -> (_ => build_library = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
"r:" -> (arg => rev = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
val progress = new Console_Progress()
def make_context(name: String): Release_Context =
Release_Context(target_dir,
release_name = name,
components_base = components_base,
progress = progress)
val context =
if (source_archive.isEmpty) {
val context = make_context(release_name)
val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
build_release_archive(context, version, parallel_jobs = parallel_jobs)
context
}
else {
val archive =
Release_Archive.get(source_archive, rename = release_name, progress = progress)
val context = make_context(archive.identifier)
Isabelle_System.make_directory(context.dist_dir)
use_release_archive(context, archive, id = rev)
context
}
build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs, website = website)
}
}
}
diff --git a/src/Pure/Admin/build_scala.scala b/src/Pure/Admin/build_scala.scala
--- a/src/Pure/Admin/build_scala.scala
+++ b/src/Pure/Admin/build_scala.scala
@@ -1,174 +1,173 @@
/* Title: Pure/Admin/build_scala.scala
Author: Makarius
Build Isabelle Scala component from official downloads.
*/
package isabelle
object Build_Scala {
/* downloads */
sealed case class Download(
name: String,
version: String,
url: String,
physical_url: String = "",
base_version: String = "3"
) {
def make_url(template: String): String =
template.replace("{V}", version).replace("{B}", base_version)
def proper_url: String = make_url(proper_string(physical_url).getOrElse(url))
def artifact: String =
Library.take_suffix[Char](_ != '/', proper_url.toList)._2.mkString
def get(path: Path, progress: Progress = new Progress): Unit =
Isabelle_System.download_file(proper_url, path, progress = progress)
- def get_unpacked(dir: Path, strip: Int = 0, progress: Progress = new Progress): Unit =
- Isabelle_System.with_tmp_file("archive"){ archive_path =>
+ def get_unpacked(dir: Path, strip: Boolean = false, progress: Progress = new Progress): Unit =
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz"){ archive_path =>
get(archive_path, progress = progress)
progress.echo("Unpacking " + artifact)
- Isabelle_System.gnutar(
- "-xzf " + File.bash_path(archive_path), dir = dir, strip = strip).check
+ Isabelle_System.extract(archive_path, dir, strip = strip)
}
def print: String =
" * " + name + " " + version +
(if (base_version.nonEmpty) " for Scala " + base_version else "") +
":\n " + make_url(url)
}
val main_download: Download =
Download("scala", "3.2.1", base_version = "",
url = "https://github.com/lampepfl/dotty/releases/download/{V}/scala3-{V}.tar.gz")
val lib_downloads: List[Download] = List(
Download("scala-parallel-collections", "1.0.4",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parallel-collections_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parallel-collections_{B}/{V}/scala-parallel-collections_{B}-{V}.jar"),
Download("scala-parser-combinators", "2.1.1",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parser-combinators_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parser-combinators_{B}/{V}/scala-parser-combinators_{B}-{V}.jar"),
Download("scala-swing", "3.0.0",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-swing_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-swing_{B}/{V}/scala-swing_{B}-{V}.jar"),
Download("scala-xml", "2.1.0",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-xml_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-xml_{B}/{V}/scala-xml_{B}-{V}.jar")
)
/* build Scala component */
def build_scala(
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
/* component */
val component_name = main_download.name + "-" + main_download.version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
/* download */
- main_download.get_unpacked(component_dir.path, strip = 1, progress = progress)
+ main_download.get_unpacked(component_dir.path, strip = true, progress = progress)
lib_downloads.foreach(download =>
download.get(component_dir.lib + Path.basic(download.artifact), progress = progress))
File.write(component_dir.LICENSE,
Url.read(Url("https://www.apache.org/licenses/LICENSE-2.0.txt")))
/* classpath */
val classpath: List[String] = {
def no_function(name: String): String = "function " + name + "() {\n:\n}"
val script =
cat_lines(List(
no_function("stty"),
no_function("tput"),
"PROG_HOME=" + File.bash_path(component_dir.path),
File.read(component_dir.path + Path.explode("bin/common"))
.replace("scala_exit_status=127", "scala_exit_status=0"),
"compilerJavaClasspathArgs",
"echo \"$jvm_cp_args\""))
val main_classpath = Path.split(Isabelle_System.bash(script).check.out).map(_.file_name)
val lib_classpath = lib_downloads.map(_.artifact)
main_classpath ::: lib_classpath
}
val interfaces =
classpath.find(_.startsWith("scala3-interfaces"))
.getOrElse(error("Missing jar for scala3-interfaces"))
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
SCALA_HOME="$COMPONENT"
SCALA_INTERFACES="$SCALA_HOME/lib/""" + interfaces + """"
""" + terminate_lines(classpath.map(jar => "classpath \"$SCALA_HOME/lib/" + jar + "\"")))
/* adhoc changes */
val patched_scripts = List("bin/scala", "bin/scalac")
for (name <- patched_scripts) {
File.change(component_dir.path + Path.explode(name)) {
_.replace(""""-Dscala.home=$PROG_HOME"""", """"-Dscala.home=\"$PROG_HOME\""""")
}
}
/* README */
File.write(component_dir.README,
"This distribution of Scala integrates the following parts:\n\n" +
(main_download :: lib_downloads).map(_.print).mkString("\n\n") + """
Minor changes to """ + patched_scripts.mkString(" and ") + """ allow an installation location
with spaces in the directory name.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_scala", "build Isabelle Scala component from official downloads",
Scala_Project.here,
{ args =>
var target_dir = Path.current
val getopts = Getopts("""
Usage: isabelle build_scala [OPTIONS]
Options are:
-D DIR target directory (default ".")
Build Isabelle Scala component from official downloads.
""",
"D:" -> (arg => target_dir = Path.explode(arg)))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_scala(target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_spass.scala b/src/Pure/Admin/build_spass.scala
--- a/src/Pure/Admin/build_spass.scala
+++ b/src/Pure/Admin/build_spass.scala
@@ -1,178 +1,176 @@
/* Title: Pure/Admin/build_spass.scala
Author: Makarius
Build Isabelle SPASS component from unofficial download.
*/
package isabelle
object Build_SPASS {
/* build SPASS */
val default_download_url = "https://www.cs.vu.nl/~jbe248/spass-3.8ds-src.tar.gz"
val standard_version = "3.8ds"
def build_spass(
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current): Unit = {
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
Isabelle_System.require_command("bison")
Isabelle_System.require_command("flex")
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
val Component_Name = """^(.+)-src\.tar.gz$""".r
val Version = """^[^-]+-([^-]+)$""".r
- val (archive_name, archive_base_name) =
+ val archive_name =
download_url match {
- case Archive_Name(name) => (name, Library.perhaps_unsuffix(".tar.gz", name))
+ case Archive_Name(name) => name
case _ => error("Failed to determine source archive name from " + quote(download_url))
}
val component_name =
archive_name match {
case Component_Name(name) => name
case _ => error("Failed to determine component name from " + quote(archive_name))
}
val version =
component_name match {
case Version(version) => version
case _ => error("Failed to determine component version from " + quote(component_name))
}
if (version != standard_version) {
progress.echo_warning("Odd SPASS version " + version + " (expected " + standard_version + ")")
}
val component_dir =
Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
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 " + archive_path, cwd = tmp_dir.file).check
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(archive_base_name) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
+
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
progress.echo("Building SPASS for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic(archive_base_name)
-
if (Platform.is_windows) {
- File.change(build_dir + Path.basic("misc.c")) {
+ File.change(source_dir + Path.basic("misc.c")) {
_.replace("""#include "execinfo.h" """, "")
.replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }")
}
}
- Isabelle_System.bash("make",
- cwd = build_dir.file,
+ Isabelle_System.bash("make", cwd = source_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.basic("LICENCE"), component_dir.LICENSE)
+ Isabelle_System.copy_file(source_dir + Path.basic("LICENCE"), component_dir.LICENSE)
val install_files = List("SPASS")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
- val path = build_dir + Path.basic(name)
+ val path = source_dir + Path.basic(name)
if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
}
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
SPASS_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
SPASS_VERSION=""" + quote(version) + """
""")
/* README */
File.write(component_dir.README,
"""This distribution of SPASS 3.8ds, described in Blanchette, Popescu, Wand, and
Weidenbach's ITP 2012 paper "More SPASS with Isabelle", has been compiled from
sources available at """ + download_url + """
via "make".
The Windows/Cygwin compilation required commenting out the line
#include "execinfo.h"
in "misc.c" as well as most of the body of the "misc_DumpCore" function.
The latest official SPASS sources can be downloaded from
http://www.spass-prover.org/. Be aware, however, that the official SPASS
releases are not compatible with Isabelle.
Viel SPASS!
Jasmin Blanchette
16-May-2018
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_spass", "build prover component from source distribution",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_download_url
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_spass [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL
(default: """" + default_download_url + """")
-v verbose
Build prover component from the specified source distribution.
""",
"D:" -> (arg => target_dir = 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_spass(download_url = download_url, 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,163 +1,162 @@
/* 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
+ Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
progress.echo("Building Vampire for " + platform_name + " ...")
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 = 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 = source_dir.file, echo = verbose).check
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,156 +1,155 @@
/* 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
+ Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
progress.echo("Building veriT for " + platform_name + " ...")
val configure_options =
if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else ""
progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"),
cwd = source_dir.file, echo = verbose).check
/* install */
Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
val exe_path = Path.basic("veriT").platform_exe
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,378 +1,380 @@
/* 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_tar_bz2(s: String): Boolean = s.endsWith(".tar.bz2")
def is_tar_gz(s: String): Boolean = s.endsWith(".tar.gz")
+ def is_tgz(s: String): Boolean = s.endsWith(".tgz")
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_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/mercurial.scala b/src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala
+++ b/src/Pure/General/mercurial.scala
@@ -1,619 +1,619 @@
/* Title: Pure/General/mercurial.scala
Author: Makarius
Support for Mercurial repositories, with local or remote repository clone
and working directory (via ssh connection).
*/
package isabelle
import scala.annotation.tailrec
import scala.collection.mutable
object Mercurial {
type Graph = isabelle.Graph[String, Unit]
/** HTTP server **/
object Server {
def apply(root: String): Server = new Server(root)
def start(root: Path): Server = {
val hg = repository(root)
val server_process = Future.promise[Bash.Process]
val server_root = Future.promise[String]
Isabelle_Thread.fork("hg") {
val process =
Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) }
server_process.fulfill_result(process)
Exn.release(process).result(progress_stdout =
line => if (!server_root.is_finished) {
server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line))
})
}
server_process.join
new Server(server_root.join) {
override def close(): Unit = server_process.join.terminate()
}
}
}
class Server private(val root: String) extends AutoCloseable {
override def toString: String = root
def close(): Unit = ()
def changeset(rev: String = "tip", raw: Boolean = false): String =
root + (if (raw) "/raw-rev/" else "/rev/") + rev
def file(path: Path, rev: String = "tip", raw: Boolean = false): String =
root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + path.expand.implode
def archive(rev: String = "tip"): String =
root + "/archive/" + rev + ".tar.gz"
def read_changeset(rev: String = "tip"): String =
Url.read(changeset(rev = rev, raw = true))
def read_file(path: Path, rev: String = "tip"): String =
Url.read(file(path, rev = rev, raw = true))
def download_archive(rev: String = "tip", progress: Progress = new Progress): HTTP.Content =
Isabelle_System.download(archive(rev = rev), progress = progress)
def download_dir(dir: Path, rev: String = "tip", progress: Progress = new Progress): Unit = {
Isabelle_System.new_directory(dir)
Isabelle_System.with_tmp_file("rev", ext = ".tar.gz") { archive_path =>
val content = download_archive(rev = rev, progress = progress)
Bytes.write(archive_path, content.bytes)
progress.echo("Unpacking " + rev + ".tar.gz")
Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
- dir = dir, original_owner = true, strip = 1).check
+ dir = dir, original_owner = true, strip = true).check
}
}
}
/** repository commands **/
/* command-line syntax */
def optional(s: String, prefix: String = ""): String =
if (s == "") "" else " " + prefix + " " + Bash.string(s)
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
def opt_rev(s: String): String = optional(s, "--rev")
def opt_template(s: String): String = optional(s, "--template")
/* repository archives */
private val Archive_Node = """^node: (\S{12}).*$""".r
private val Archive_Tag = """^tag: (\S+).*$""".r
sealed case class Archive_Info(lines: List[String]) {
def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a })
def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag
}
def archive_info(root: Path): Option[Archive_Info] = {
val path = root + Path.explode(".hg_archival.txt")
if (path.is_file) Some(Archive_Info(Library.trim_split_lines(File.read(path)))) else None
}
def archive_id(root: Path): Option[String] =
archive_info(root).flatMap(_.id)
def archive_tags(root: Path): Option[String] =
archive_info(root).map(info => info.tags.mkString(" "))
/* hg_sync meta data */
object Hg_Sync {
val NAME = ".hg_sync"
val _NAME: String = " " + NAME
val PATH: Path = Path.explode(NAME)
val PATH_ID: Path = PATH + Path.explode("id")
val PATH_LOG: Path = PATH + Path.explode("log")
val PATH_DIFF: Path = PATH + Path.explode("diff")
val PATH_STAT: Path = PATH + Path.explode("stat")
def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean =
ssh.is_dir(root + PATH)
def directory(root: Path, ssh: SSH.System = SSH.Local): Directory = {
if (is_directory(root, ssh = ssh)) new Directory(root, ssh)
else error("No .hg_sync directory found in " + ssh.rsync_path(root))
}
class Directory private [Hg_Sync](val root: Path, val ssh: SSH.System)
{
override def toString: String = ssh.rsync_path(root)
def read(path: Path): String = ssh.read(root + path)
lazy val id: String = read(PATH_ID)
lazy val log: String = read(PATH_LOG)
lazy val diff: String = read(PATH_DIFF)
lazy val stat: String = read(PATH_STAT)
def changed: Boolean = id.endsWith("+")
}
}
/* repository access */
def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
ssh.is_dir(root + Path.explode(".hg")) &&
new Repository(root, ssh).command("root").ok
def id_repository(root: Path, ssh: SSH.System = SSH.Local, rev: String = "tip"): Option[String] =
if (is_repository(root, ssh = ssh)) Some(repository(root, ssh = ssh).id(rev = rev)) else None
def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = {
val hg = new Repository(root, ssh)
hg.command("root").check
hg
}
def self_repository(): Repository = repository(Path.ISABELLE_HOME)
def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = {
@tailrec def find(root: Path): Option[Repository] =
if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
else if (root.is_root) None
else find(root + Path.parent)
find(ssh.expand_path(start))
}
def the_repository(start: Path, ssh: SSH.System = SSH.Local): Repository =
find_repository(start, ssh = ssh) getOrElse
error("No repository found in " + start.absolute)
private def make_repository(
root: Path,
cmd: String,
args: String,
ssh: SSH.System = SSH.Local
) : Repository = {
val hg = new Repository(root, ssh)
ssh.make_directory(hg.root.dir)
hg.command(cmd, args, repository = false).check
hg
}
def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
def clone_repository(source: String, root: Path,
rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
make_repository(root, "clone",
options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = {
if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
else clone_repository(source, root, options = "--noupdate", ssh = ssh)
}
class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) {
hg =>
val root: Path = ssh.expand_path(root_path)
def root_url: String = ssh.hg_url + root.implode
override def toString: String = ssh.hg_url + root.implode
def command_line(
name: String,
args: String = "",
options: String = "",
repository: Boolean = true
): String = {
"export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
(if (repository) " --repository " + ssh.bash_path(root) else "") +
" --noninteractive " + name + " " + options + " " + args
}
def command(
name: String,
args: String = "",
options: String = "",
repository: Boolean = true
): Process_Result = {
ssh.execute(command_line(name, args = args, options = options, repository = repository))
}
def add(files: List[Path]): Unit =
hg.command("add", files.map(ssh.bash_path).mkString(" "))
def archive(target: String, rev: String = "", options: String = ""): Unit =
hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
hg.command("heads", opt_template(template), options).check.out_lines
def identify(rev: String = "tip", options: String = ""): String =
hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
def id(rev: String = "tip"): String = identify(rev, options = "-i")
def tags(rev: String = "tip"): String = {
val result = identify(rev, options = "-t")
Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
}
def paths(args: String = "", options: String = ""): List[String] =
hg.command("paths", args = args, options = options).check.out_lines
def manifest(rev: String = "", options: String = ""): List[String] =
hg.command("manifest", opt_rev(rev), options).check.out_lines
def log(rev: String = "", template: String = "", options: String = ""): String =
hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
def diff(rev: String = "", options: String = ""): String =
hg.command("diff", opt_rev(rev), options).check.out
def parent(): String = log(rev = "p1()", template = "{node|short}")
def push(
remote: String = "",
rev: String = "",
force: Boolean = false,
options: String = ""
): Unit = {
hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
check_rc(rc => rc == 0 | rc == 1)
}
def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
hg.command("pull", opt_rev(rev) + optional(remote), options).check
def update(
rev: String = "",
clean: Boolean = false,
check: Boolean = false,
options: String = ""
): Unit = {
hg.command("update",
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
}
def status(options: String = ""): List[String] =
hg.command("status", options = options).check.out_lines
def known_files(): List[String] = status(options = "--modified --added --clean --no-status")
def sync(context: Rsync.Context, target: String,
verbose: Boolean = false,
thorough: Boolean = false,
dry_run: Boolean = false,
filter: List[String] = Nil,
contents: List[File.Content] = Nil,
rev: String = ""
): Unit = {
require(ssh == SSH.Local, "local repository required")
Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
val context0 = context.copy(progress = new Progress)
Rsync.init(context0, target)
val list =
Rsync.exec(context0, list = true, args = List("--", Rsync.terminate(target)))
.check.out_lines.filterNot(_.endsWith(" ."))
if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
error("No .hg_sync meta data in " + quote(target))
}
val id_content = id(rev = rev)
val is_changed = id_content.endsWith("+")
val log_content = if (is_changed) "" else log(rev = rev, options = "-l1")
val diff_content = if (is_changed) diff(rev = rev, options = "--git") else ""
val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else ""
Rsync.init(context0, target,
contents =
File.content(Hg_Sync.PATH_ID, id_content) ::
File.content(Hg_Sync.PATH_LOG, log_content) ::
File.content(Hg_Sync.PATH_DIFF, diff_content) ::
File.content(Hg_Sync.PATH_STAT, stat_content) :: contents)
val (exclude, source) =
if (rev.isEmpty) {
val exclude = ".hg" :: status(options = "--unknown --ignored --no-status")
val source = File.standard_path(root)
(exclude, source)
}
else {
val exclude = List(".hg_archival.txt")
val source = File.standard_path(tmp_dir + Path.explode("archive"))
archive(source, rev = rev)
(exclude, source)
}
val exclude_path = tmp_dir + Path.explode("exclude")
File.write(exclude_path, cat_lines(exclude.map("/" + _)))
val protect =
(Hg_Sync.PATH :: contents.map(_.path))
.map(path => "protect /" + File.standard_path(path))
Rsync.exec(context,
verbose = verbose,
thorough = thorough,
dry_run = dry_run,
clean = true,
prune_empty_dirs = true,
filter = protect ::: filter,
args = List("--exclude-from=" + exclude_path.implode, "--",
Rsync.terminate(source), target)
).check
}
}
def graph(): Graph = {
val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
val log_result =
log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
split_lines(log_result).foldLeft(Graph.string[Unit]) {
case (graph, Node(x, y, z)) =>
val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ()))
deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) })
case (graph, _) => graph
}
}
}
/** check files **/
def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) = {
val outside = new mutable.ListBuffer[Path]
val unknown = new mutable.ListBuffer[Path]
@tailrec def check(paths: List[Path]): Unit = {
paths match {
case path :: rest =>
find_repository(path, ssh) match {
case None => outside += path; check(rest)
case Some(hg) =>
val known =
hg.known_files().iterator.map(name =>
(hg.root + Path.explode(name)).canonical_file).toSet
if (!known(path.canonical_file)) unknown += path
check(rest.filterNot(p => known(p.canonical_file)))
}
case Nil =>
}
}
check(files)
(outside.toList, unknown.toList)
}
/** hg_setup **/
private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit = {
val hgrc = local_hg.root + Path.explode(".hg/hgrc")
def header(line: String): Boolean = line.startsWith("[paths]")
val Entry = """^(\S+)\s*=\s*(.*)$""".r
val new_entry = path_name + " = " + source
def commit(lines: List[String]): Boolean = {
File.write(hgrc, cat_lines(lines))
true
}
val edited =
hgrc.is_file && {
val lines = split_lines(File.read(hgrc))
lines.count(header) == 1 && {
if (local_hg.paths(options = "-q").contains(path_name)) {
val old_source = local_hg.paths(args = path_name).head
val old_entry = path_name + ".old = " + old_source
val lines1 =
lines.map {
case Entry(a, b) if a == path_name && b == old_source =>
new_entry + "\n" + old_entry
case line => line
}
lines != lines1 && commit(lines1)
}
else {
val prefix = lines.takeWhile(line => !header(line))
val n = prefix.length
commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1))
}
}
}
if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n")
}
val default_path_name = "default"
def hg_setup(
remote: String,
local_path: Path,
remote_name: String = "",
path_name: String = default_path_name,
remote_exists: Boolean = false,
progress: Progress = new Progress
): Unit = {
/* local repository */
Isabelle_System.make_directory(local_path)
val repos_name =
proper_string(remote_name) getOrElse local_path.absolute.base.implode
val local_hg =
if (is_repository(local_path)) repository(local_path)
else init_repository(local_path)
progress.echo("Local repository " + local_hg.root.absolute)
/* remote repository */
val remote_url = {
if (remote.startsWith("ssh://")) {
val ssh_url = remote + "/" + repos_name
if (!remote_exists) {
try { local_hg.command("init", ssh_url, repository = false).check }
catch { case ERROR(msg) => progress.echo_warning(msg) }
}
ssh_url
}
else {
val phabricator = Phabricator.API(remote)
var repos =
phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
if (remote_exists) {
error("Remote repository " +
quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
}
else phabricator.create_repository(repos_name, short_name = repos_name)
}
while (repos.importing) {
progress.echo("Awaiting remote repository ...")
Time.seconds(0.5).sleep()
repos = phabricator.the_repository(repos.phid)
}
repos.ssh_url
}
}
progress.echo("Remote repository " + quote(remote_url))
/* synchronize local and remote state */
progress.echo("Synchronizing ...")
edit_hgrc(local_hg, path_name, remote_url)
local_hg.pull(options = "-u")
local_hg.push(remote = remote_url)
}
val isabelle_tool1 =
Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository",
Scala_Project.here,
{ args =>
var remote_name = ""
var path_name = default_path_name
var remote_exists = false
val getopts = Getopts("""
Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
Options are:
-n NAME remote repository name (default: base name of LOCAL_DIR)
-p PATH Mercurial path name (default: """ + quote(default_path_name) + """)
-r assume that remote repository already exists
Setup a remote vs. local Mercurial repository: REMOTE either refers to a
Phabricator server "user@host" or SSH file server "ssh://user@host/path".
""",
"n:" -> (arg => remote_name = arg),
"p:" -> (arg => path_name = arg),
"r" -> (_ => remote_exists = true))
val more_args = getopts(args)
val (remote, local_path) =
more_args match {
case List(arg1, arg2) => (arg1, Path.explode(arg2))
case _ => getopts.usage()
}
val progress = new Console_Progress
hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
remote_exists = remote_exists, progress = progress)
})
/** hg_sync **/
val isabelle_tool2 =
Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
Scala_Project.here, { args =>
var filter: List[String] = Nil
var protect_args = false
var root: Option[Path] = None
var ssh_control_path = ""
var thorough = false
var dry_run = false
var ssh_port = 0
var rev = ""
var verbose = false
val getopts = Getopts("""
Usage: isabelle hg_sync [OPTIONS] TARGET
Options are:
-F RULE add rsync filter RULE
(e.g. "protect /foo" to avoid deletion)
-P protect spaces in target file names: more robust, less portable
-R ROOT explicit repository root directory
(default: implicit from current directory)
-S PATH SSH control path for connection multiplexing
-T thorough treatment of file content and directory times
-n no changes: dry-run
-p PORT SSH port
-r REV explicit revision (default: state of working directory)
-v verbose
Synchronize Mercurial repository with TARGET directory,
which can be local or remote (using notation of rsync).
""",
"F:" -> (arg => filter = filter ::: List(arg)),
"P" -> (_ => protect_args = true),
"R:" -> (arg => root = Some(Path.explode(arg))),
"S:" -> (arg => ssh_control_path = arg),
"T" -> (_ => thorough = true),
"n" -> (_ => dry_run = true),
"p:" -> (arg => ssh_port = Value.Int.parse(arg)),
"r:" -> (arg => rev = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
val target =
more_args match {
case List(target) => target
case _ => getopts.usage()
}
val progress = new Console_Progress
val hg =
root match {
case Some(dir) => repository(dir)
case None => the_repository(Path.current)
}
val context = Rsync.Context(progress, ssh_port = ssh_port,
ssh_control_path = ssh_control_path, protect_args = protect_args)
hg.sync(context, target, verbose = verbose, thorough = thorough,
dry_run = dry_run, filter = filter, rev = rev)
}
)
}
diff --git a/src/Pure/System/components.scala b/src/Pure/System/components.scala
--- a/src/Pure/System/components.scala
+++ b/src/Pure/System/components.scala
@@ -1,371 +1,371 @@
/* Title: Pure/System/components.scala
Author: Makarius
Isabelle system components.
*/
package isabelle
import java.io.{File => JFile}
object Components {
/* archive name */
object Archive {
val suffix: String = ".tar.gz"
def apply(name: String): String =
if (name == "") error("Bad component name: " + quote(name))
else name + suffix
def unapply(archive: String): Option[String] = {
for {
name0 <- Library.try_unsuffix(suffix, archive)
name <- proper_string(name0)
} yield name
}
def get_name(archive: String): String =
unapply(archive) getOrElse
error("Bad component archive name (expecting .tar.gz): " + quote(archive))
}
/* component collections */
def default_component_repository: String =
Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
def admin(dir: Path): Path = dir + Path.explode("Admin/components")
def contrib(dir: Path = Path.current, name: String = ""): Path =
dir + Path.explode("contrib") + Path.explode(name)
def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = {
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+ Isabelle_System.extract(archive, dir)
name
}
def resolve(base_dir: Path, names: List[String],
target_dir: Option[Path] = None,
copy_dir: Option[Path] = None,
progress: Progress = new Progress
): Unit = {
Isabelle_System.make_directory(base_dir)
for (name <- names) {
val archive_name = Archive(name)
val archive = base_dir + Path.explode(archive_name)
if (!archive.is_file) {
val remote = Components.default_component_repository + "/" + archive_name
Isabelle_System.download_file(remote, archive, progress = progress)
}
for (dir <- copy_dir) {
Isabelle_System.make_directory(dir)
Isabelle_System.copy_file(archive, dir)
}
unpack(target_dir getOrElse base_dir, archive, progress = progress)
}
}
private val platforms_family: Map[Platform.Family.Value, Set[String]] =
Map(
Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"),
Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"),
Platform.Family.macos ->
Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"),
Platform.Family.windows ->
Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows"))
private val platforms_all: Set[String] =
Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2)
def purge(dir: Path, platform: Platform.Family.Value): Unit = {
val purge_set = platforms_all -- platforms_family(platform)
File.find_files(dir.file,
(file: JFile) => file.isDirectory && purge_set(file.getName),
include_dirs = true).foreach(Isabelle_System.rm_tree)
}
/* component directories */
def directories(): List[Path] =
Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS"))
/* component directory content */
object Directory {
def apply(path: Path): Directory = new Directory(path.absolute)
def create(path: Path, progress: Progress = new Progress): Directory = {
val component_dir = new Directory(path.absolute)
progress.echo("Creating component directory " + component_dir.path)
Isabelle_System.new_directory(component_dir.path)
Isabelle_System.make_directory(component_dir.etc)
component_dir
}
}
class Directory private(val path: Path) {
override def toString: String = path.toString
def etc: Path = path + Path.basic("etc")
def src: Path = path + Path.basic("src")
def lib: Path = path + Path.basic("lib")
def settings: Path = etc + Path.basic("settings")
def components: Path = etc + Path.basic("components")
def build_props: Path = etc + Path.basic("build.props")
def README: Path = path + Path.basic("README")
def LICENSE: Path = path + Path.basic("LICENSE")
def check: Boolean = settings.is_file || components.is_file
def read_components(): List[String] =
split_lines(File.read(components)).filter(_.nonEmpty)
def write_components(lines: List[String]): Unit =
File.write(components, terminate_lines(lines))
}
/* component repository content */
val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) {
override def toString: String = digest.shasum(name)
}
def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
(proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
Word.explode(line) match {
case Nil => None
case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name))
case _ => error("Bad components.sha1 entry: " + quote(line))
})
def write_components_sha1(entries: List[SHA1_Digest]): Unit =
File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n"))
/** manage user components **/
val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components")
def read_components(): List[String] =
if (components_path.is_file) Library.trim_split_lines(File.read(components_path))
else Nil
def write_components(lines: List[String]): Unit = {
Isabelle_System.make_directory(components_path.dir)
File.write(components_path, Library.terminate_lines(lines))
}
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
val path = path0.expand.absolute
if (!Directory(path).check && !Sessions.is_session_dir(path)) {
error("Bad component directory: " + path)
}
val lines1 = read_components()
val lines2 =
lines1.filter(line =>
line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path))
val lines3 = if (add) lines2 ::: List(path.implode) else lines2
if (lines1 != lines3) write_components(lines3)
val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed"
progress.echo(prefix + " component " + path)
}
/* main entry point */
def main(args: Array[String]): Unit = {
Command_Line.tool {
for (arg <- args) {
val add =
if (arg.startsWith("+")) true
else if (arg.startsWith("-")) false
else error("Bad argument: " + quote(arg))
val path = Path.explode(arg.substring(1))
update_components(add, path, progress = new Console_Progress)
}
}
}
/** build and publish components **/
def build_components(
options: Options,
components: List[Path],
progress: Progress = new Progress,
publish: Boolean = false,
force: Boolean = false,
update_components_sha1: Boolean = false
): Unit = {
val archives: List[Path] =
for (path <- components) yield {
path.file_name match {
case Archive(_) => path
case name =>
if (!path.is_dir) error("Bad component directory: " + path)
else if (!Directory(path).check) {
error("Malformed component directory: " + path +
"\n (requires etc/settings or etc/components)")
}
else {
val component_path = path.expand
val archive_dir = component_path.dir
val archive_name = Archive(name)
val archive = archive_dir + Path.explode(archive_name)
if (archive.is_file && !force) {
error("Component archive already exists: " + archive)
}
progress.echo("Packaging " + archive_name)
Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
dir = archive_dir).check
archive
}
}
}
if ((publish && archives.nonEmpty) || update_components_sha1) {
val server = options.string("isabelle_components_server")
if (server.isEmpty) error("Undefined option isabelle_components_server")
using(SSH.open_session(options, server)) { ssh =>
val components_dir = Path.explode(options.string("isabelle_components_dir"))
val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
error("Bad remote directory: " + dir)
}
if (publish) {
for (archive <- archives) {
val archive_name = archive.file_name
val name = Archive.get_name(archive_name)
val remote_component = components_dir + archive.base
val remote_contrib = contrib_dir + Path.explode(name)
// component archive
if (ssh.is_file(remote_component) && !force) {
error("Remote component archive already exists: " + remote_component)
}
progress.echo("Uploading " + archive_name)
ssh.write_file(remote_component, archive)
// contrib directory
val is_standard_component =
Isabelle_System.with_tmp_dir("component") { tmp_dir =>
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
+ Isabelle_System.extract(archive, tmp_dir)
Directory(tmp_dir + Path.explode(name)).check
}
if (is_standard_component) {
if (ssh.is_dir(remote_contrib)) {
if (force) ssh.rm_tree(remote_contrib)
else error("Remote component directory already exists: " + remote_contrib)
}
progress.echo("Unpacking remote " + archive_name)
ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " +
ssh.bash_path(remote_component)).check
}
else {
progress.echo_warning("No unpacking of non-standard component: " + archive_name)
}
}
}
// remote SHA1 digests
if (update_components_sha1) {
val lines =
for {
entry <- ssh.read_dir(components_dir)
if ssh.is_file(components_dir + Path.basic(entry)) &&
entry.endsWith(Archive.suffix)
}
yield {
progress.echo("Digesting remote " + entry)
ssh.execute("cd " + ssh.bash_path(components_dir) +
"; sha1sum " + Bash.string(entry)).check.out
}
write_components_sha1(read_components_sha1(lines))
}
}
}
// local SHA1 digests
{
val new_entries =
for (archive <- archives)
yield {
val name = archive.file_name
progress.echo("Digesting local " + name)
SHA1_Digest(SHA1.digest(archive), name)
}
val new_names = new_entries.map(_.name).toSet
write_components_sha1(
new_entries :::
read_components_sha1().filterNot(entry => new_names.contains(entry.name)))
}
}
/* Isabelle tool wrapper */
private val relevant_options =
List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir")
val isabelle_tool =
Isabelle_Tool("build_components", "build and publish Isabelle components",
Scala_Project.here,
{ args =>
var publish = false
var update_components_sha1 = false
var force = false
var options = Options.init()
def show_options: String =
cat_lines(relevant_options.flatMap(options.get).map(_.print))
val getopts = Getopts("""
Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
Options are:
-P publish on SSH server (see options below)
-f force: overwrite existing component archives and directories
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-u update all SHA1 keys in Isabelle repository Admin/components
Build and publish Isabelle components as .tar.gz archives on SSH server,
depending on system options:
""" + Library.indent_lines(2, show_options) + "\n",
"P" -> (_ => publish = true),
"f" -> (_ => force = true),
"o:" -> (arg => options = options + arg),
"u" -> (_ => update_components_sha1 = true))
val more_args = getopts(args)
if (more_args.isEmpty && !update_components_sha1) getopts.usage()
val progress = new Console_Progress
build_components(options, more_args.map(Path.explode), progress = progress,
publish = publish, force = force, update_components_sha1 = update_components_sha1)
})
}
diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala
+++ b/src/Pure/System/isabelle_system.scala
@@ -1,526 +1,528 @@
/* Title: Pure/System/isabelle_system.scala
Author: Makarius
Miscellaneous Isabelle system operations.
*/
package isabelle
import java.util.{Map => JMap, HashMap}
import java.io.{File => JFile, IOException}
import java.net.ServerSocket
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
object Isabelle_System {
/* settings environment */
def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = {
val env0 = isabelle.setup.Environment.settings()
if (putenv.isEmpty) env0
else {
val env = new HashMap(env0)
for ((a, b) <- putenv) env.put(a, b)
env
}
}
def getenv(name: String, env: JMap[String, String] = settings()): String =
Option(env.get(name)).getOrElse("")
def getenv_strict(name: String, env: JMap[String, String] = settings()): String =
proper_string(getenv(name, env)) getOrElse
error("Undefined Isabelle environment variable: " + quote(name))
/* services */
type Service = Classpath.Service
@volatile private var _classpath: Option[Classpath] = None
def classpath(): Classpath = {
if (_classpath.isEmpty) init() // unsynchronized check
_classpath.get
}
def make_services[C](c: Class[C]): List[C] = classpath().make_services(c)
/* init settings + classpath */
def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = {
isabelle.setup.Environment.init(isabelle_root, cygwin_root)
synchronized {
if (_classpath.isEmpty) _classpath = Some(Classpath())
}
}
/* getetc -- static distribution parameters */
def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = {
val path = root + Path.basic("etc") + Path.basic(name)
if (path.is_file) {
Library.trim_split_lines(File.read(path)) match {
case Nil => None
case List(s) => Some(s)
case _ => error("Single line expected in " + path.absolute)
}
}
else None
}
/* Isabelle distribution identification */
def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
getetc("ISABELLE_ID", root = root) orElse
Mercurial.archive_id(root) orElse
Mercurial.id_repository(root, rev = "") getOrElse
error("Failed to identify Isabelle distribution " + root.expand)
object Isabelle_Id extends Scala.Fun_String("isabelle_id") {
val here = Scala_Project.here
def apply(arg: String): String = isabelle_id()
}
def isabelle_tags(root: Path = Path.ISABELLE_HOME): String =
getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse {
if (Mercurial.is_repository(root)) {
val hg = Mercurial.repository(root)
hg.tags(rev = hg.parent())
}
else ""
}
def export_isabelle_identifier(isabelle_identifier: String): String =
"export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER"))
def isabelle_heading(): String =
isabelle_identifier() match {
case None => ""
case Some(version) => " (" + version + ")"
}
def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
def identification(): String =
"Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading()
/** file-system operations **/
/* scala functions */
private def apply_paths(
args: List[String],
fun: PartialFunction[List[Path], Unit]
): List[String] = {
fun(args.map(Path.explode))
Nil
}
private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
apply_paths(args, { case List(path) => fun(path) })
private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
/* permissions */
def chmod(arg: String, path: Path): Unit =
bash("chmod " + arg + " " + File.bash_path(path)).check
def chown(arg: String, path: Path): Unit =
bash("chown " + arg + " " + File.bash_path(path)).check
/* directories */
def make_directory(path: Path): Path = {
if (!path.is_dir) {
try { Files.createDirectories(path.java_path) }
catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
}
path
}
def new_directory(path: Path): Path =
if (path.is_dir) error("Directory already exists: " + path.absolute)
else make_directory(path)
def copy_dir(dir1: Path, dir2: Path): Unit = {
val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2))
if (!res.ok) {
cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err)
}
}
def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = {
if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute)
else {
try { copy_dir(dir1, dir2); body }
finally { rm_tree(dir2 ) }
}
}
object Make_Directory extends Scala.Fun_Strings("make_directory") {
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths1(args, make_directory)
}
object Copy_Dir extends Scala.Fun_Strings("copy_dir") {
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir)
}
/* copy files */
def copy_file(src: JFile, dst: JFile): Unit = {
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
if (!File.eq(src, target)) {
try {
Files.copy(src.toPath, target.toPath,
StandardCopyOption.COPY_ATTRIBUTES,
StandardCopyOption.REPLACE_EXISTING)
}
catch {
case ERROR(msg) =>
cat_error("Failed to copy file " +
File.path(src).absolute + " to " + File.path(dst).absolute, msg)
}
}
}
def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file)
def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = {
val src1 = src.expand
val src1_dir = src1.dir
if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory")
copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir))
}
object Copy_File extends Scala.Fun_Strings("copy_file") {
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths2(args, copy_file)
}
object Copy_File_Base extends Scala.Fun_Strings("copy_file_base") {
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base)
}
/* move files */
def move_file(src: JFile, dst: JFile): Unit = {
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
if (!File.eq(src, target))
Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
}
def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file)
/* symbolic link */
def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit = {
val src_file = src.file
val dst_file = dst.file
val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
if (force) target.delete
def cygwin_link(): Unit = {
if (native) {
error("Failed to create native symlink on Windows: " + quote(src_file.toString) +
"\n(but it could work as Administrator)")
}
else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target)
}
try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
catch {
case _: UnsupportedOperationException if Platform.is_windows => cygwin_link()
case _: FileSystemException if Platform.is_windows => cygwin_link()
}
}
/* tmp files */
def isabelle_tmp_prefix(): JFile = {
val path = Path.explode("$ISABELLE_TMP_PREFIX")
path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment
File.platform_file(path)
}
def tmp_file(
name: String,
ext: String = "",
base_dir: JFile = isabelle_tmp_prefix(),
initialized: Boolean = true
): JFile = {
val suffix = if (ext == "") "" else "." + ext
val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
if (initialized) file.deleteOnExit() else file.delete()
file
}
def with_tmp_file[A](
name: String,
ext: String = "",
base_dir: JFile = isabelle_tmp_prefix()
)(body: Path => A): A = {
val file = tmp_file(name, ext, base_dir = base_dir)
try { body(File.path(file)) } finally { file.delete }
}
/* tmp dirs */
def rm_tree(root: JFile): Unit = {
root.delete
if (root.isDirectory) {
Files.walkFileTree(root.toPath,
new SimpleFileVisitor[JPath] {
override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = {
try { Files.deleteIfExists(file) }
catch { case _: IOException => }
FileVisitResult.CONTINUE
}
override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = {
if (e == null) {
try { Files.deleteIfExists(dir) }
catch { case _: IOException => }
FileVisitResult.CONTINUE
}
else throw e
}
}
)
}
}
def rm_tree(root: Path): Unit = rm_tree(root.file)
object Rm_Tree extends Scala.Fun_Strings("rm_tree") {
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree)
}
def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = {
val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
dir.deleteOnExit()
dir
}
def with_tmp_dir[A](
name: String,
base_dir: JFile = isabelle_tmp_prefix()
)(body: Path => A): A = {
val dir = tmp_dir(name, base_dir = base_dir)
try { body(File.path(dir)) } finally { rm_tree(dir) }
}
/* quasi-atomic update of directory */
def update_directory(dir: Path, f: Path => Unit): Unit = {
val new_dir = dir.ext("new")
val old_dir = dir.ext("old")
rm_tree(new_dir)
rm_tree(old_dir)
f(new_dir)
if (dir.is_dir) move_file(dir, old_dir)
move_file(new_dir, dir)
rm_tree(old_dir)
}
/* TCP/IP ports */
def local_port(): Int = {
val socket = new ServerSocket(0)
val port = socket.getLocalPort
socket.close()
port
}
/* JVM shutdown hook */
def create_shutdown_hook(body: => Unit): Thread = {
val shutdown_hook = Isabelle_Thread.create(new Runnable { def run: Unit = body })
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
shutdown_hook
}
def remove_shutdown_hook(shutdown_hook: Thread): Unit =
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
/** external processes **/
/* GNU bash */
def bash(script: String,
description: String = "",
cwd: JFile = null,
env: JMap[String, String] = settings(),
redirect: Boolean = false,
input: String = "",
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
watchdog: Option[Bash.Watchdog] = None,
strict: Boolean = true,
cleanup: () => Unit = () => ()
): Process_Result = {
Bash.process(script,
description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr,
watchdog = watchdog, strict = strict)
}
/* command-line tools */
def require_command(cmd: String, test: String = "--version"): Unit = {
if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd))
}
private lazy val gnutar_check: Boolean =
try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
catch { case ERROR(_) => false }
def gnutar(
args: String,
dir: Path = Path.current,
original_owner: Boolean = false,
- strip: Int = 0,
+ strip: Boolean = false,
redirect: Boolean = false
): Process_Result = {
val options =
(if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
(if (original_owner) "" else "--owner=root --group=staff ") +
- (if (strip <= 0) "" else "--strip-components=" + strip + " ")
+ (if (!strip) "" else "--strip-components=1 ")
if (gnutar_check) bash("tar " + options + args, redirect = redirect)
else error("Expected to find GNU tar executable")
}
- def extract(archive: Path, dir: Path): Unit = {
+ def extract(archive: Path, dir: Path, strip: Boolean = false): Unit = {
val name = archive.file_name
if (File.is_zip(name)) {
+ require(!strip, "Cannot use unzip with strip")
Isabelle_System.bash("unzip -x " + File.bash_path(archive.absolute), cwd = dir.file).check
}
- else if (File.is_tar_gz(name)) {
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+ else if (File.is_tar_bz2(name) || File.is_tgz(name) || File.is_tar_gz(name)) {
+ val flags = if (File.is_tar_bz2(name)) "-xjf " else "-xzf "
+ Isabelle_System.gnutar(flags + File.bash_path(archive), dir = dir, strip = strip).check
}
else error("Cannot extract " + archive)
}
def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
with_tmp_file("patch") { patch =>
Isabelle_System.bash(
"diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) +
" > " + File.bash_path(patch),
cwd = base_dir.file).check_rc(_ <= 1)
File.read(patch)
}
}
def hostname(): String = bash("hostname -s").check.out
def open(arg: String): Unit =
bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
def pdf_viewer(arg: Path): Unit =
bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
def open_external_file(name: String): Boolean = {
val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
val external =
ext.nonEmpty &&
Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
if (external) {
if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
else open(name)
}
external
}
/** Isabelle resources **/
/* repository clone with Admin */
def admin(): Boolean = Path.explode("~~/Admin").is_dir
/* default logic */
def default_logic(args: String*): String = {
args.find(_ != "") match {
case Some(logic) => logic
case None => getenv_strict("ISABELLE_LOGIC")
}
}
/* download file */
def download(url_name: String, progress: Progress = new Progress): HTTP.Content = {
val url = Url(url_name)
progress.echo("Getting " + quote(url_name))
try { HTTP.Client.get(url) }
catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
}
def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
Bytes.write(file, download(url_name, progress = progress).bytes)
object Download extends Scala.Fun("download", thread = true) {
val here = Scala_Project.here
override def invoke(args: List[Bytes]): List[Bytes] =
args.map(url => download(url.text).bytes)
}
/* repositories */
val isabelle_repository: Mercurial.Server =
Mercurial.Server("https://isabelle.sketis.net/repos/isabelle")
val afp_repository: Mercurial.Server =
Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel")
def official_releases(): List[String] =
Library.trim_split_lines(
isabelle_repository.read_file(Path.explode("Admin/Release/official")))
}
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
+ Isabelle_System.extract(archive, 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)
}
}
}