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,546 +1,546 @@
/* 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_dir: 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")
Isabelle_System.require_command("unzip", test = "-h")
Isabelle_System.new_directory(component_dir)
val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
/* jEdit directory */
val jedit = "jedit" + version
val jedit_patched = jedit + "-patched"
val jedit_dir = Isabelle_System.make_directory(component_dir + Path.basic(jedit))
val jedit_patched_dir = component_dir + 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("tmp") { tmp_dir =>
+ 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
/* 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).iterator
name = file.getName
if !name.endsWith("~") && !name.endsWith(".orig")
} {
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.getName.endsWith(".java"))
package_name <- Scala_Project.package_name(File.path(file))
if !exclude_package(package_name)
} yield File.path(component_dir.java_path.relativize(file.toPath).toFile).implode
File.write(etc_dir + Path.explode("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.bash("unzip -x " + File.bash_path(zip_path), cwd = jars_dir.file).check
}
}
/* 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_dir + Path.basic(jedit).patch,
Isabelle_System.make_patch(component_dir, Path.basic(jedit), Path.basic(jedit_patched)))
if (!original) Isabelle_System.rm_tree(jedit_dir)
/* settings */
File.write(etc_dir + Path.explode("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 + Path.basic("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_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,936 +1,936 @@
/* 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): Unit =
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("tmp")(dir =>
+ 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)
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.components(dir),
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.read_components(dir) } 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))
Components.write_components(dir,
Components.read_components(dir).flatMap(line =>
line match {
case Bundled(name) =>
if (Components.check_dir(Components.contrib(dir, name))) 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
): Unit = {
val server_option = "build_host_" + platform.toString
val ssh =
options.string(server_option) match {
case "" =>
if (Platform.family == platform) SSH.Local
else error("Undefined option " + server_option + ": cannot build heaps")
case SSH.Target(user, host) =>
SSH.open_session(options, host = host, user = user)
case s => error("Malformed option " + server_option + ": " + quote(s))
}
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 remote_commands =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
"bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
"tar -cf tmp.tar heaps")
ssh.execute(remote_commands.mkString(" && "), settings = false).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
}
execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
}
}
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.repository(Path.ISABELLE_HOME)
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) {
progress.echo("Building heaps " + commas_quote(build_sessions) + " ...")
build_heaps(options, platform, build_sessions, isabelle_target)
}
// 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_sqlite.scala b/src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala
+++ b/src/Pure/Admin/build_sqlite.scala
@@ -1,113 +1,113 @@
/* Title: Pure/Admin/build_sqlite.scala
Author: Makarius
Build Isabelle sqlite-jdbc component from official download.
*/
package isabelle
object Build_SQLite {
/* build sqlite */
def build_sqlite(
download_url: String,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
val Download_Name = """^.*/([^/]+)\.jar""".r
val download_name =
download_url match {
case Download_Name(download_name) => download_name
case _ => error("Malformed jar download URL: " + quote(download_url))
}
/* component */
val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(download_name))
progress.echo("Component " + component_dir)
/* README */
File.write(component_dir + Path.basic("README"),
"This is " + download_name + " from\n" + download_url +
"\n\n Makarius\n " + Date.Format.date(Date.now()) + "\n")
/* settings */
val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
File.write(etc_dir + Path.basic("settings"),
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_SQLITE_HOME="$COMPONENT"
classpath "$ISABELLE_SQLITE_HOME/""" + download_name + """.jar"
""")
/* jar */
val jar = component_dir + Path.basic(download_name).ext("jar")
Isabelle_System.download_file(download_url, jar, progress = progress)
- Isabelle_System.with_tmp_dir("sqlite") { jar_dir =>
+ Isabelle_System.with_tmp_dir("build") { jar_dir =>
progress.echo("Unpacking " + jar)
Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute),
cwd = jar_dir.file).check
val jar_files =
List(
"META-INF/maven/org.xerial/sqlite-jdbc/LICENSE" -> ".",
"META-INF/maven/org.xerial/sqlite-jdbc/LICENSE.zentus" -> ".",
"org/sqlite/native/Linux/aarch64/libsqlitejdbc.so" -> "arm64-linux",
"org/sqlite/native/Linux/x86_64/libsqlitejdbc.so" -> "x86_64-linux",
"org/sqlite/native/Mac/aarch64/libsqlitejdbc.jnilib" -> "arm64-darwin",
"org/sqlite/native/Mac/x86_64/libsqlitejdbc.jnilib" -> "x86_64-darwin",
"org/sqlite/native/Windows/x86_64/sqlitejdbc.dll" -> "x86_64-windows")
for ((file, dir) <- jar_files) {
val target = Isabelle_System.make_directory(component_dir + Path.explode(dir))
Isabelle_System.copy_file(jar_dir + Path.explode(file), target)
}
File.set_executable(component_dir + Path.explode("x86_64-windows/sqlitejdbc.dll"), true)
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_sqlite", "build Isabelle sqlite-jdbc component from official download",
Scala_Project.here,
{ args =>
var target_dir = Path.current
val getopts = Getopts("""
Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD
Options are:
-D DIR target directory (default ".")
Build sqlite-jdbc component from the specified download URL (JAR), see also
https://github.com/xerial/sqlite-jdbc and
https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
""",
"D:" -> (arg => target_dir = Path.explode(arg)))
val more_args = getopts(args)
val download_url =
more_args match {
case List(download_url) => download_url
case _ => getopts.usage()
}
val progress = new Console_Progress()
build_sqlite(download_url, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/sync_repos.scala b/src/Pure/Admin/sync_repos.scala
--- a/src/Pure/Admin/sync_repos.scala
+++ b/src/Pure/Admin/sync_repos.scala
@@ -1,100 +1,100 @@
/* Title: Pure/Admin/sync_repos.scala
Author: Makarius
Synchronize Isabelle + AFP repositories.
*/
package isabelle
object Sync_Repos {
def sync_repos(target: String,
progress: Progress = new Progress,
verbose: Boolean = false,
thorough: Boolean = false,
dry_run: Boolean = false,
clean: Boolean = false,
rev: String = "",
afp_root: Option[Path] = None,
afp_rev: String = ""
): Unit = {
val target_dir = if (target.endsWith(":") || target.endsWith("/")) target else target + "/"
val isabelle_hg = Mercurial.repository(Path.ISABELLE_HOME)
val afp_hg = afp_root.map(Mercurial.repository(_))
def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit =
hg.sync(dest, rev = r, progress = progress, verbose = verbose, thorough = thorough,
dry_run = dry_run, clean = clean, filter = filter)
progress.echo("\n* Isabelle repository:")
sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID"))
if (!dry_run) {
- Isabelle_System.with_tmp_dir("sync_repos") { tmp_dir =>
+ Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
val id_path = tmp_dir + Path.explode("ISABELLE_ID")
File.write(id_path, isabelle_hg.id(rev = rev))
Isabelle_System.rsync(thorough = thorough,
args = List(File.standard_path(id_path), target_dir + "etc/"))
}
}
for (hg <- afp_hg) {
progress.echo("\n* AFP repository:")
sync(hg, target_dir + "AFP", afp_rev)
}
}
val isabelle_tool =
Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories",
Scala_Project.here, { args =>
var afp_root: Option[Path] = None
var clean = false
var thorough = false
var afp_rev = ""
var dry_run = false
var rev = ""
var verbose = false
val getopts = Getopts("""
Usage: isabelle sync_repos [OPTIONS] TARGET
Options are:
-A ROOT include AFP with given root directory
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
-T thorough check of file content (default: time and size)
-a REV explicit AFP revision (default: state of working directory)
-f force changes: no dry-run
-n no changes: dry-run
-r REV explicit revision (default: state of working directory)
-v verbose
Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
Example (without -f as "dry-run"):
isabelle sync_repos -A '$AFP_BASE' -C testmachine:test/isabelle_afp
""",
"A:" -> (arg => afp_root = Some(Path.explode(arg))),
"C" -> { _ => clean = true; dry_run = true },
"T" -> (_ => thorough = true),
"a:" -> (arg => afp_rev = arg),
"f" -> (_ => dry_run = false),
"n" -> (_ => dry_run = true),
"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
sync_repos(target, progress = progress, verbose = verbose, thorough = thorough,
dry_run = dry_run, clean = clean, rev = rev, afp_root = afp_root, afp_rev = afp_rev)
}
)
}
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,540 +1,540 @@
/* 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
}
}
}
/** 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(" "))
/* 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 repository(root: Path, ssh: SSH.System = SSH.Local): Repository = {
val hg = new Repository(root, ssh)
hg.command("root").check
hg
}
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 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(target: String,
progress: Progress = new Progress,
verbose: Boolean = false,
thorough: Boolean = false,
dry_run: Boolean = false,
clean: Boolean = false,
filter: List[String] = Nil,
rev: String = ""
): Unit = {
require(ssh == SSH.Local, "local repository required")
- Isabelle_System.with_tmp_dir("rsync") { tmp_dir =>
+ Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
val (options, source) =
if (rev.isEmpty) {
val exclude_path = tmp_dir + Path.explode("exclude")
val exclude = status(options = "--unknown --ignored --no-status")
File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
val options = List("--exclude-from=" + exclude_path.implode)
val source = File.standard_path(root)
(options, source)
}
else {
val source = File.standard_path(tmp_dir + Path.explode("archive"))
archive(source, rev = rev)
(Nil, source)
}
Isabelle_System.rsync(
progress = progress, verbose = verbose, thorough = thorough,
dry_run = dry_run, clean = clean, filter = filter,
args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target))
}
}
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 =
remote match {
case _ 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
case SSH.Target(user, host) =>
val phabricator = Phabricator.API(user, host)
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
case _ => error("Malformed remote specification " + quote(remote))
}
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 clean = false
var filter: List[String] = Nil
var root: Option[Path] = None
var thorough = false
var dry_run = false
var rev = ""
var verbose = false
val getopts = Getopts("""
Usage: isabelle hg_sync [OPTIONS] TARGET
Options are:
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
-F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion)
-R ROOT explicit repository root directory
(default: implicit from current directory)
-T thorough check of file content (default: time and size)
-f force changes: no dry-run
-n no changes: dry-run
-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).
""",
"C" -> { _ => clean = true; dry_run = true },
"F:" -> (arg => filter = filter ::: List(arg)),
"R:" -> (arg => root = Some(Path.explode(arg))),
"T" -> (_ => thorough = true),
"f" -> (_ => dry_run = false),
"n" -> (_ => dry_run = true),
"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)
}
hg.sync(target, progress = progress, verbose = verbose, thorough = thorough,
dry_run = dry_run, clean = clean, filter = filter, rev = rev)
}
)
}