diff --git a/src/Pure/Admin/build_easychair.scala b/src/Pure/Admin/build_easychair.scala
--- a/src/Pure/Admin/build_easychair.scala
+++ b/src/Pure/Admin/build_easychair.scala
@@ -1,102 +1,99 @@
/* Title: Pure/Admin/build_easychair.scala
Author: Makarius
Build Isabelle component for Easychair LaTeX style.
See also https://easychair.org/publications/for_authors
*/
package isabelle
object Build_Easychair {
/* build easychair component */
val default_url = "https://easychair.org/publications/easychair.zip"
def build_easychair(
download_url: String = default_url,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
- cwd = download_dir.file).check
+ Isabelle_System.extract(download_file, download_dir)
val easychair_dir = File.get_dir(download_dir, title = download_url)
/* component */
val version =
Library.try_unprefix("EasyChair", easychair_dir.file_name)
.getOrElse("Failed to detect version from " + quote(easychair_dir.file_name))
val component = "easychair-" + version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component), progress = progress)
Isabelle_System.rm_tree(component_dir.path)
Isabelle_System.copy_dir(easychair_dir, component_dir.path)
Isabelle_System.make_directory(component_dir.etc)
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_EASYCHAIR_HOME="$COMPONENT"
""")
/* README */
File.write(component_dir.README,
"""This is the Easychair style for authors from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_easychair", "build component for Easychair LaTeX style",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_url
val getopts = Getopts("""
Usage: isabelle build_easychair [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
Build component for Easychair LaTeX style.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_easychair(download_url = download_url, target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_eptcs.scala b/src/Pure/Admin/build_eptcs.scala
--- a/src/Pure/Admin/build_eptcs.scala
+++ b/src/Pure/Admin/build_eptcs.scala
@@ -1,100 +1,96 @@
/* Title: Pure/Admin/build_eptcs.scala
Author: Makarius
Build Isabelle component for EPTCS LaTeX style.
See also:
- http://style.eptcs.org
- https://github.com/EPTCS/style/releases
*/
package isabelle
object Build_EPTCS {
/* build eptcs component */
val default_url = "https://github.com/EPTCS/style/releases/download"
val default_version = "1.7.0"
def build_eptcs(
base_url: String = default_url,
version: String = default_version,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
-
/* component */
val component = "eptcs-" + version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component), progress = progress)
/* download */
val download_url = base_url + "/v" + version + "/eptcsstyle.zip"
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(download_file, component_dir.path)
}
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_EPTCS_HOME="$COMPONENT"
""")
/* README */
File.write(component_dir.README,
"""This is the EPTCS style from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_eptcs", "build component for EPTCS LaTeX style",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var base_url = default_url
var version = default_version
val getopts = Getopts("""
Usage: isabelle build_eptcs [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
-V VERSION version (default: """" + default_version + """")
Build component for EPTCS LaTeX style.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => base_url = arg),
"V:" -> (arg => version = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_eptcs(base_url = base_url, version = version, target_dir = target_dir,
progress = progress)
})
}
diff --git a/src/Pure/Admin/build_foiltex.scala b/src/Pure/Admin/build_foiltex.scala
--- a/src/Pure/Admin/build_foiltex.scala
+++ b/src/Pure/Admin/build_foiltex.scala
@@ -1,111 +1,108 @@
/* Title: Pure/Admin/build_foiltex.scala
Author: Makarius
Build Isabelle component for FoilTeX.
See also https://ctan.org/pkg/foiltex
*/
package isabelle
object Build_Foiltex {
/* build FoilTeX component */
val default_url = "https://mirrors.ctan.org/macros/latex/contrib/foiltex.zip"
def build_foiltex(
download_url: String = default_url,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
- cwd = download_dir.file).check
+ Isabelle_System.extract(download_file, download_dir)
val foiltex_dir = File.get_dir(download_dir, title = download_url)
val README = Path.explode("README")
val README_flt = Path.explode("README.flt")
Isabelle_System.move_file(foiltex_dir + README, foiltex_dir + README_flt)
Isabelle_System.bash("pdflatex foiltex.ins", cwd = foiltex_dir.file).check
/* component */
val version = {
val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r
split_lines(File.read(foiltex_dir + README_flt))
.collectFirst({ case Version(v) => v })
.getOrElse(error("Failed to detect version in " + README_flt))
}
val component = "foiltex-" + version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component), progress = progress)
Isabelle_System.rm_tree(component_dir.path)
Isabelle_System.copy_dir(foiltex_dir, component_dir.path)
Isabelle_System.make_directory(component_dir.etc)
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_FOILTEX_HOME="$COMPONENT"
""")
/* README */
File.write(component_dir.README,
"""This is FoilTeX from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_foiltex", "build component for FoilTeX",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_url
val getopts = Getopts("""
Usage: isabelle build_foiltex [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
Build component for FoilTeX: slides in LaTeX.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_foiltex(download_url = download_url, target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_jdk.scala b/src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala
+++ b/src/Pure/Admin/build_jdk.scala
@@ -1,229 +1,223 @@
/* Title: Pure/Admin/build_jdk.scala
Author: Makarius
Build Isabelle jdk component from original platform installations.
*/
package isabelle
import java.io.{File => JFile}
import java.nio.file.Files
import java.nio.file.attribute.PosixFilePermission
import scala.util.matching.Regex
object Build_JDK {
/* platform and version information */
sealed case class JDK_Platform(
platform_name: String,
platform_regex: Regex,
exe: String = "java",
macos_home: Boolean = false,
jdk_version: String = ""
) {
override def toString: String = platform_name
def platform_path: Path = Path.explode(platform_name)
def detect(jdk_dir: Path): Option[JDK_Platform] = {
val major_version = {
val Major_Version = """.*jdk(\d+).*$""".r
val jdk_name = jdk_dir.file.getName
jdk_name match {
case Major_Version(s) => s
case _ => error("Cannot determine major version from " + quote(jdk_name))
}
}
val path = jdk_dir + Path.explode("bin") + Path.explode(exe)
if (path.is_file) {
val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out
if (platform_regex.matches(file_descr)) {
val Version = ("^(" + major_version + """[0-9.+]+)(?:-LTS)?$""").r
val version_lines =
Isabelle_System.bash("strings " + File.bash_path(path)).check
.out_lines.flatMap({ case Version(s) => Some(s) case _ => None })
version_lines match {
case List(jdk_version) => Some(copy(jdk_version = jdk_version))
case _ => error("Expected unique version within executable " + path)
}
}
else None
}
else None
}
}
val templates: List[JDK_Platform] =
List(
JDK_Platform("arm64-darwin", """.*Mach-O 64-bit.*arm64.*""".r, macos_home = true),
JDK_Platform("arm64-linux", """.*ELF 64-bit.*ARM aarch64.*""".r),
JDK_Platform("x86_64-darwin", """.*Mach-O 64-bit.*x86[-_]64.*""".r, macos_home = true),
JDK_Platform("x86_64-linux", """.*ELF 64-bit.*x86[-_]64.*""".r),
JDK_Platform("x86_64-windows", """.*PE32\+ executable.*x86[-_]64.*""".r, exe = "java.exe"))
/* README */
def readme(jdk_version: String): String =
"""This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also
https://www.azul.com/downloads/zulu-community/?package=jdk
The main license is GPL2, but some modules are covered by other (more liberal)
licenses, see legal/* for details.
Linux, Windows, macOS all work uniformly, depending on platform-specific
subdirectories.
"""
/* settings */
val settings: String =
"""# -*- shell-script -*- :mode=shellscript:
case "$ISABELLE_PLATFORM_FAMILY" in
linux)
ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
windows)
ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64"
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
macos)
if [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$COMPONENT/$ISABELLE_APPLE_PLATFORM64" ]
then
ISABELLE_JAVA_PLATFORM="$ISABELLE_APPLE_PLATFORM64"
else
ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
fi
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
esac
"""
/* extract archive */
def extract_archive(dir: Path, archive: Path): JDK_Platform = {
try {
val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp"))
- if (archive.get_ext == "zip") {
- Isabelle_System.bash(
- "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check
- }
- else {
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
- }
+ Isabelle_System.extract(archive, tmp_dir)
val jdk_dir = File.get_dir(tmp_dir, title = archive.file_name)
val platform =
templates.view.flatMap(_.detect(jdk_dir))
.headOption.getOrElse(error("Failed to detect JDK platform"))
val platform_dir = dir + platform.platform_path
if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
Isabelle_System.move_file(jdk_dir, platform_dir)
platform
}
catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) }
}
/* build jdk */
def build_jdk(
archives: List[Path],
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
if (Platform.is_windows) error("Cannot build jdk on Windows")
Isabelle_System.with_tmp_dir("jdk") { dir =>
progress.echo("Extracting ...")
val platforms = archives.map(extract_archive(dir, _))
val jdk_version =
platforms.map(_.jdk_version).distinct match {
case List(version) => version
case Nil => error("No archives")
case versions =>
error("Archives contain multiple JDK versions: " + commas_quote(versions))
}
templates.filterNot(p1 => platforms.exists(p2 => p1.platform_name == p2.platform_name))
match {
case Nil =>
case missing => error("Missing platforms: " + commas_quote(missing.map(_.platform_name)))
}
val jdk_name = "jdk-" + jdk_version
val jdk_path = Path.explode(jdk_name)
val component_dir = Components.Directory.create(dir + jdk_path, progress = progress)
File.write(component_dir.settings, settings)
File.write(component_dir.README, readme(jdk_version))
for (platform <- platforms) {
Isabelle_System.move_file(dir + platform.platform_path, component_dir.path)
}
for (file <- File.find_files(component_dir.path.file, include_dirs = true)) {
val path = file.toPath
val perms = Files.getPosixFilePermissions(path)
perms.add(PosixFilePermission.OWNER_READ)
perms.add(PosixFilePermission.GROUP_READ)
perms.add(PosixFilePermission.OTHERS_READ)
perms.add(PosixFilePermission.OWNER_WRITE)
if (file.isDirectory) {
perms.add(PosixFilePermission.OWNER_WRITE)
perms.add(PosixFilePermission.OWNER_EXECUTE)
perms.add(PosixFilePermission.GROUP_EXECUTE)
perms.add(PosixFilePermission.OTHERS_EXECUTE)
}
Files.setPosixFilePermissions(path, perms)
}
progress.echo("Archiving ...")
Isabelle_System.gnutar(
"-czf " + File.bash_path(target_dir + jdk_path.tar.gz) + " " + jdk_name, dir = dir).check
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives",
Scala_Project.here,
{ args =>
var target_dir = Path.current
val getopts = Getopts("""
Usage: isabelle build_jdk [OPTIONS] ARCHIVES...
Options are:
-D DIR target directory (default ".")
Build jdk component from tar.gz archives, with original jdk archives
for Linux, Windows, and macOS.
""",
"D:" -> (arg => target_dir = Path.explode(arg)))
val more_args = getopts(args)
if (more_args.isEmpty) getopts.usage()
val archives = more_args.map(Path.explode)
val progress = new Console_Progress()
build_jdk(archives = archives, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_jedit.scala b/src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala
+++ b/src/Pure/Admin/build_jedit.scala
@@ -1,544 +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")
- Isabelle_System.require_command("unzip", test = "-h")
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
/* 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.bash("unzip -x " + File.bash_path(zip_path), cwd = jars_dir.file).check
+ 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_llncs.scala b/src/Pure/Admin/build_llncs.scala
--- a/src/Pure/Admin/build_llncs.scala
+++ b/src/Pure/Admin/build_llncs.scala
@@ -1,111 +1,108 @@
/* Title: Pure/Admin/build_llncs.scala
Author: Makarius
Build Isabelle component for Springer LaTeX LNCS style.
See also:
- https://ctan.org/pkg/llncs?lang=en
- https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines
*/
package isabelle
object Build_LLNCS {
/* build llncs component */
val default_url = "https://mirrors.ctan.org/macros/latex/contrib/llncs.zip"
def build_llncs(
download_url: String = default_url,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
- cwd = download_dir.file).check
+ Isabelle_System.extract(download_file, download_dir)
val llncs_dir = File.get_dir(download_dir, title = download_url)
val readme = Path.explode("README.md")
File.change(llncs_dir + readme)(_.replace(" ", "\u00a0"))
/* component */
val version = {
val Version = """^_.* v(.*)_$""".r
split_lines(File.read(llncs_dir + readme))
.collectFirst({ case Version(v) => v })
.getOrElse(error("Failed to detect version in " + readme))
}
val component = "llncs-" + version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component), progress = progress)
Isabelle_System.rm_tree(component_dir.path)
Isabelle_System.copy_dir(llncs_dir, component_dir.path)
Isabelle_System.make_directory(component_dir.etc)
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_LLNCS_HOME="$COMPONENT"
""")
/* README */
File.write(component_dir.README,
"""This is the Springer LaTeX LNCS style for authors from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_llncs", "build component for Springer LaTeX LNCS style",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_url
val getopts = Getopts("""
Usage: isabelle build_llncs [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
Build component for Springer LaTeX LNCS style.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_llncs(download_url = download_url, target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_pdfjs.scala b/src/Pure/Admin/build_pdfjs.scala
--- a/src/Pure/Admin/build_pdfjs.scala
+++ b/src/Pure/Admin/build_pdfjs.scala
@@ -1,102 +1,98 @@
/* Title: Pure/Admin/build_pdfjs.scala
Author: Makarius
Build Isabelle component for Mozilla PDF.js.
See also:
- https://github.com/mozilla/pdf.js
- https://github.com/mozilla/pdf.js/releases
- https://github.com/mozilla/pdf.js/wiki/Setup-PDF.js-in-a-website
*/
package isabelle
object Build_PDFjs {
/* build pdfjs component */
val default_url = "https://github.com/mozilla/pdf.js/releases/download"
val default_version = "2.14.305"
def build_pdfjs(
base_url: String = default_url,
version: String = default_version,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
-
/* component name */
val component = "pdfjs-" + version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component), progress = progress)
/* download */
val download_url = base_url + "/v" + version
Isabelle_System.with_tmp_file("archive", ext = "zip") { archive_file =>
Isabelle_System.download_file(download_url + "/pdfjs-" + version + "-legacy-dist.zip",
archive_file, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(archive_file),
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_file, component_dir.path)
}
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_PDFJS_HOME="$COMPONENT"
""")
/* README */
File.write(component_dir.README,
"""This is PDF.js from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_pdfjs", "build component for Mozilla PDF.js",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var base_url = default_url
var version = default_version
val getopts = Getopts("""
Usage: isabelle build_pdfjs [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
-V VERSION version (default: """" + default_version + """")
Build component for PDF.js.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => base_url = arg),
"V:" -> (arg => version = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_pdfjs(base_url = base_url, version = version, target_dir = target_dir,
progress = progress)
})
}
diff --git a/src/Pure/Admin/build_polyml.scala b/src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala
+++ b/src/Pure/Admin/build_polyml.scala
@@ -1,266 +1,260 @@
/* Title: Pure/Admin/build_polyml.scala
Author: Makarius
Build Poly/ML from sources.
*/
package isabelle
import scala.util.matching.Regex
object Build_PolyML {
/** platform-specific build **/
sealed case class Platform_Info(
options: List[String] = Nil,
setup: String = "",
libs: Set[String] = Set.empty)
private val platform_info = Map(
"linux" ->
Platform_Info(
options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
libs = Set("libgmp")),
"darwin" ->
Platform_Info(
options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"),
setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
libs = Set("libpolyml", "libgmp")),
"windows" ->
Platform_Info(
options =
List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
setup = MinGW.environment_export,
libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread")))
def build_polyml(
root: Path,
sha1_root: Option[Path] = None,
progress: Progress = new Progress,
arch_64: Boolean = false,
options: List[String] = Nil,
mingw: MinGW = MinGW.none
): Unit = {
if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
error("Bad Poly/ML root directory: " + root)
val platform = Isabelle_Platform.self
val polyml_platform =
(if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name
val sha1_platform = platform.arch_64 + "-" + platform.os_name
val info =
platform_info.getOrElse(platform.os_name,
error("Bad OS platform: " + quote(platform.os_name)))
if (platform.is_linux) Isabelle_System.require_command("chrpath")
/* bash */
def bash(
cwd: Path, script: String,
redirect: Boolean = false,
echo: Boolean = false
): Process_Result = {
val script1 =
if (platform.is_arm && platform.is_macos) {
"arch -arch arm64 bash -c " + Bash.string(script)
}
else mingw.bash_script(script)
progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo)
}
/* configure and make */
val configure_options =
List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") :::
info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit"))
bash(root,
info.setup + "\n" +
"""
[ -f Makefile ] && make distclean
{
./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
rm -rf target
make && make install
} || { echo "Build failed" >&2; exit 2; }
""", redirect = true, echo = true).check
/* sha1 library */
val sha1_files =
if (sha1_root.isDefined) {
val dir1 = sha1_root.get
bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check
val dir2 = dir1 + Path.explode(sha1_platform)
File.read_dir(dir2).map(entry => dir2 + Path.basic(entry))
}
else Nil
/* install */
val platform_dir = Path.explode(polyml_platform)
Isabelle_System.rm_tree(platform_dir)
Isabelle_System.make_directory(platform_dir)
for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir)
for {
d <- List("target/bin", "target/lib")
dir = root + Path.explode(d)
entry <- File.read_dir(dir)
} Isabelle_System.move_file(dir + Path.explode(entry), platform_dir)
Executable.libraries_closure(
platform_dir + Path.basic("poly").platform_exe, mingw = mingw, filter = info.libs)
/* polyc: directory prefix */
val Header = "#! */bin/sh".r
File.change_lines(platform_dir + Path.explode("polyc")) {
case Header() :: lines =>
val lines1 =
lines.map(line =>
if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
else line)
"#!/usr/bin/env bash" :: lines1
case lines =>
error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
}
}
/** skeleton for component **/
private def extract_sources(source_archive: Path, component_dir: Path): Unit = {
- if (source_archive.get_ext == "zip") {
- Isabelle_System.bash(
- "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check
- }
- else {
- Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
- }
+ Isabelle_System.extract(source_archive, component_dir)
val src_dir = component_dir + Path.explode("src")
File.read_dir(component_dir) match {
case List(s) => Isabelle_System.move_file(component_dir + Path.basic(s), src_dir)
case _ => error("Source archive contains multiple directories")
}
val lines = split_lines(File.read(src_dir + Path.explode("RootX86.ML")))
val ml_files =
for {
line <- lines
rest <- Library.try_unprefix("use", line)
} yield "ML_file" + rest
File.write(src_dir + Path.explode("ROOT.ML"),
"""(* Poly/ML Compiler root file.
When this file is open in the Prover IDE, the ML files of the Poly/ML
compiler can be explored interactively. This is a separate copy: it does
not affect the running ML session. *)
""" + ml_files.mkString("\n", "\n", "\n"))
}
def build_polyml_component(
source_archive: Path,
component_path: Path,
sha1_root: Option[Path] = None
): Unit = {
val component_dir = Components.Directory.create(component_path)
extract_sources(source_archive, component_path)
Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/settings"), component_dir.etc)
Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/README"), component_dir.path)
sha1_root match {
case Some(dir) =>
Mercurial.repository(dir)
.archive(File.standard_path(component_dir.path + Path.explode("sha1")))
case None =>
}
}
/** Isabelle tool wrappers **/
val isabelle_tool1 =
Isabelle_Tool("build_polyml", "build Poly/ML from sources", Scala_Project.here,
{ args =>
var mingw = MinGW.none
var arch_64 = false
var sha1_root: Option[Path] = None
val getopts = Getopts("""
Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
Options are:
-M DIR msys/mingw root specification for Windows
-m ARCH processor architecture (32 or 64, default: """ +
(if (arch_64) "64" else "32") + """)
-s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1
Build Poly/ML in the ROOT directory of its sources, with additional
CONFIGURE_OPTIONS (e.g. --without-gmp).
""",
"M:" -> (arg => mingw = MinGW(Path.explode(arg))),
"m:" ->
{
case "32" => arch_64 = false
case "64" => arch_64 = true
case bad => error("Bad processor architecture: " + quote(bad))
},
"s:" -> (arg => sha1_root = Some(Path.explode(arg))))
val more_args = getopts(args)
val (root, options) =
more_args match {
case root :: options => (Path.explode(root), options)
case Nil => getopts.usage()
}
build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
arch_64 = arch_64, options = options, mingw = mingw)
})
val isabelle_tool2 =
Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component",
Scala_Project.here,
{ args =>
var sha1_root: Option[Path] = None
val getopts = Getopts("""
Usage: isabelle build_polyml_component [OPTIONS] SOURCE_ARCHIVE COMPONENT_DIR
Options are:
-s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1
Make skeleton for Poly/ML component, based on official source archive
(zip or tar.gz).
""",
"s:" -> (arg => sha1_root = Some(Path.explode(arg))))
val more_args = getopts(args)
val (source_archive, component_dir) =
more_args match {
case List(archive, dir) => (Path.explode(archive), Path.explode(dir))
case _ => getopts.usage()
}
build_polyml_component(source_archive, component_dir, sha1_root = sha1_root)
})
}
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,515 +1,524 @@
/* 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,
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 (gnutar_check) bash("tar " + options + args, redirect = redirect)
else error("Expected to find GNU tar executable")
}
+ def extract(archive: Path, dir: Path): Unit =
+ archive.get_ext match {
+ case "zip" =>
+ Isabelle_System.bash("unzip -x " + File.bash_path(archive.absolute), cwd = dir.file).check
+ case "tar.gz" | "tgz" =>
+ Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+ case _ => 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/Tools/VSCode/src/build_vscodium.scala b/src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala
+++ b/src/Tools/VSCode/src/build_vscodium.scala
@@ -1,476 +1,469 @@
/* Title: Tools/VSCode/src/build_vscodium.scala
Author: Makarius
Build the Isabelle system component for VSCodium: cross-compilation for all
platforms.
*/
package isabelle.vscode
import isabelle._
import java.security.MessageDigest
import java.util.Base64
object Build_VSCodium {
/* global parameters */
lazy val version: String = Isabelle_System.getenv_strict("ISABELLE_VSCODE_VERSION")
val vscodium_repository = "https://github.com/VSCodium/vscodium.git"
val vscodium_download = "https://github.com/VSCodium/vscodium/releases/download"
private val resources = Path.explode("resources")
/* Isabelle symbols (static subset only) */
def make_symbols(): File.Content = {
val symbols = Symbol.Symbols.load(static = true)
val symbols_js =
JSON.Format.pretty_print(
for (entry <- symbols.entries) yield
JSON.Object(
"symbol" -> entry.symbol,
"name" -> entry.name,
"abbrevs" -> entry.abbrevs) ++
JSON.optional("code", entry.code))
File.content(Path.explode("symbols.json"), symbols_js)
}
def make_isabelle_encoding(header: String): File.Content = {
val symbols = Symbol.Symbols.load(static = true)
val symbols_js =
JSON.Format.pretty_print(
for (entry <- symbols.entries; code <- entry.code)
yield JSON.Object("symbol" -> entry.symbol, "code" -> code))
val path = Path.explode("isabelle_encoding.ts")
val body =
File.read(Path.explode("$ISABELLE_VSCODE_HOME/patches") + path)
.replace("[/*symbols*/]", symbols_js)
File.content(path, header + "\n" + body)
}
/* platform info */
sealed case class Platform_Info(
platform: Platform.Family.Value,
download_template: String,
build_name: String,
env: List[String]
) {
def is_linux: Boolean = platform == Platform.Family.linux
def download_name: String = "VSCodium-" + download_template.replace("{VERSION}", version)
def download_zip: Boolean = File.is_zip(download_name)
def download(dir: Path, progress: Progress = new Progress): Unit = {
- if (download_zip) Isabelle_System.require_command("unzip", test = "-h")
-
Isabelle_System.with_tmp_file("download") { download_file =>
Isabelle_System.download_file(vscodium_download + "/" + version + "/" + download_name,
download_file, progress = progress)
progress.echo("Extract ...")
- if (download_zip) {
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file), cwd = dir.file).check
- }
- else {
- Isabelle_System.gnutar("-xzf " + File.bash_path(download_file), dir = dir).check
- }
+ Isabelle_System.extract(download_file, dir)
}
}
def get_vscodium_repository(build_dir: Path, progress: Progress = new Progress): Unit = {
progress.echo("Getting VSCodium repository ...")
Isabelle_System.bash(
List(
"set -e",
"git clone -n " + Bash.string(vscodium_repository) + " .",
"git checkout -q " + Bash.string(version)
).mkString("\n"), cwd = build_dir.file).check
progress.echo("Getting VSCode repository ...")
Isabelle_System.bash(environment + "\n" + "./get_repo.sh", cwd = build_dir.file).check
}
def platform_dir(dir: Path): Path = {
val platform_name =
if (platform == Platform.Family.windows) Platform.Family.native(platform)
else Platform.Family.standard(platform)
dir + Path.explode(platform_name)
}
def build_dir(dir: Path): Path = dir + Path.explode(build_name)
def environment: String =
(("MS_TAG=" + Bash.string(version)) :: "SHOULD_BUILD=yes" :: "VSCODE_ARCH=x64" :: env)
.map(s => "export " + s + "\n").mkString
def patch_sources(base_dir: Path): String = {
val dir = base_dir + Path.explode("vscode")
Isabelle_System.with_copy_dir(dir, dir.orig) {
// macos icns
for (name <- Seq("build/lib/electron.js", "build/lib/electron.ts")) {
File.change(dir + Path.explode(name), strict = true) {
_.replace("""'resources/darwin/' + icon + '.icns'""",
"""'resources/darwin/' + icon.toLowerCase() + '.icns'""")
}
}
// isabelle_encoding.ts
{
val common_dir = dir + Path.explode("src/vs/workbench/services/textfile/common")
val header =
split_lines(File.read(common_dir + Path.explode("encoding.ts")))
.takeWhile(_.trim.nonEmpty)
make_isabelle_encoding(cat_lines(header)).write(common_dir)
}
// explicit patches
{
val patches_dir = Path.explode("$ISABELLE_VSCODE_HOME/patches")
for (name <- Seq("cli", "isabelle_encoding", "no_ocaml_icons")) {
val path = patches_dir + Path.explode(name).patch
Isabelle_System.bash("patch -p1 < " + File.bash_path(path), cwd = dir.file).check
}
}
Isabelle_System.make_patch(base_dir, dir.base.orig, dir.base)
}
}
def patch_resources(base_dir: Path): String = {
val dir = base_dir + resources
val patch =
Isabelle_System.with_copy_dir(dir, dir.orig) {
val fonts_dir = dir + Path.explode("app/out/vs/base/browser/ui/fonts")
HTML.init_fonts(fonts_dir.dir)
make_symbols().write(fonts_dir)
val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css")
val checksum1 = file_checksum(workbench_css)
File.append(workbench_css, "\n\n" + HTML.fonts_css_dir(prefix = "../base/browser/ui"))
val checksum2 = file_checksum(workbench_css)
val file_name = workbench_css.file_name
File.change_lines(dir + Path.explode("app/product.json")) { _.map(line =>
if (line.containsSlice(file_name) && line.contains(checksum1)) {
line.replace(checksum1, checksum2)
}
else line)
}
Isabelle_System.make_patch(dir.dir, dir.orig.base, dir.base)
}
val app_dir = dir + Path.explode("app")
val vscodium_app_dir = dir + Path.explode("vscodium")
Isabelle_System.move_file(app_dir, vscodium_app_dir)
Isabelle_System.make_directory(app_dir)
if ((vscodium_app_dir + resources).is_dir) {
Isabelle_System.copy_dir(vscodium_app_dir + resources, app_dir)
}
patch
}
def init_resources(base_dir: Path): Path = {
val dir = base_dir + resources
if (platform == Platform.Family.macos) {
Isabelle_System.symlink(Path.explode("VSCodium.app/Contents/Resources"), dir)
}
dir
}
def setup_node(target_dir: Path, progress: Progress): Unit = {
Isabelle_System.with_tmp_dir("download") { download_dir =>
download(download_dir, progress = progress)
val dir1 = init_resources(download_dir)
val dir2 = init_resources(target_dir)
for (name <- Seq("app/node_modules.asar", "app/node_modules.asar.unpacked")) {
val path = Path.explode(name)
Isabelle_System.rm_tree(dir2 + path)
Isabelle_System.copy_dir(dir1 + path, dir2 + path)
}
}
}
def setup_electron(dir: Path): Unit = {
val electron = Path.explode("electron")
platform match {
case Platform.Family.linux | Platform.Family.linux_arm =>
Isabelle_System.move_file(dir + Path.explode("codium"), dir + electron)
case Platform.Family.windows =>
Isabelle_System.move_file(dir + Path.explode("VSCodium.exe"), dir + electron.exe)
Isabelle_System.move_file(
dir + Path.explode("VSCodium.VisualElementsManifest.xml"),
dir + Path.explode("electron.VisualElementsManifest.xml"))
case Platform.Family.macos =>
}
}
def setup_executables(dir: Path): Unit = {
Isabelle_System.rm_tree(dir + Path.explode("bin"))
if (platform == Platform.Family.windows) {
val files =
File.find_files(dir.file, pred = { file =>
val name = file.getName
File.is_dll(name) || File.is_exe(name) || File.is_node(name)
})
files.foreach(file => File.set_executable(File.path(file), true))
Isabelle_System.bash("chmod -R o-w " + File.bash_path(dir)).check
}
}
}
// see https://github.com/microsoft/vscode/blob/main/build/gulpfile.vscode.js
// function computeChecksum(filename)
private def file_checksum(path: Path): String = {
val digest = MessageDigest.getInstance("MD5")
digest.update(Bytes.read(path).array)
Bytes(Base64.getEncoder.encode(digest.digest()))
.text.replaceAll("=", "")
}
private val platform_infos: Map[Platform.Family.Value, Platform_Info] =
Iterator(
Platform_Info(Platform.Family.linux, "linux-x64-{VERSION}.tar.gz", "VSCode-linux-x64",
List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True")),
Platform_Info(Platform.Family.linux_arm, "linux-arm64-{VERSION}.tar.gz", "VSCode-linux-arm64",
List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True", "VSCODE_ARCH=arm64")),
Platform_Info(Platform.Family.macos, "darwin-x64-{VERSION}.zip", "VSCode-darwin-x64",
List("OS_NAME=osx")),
Platform_Info(Platform.Family.windows, "win32-x64-{VERSION}.zip", "VSCode-win32-x64",
List("OS_NAME=windows",
"SHOULD_BUILD_ZIP=no",
"SHOULD_BUILD_EXE_SYS=no",
"SHOULD_BUILD_EXE_USR=no",
"SHOULD_BUILD_MSI=no",
"SHOULD_BUILD_MSI_NOUP=no")))
.map(info => info.platform -> info).toMap
def the_platform_info(platform: Platform.Family.Value): Platform_Info =
platform_infos.getOrElse(platform, error("No platform info for " + quote(platform.toString)))
def linux_platform_info: Platform_Info =
the_platform_info(Platform.Family.linux)
/* check system */
def check_system(platforms: List[Platform.Family.Value]): Unit = {
if (Platform.family != Platform.Family.linux) error("Not a Linux/x86_64 system")
Isabelle_System.require_command("git")
Isabelle_System.require_command("node")
Isabelle_System.require_command("yarn")
Isabelle_System.require_command("jq")
if (platforms.contains(Platform.Family.windows)) {
Isabelle_System.require_command("wine")
}
if (platforms.exists(platform => the_platform_info(platform).download_zip)) {
Isabelle_System.require_command("unzip", test = "-h")
}
}
/* original repository clones and patches */
def vscodium_patch(verbose: Boolean = false, progress: Progress = new Progress): String = {
val platform_info = linux_platform_info
check_system(List(platform_info.platform))
Isabelle_System.with_tmp_dir("build") { build_dir =>
platform_info.get_vscodium_repository(build_dir, progress = progress)
val vscode_dir = build_dir + Path.explode("vscode")
progress.echo("Prepare ...")
Isabelle_System.with_copy_dir(vscode_dir, vscode_dir.orig) {
progress.bash(
List(
"set -e",
platform_info.environment,
"./prepare_vscode.sh",
// enforce binary diff of code.xpm
"cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm"
).mkString("\n"), cwd = build_dir.file, echo = verbose).check
Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base,
diff_options = "--exclude=.git --exclude=node_modules")
}
}
}
/* build vscodium */
def default_platforms: List[Platform.Family.Value] = Platform.Family.list
def build_vscodium(
target_dir: Path = Path.current,
platforms: List[Platform.Family.Value] = default_platforms,
verbose: Boolean = false,
progress: Progress = new Progress
): Unit = {
check_system(platforms)
/* component */
val component_name = "vscodium-" + version
val component_dir =
Components.Directory.create(target_dir + Path.explode(component_name), progress = progress)
/* patches */
progress.echo("\n* Building patches:")
val patches_dir = Isabelle_System.new_directory(component_dir.path + Path.explode("patches"))
def write_patch(name: String, patch: String): Unit =
File.write(patches_dir + Path.explode(name).patch, patch)
write_patch("01-vscodium", vscodium_patch(verbose = verbose, progress = progress))
/* build */
for (platform <- platforms) yield {
val platform_info = the_platform_info(platform)
Isabelle_System.with_tmp_dir("build") { build_dir =>
progress.echo("\n* Building " + platform + ":")
platform_info.get_vscodium_repository(build_dir, progress = progress)
val sources_patch = platform_info.patch_sources(build_dir)
if (platform_info.is_linux) write_patch("02-isabelle_sources", sources_patch)
progress.echo("Build ...")
progress.bash(platform_info.environment + "\n" + "./build.sh",
cwd = build_dir.file, echo = verbose).check
if (platform_info.is_linux) {
Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
}
val platform_dir = platform_info.platform_dir(component_dir.path)
Isabelle_System.copy_dir(platform_info.build_dir(build_dir), platform_dir)
platform_info.setup_node(platform_dir, progress)
platform_info.setup_electron(platform_dir)
val resources_patch = platform_info.patch_resources(platform_dir)
if (platform_info.is_linux) write_patch("03-isabelle_resources", resources_patch)
Isabelle_System.copy_file(
build_dir + Path.explode("vscode/node_modules/electron/dist/resources/default_app.asar"),
platform_dir + resources)
platform_info.setup_executables(platform_dir)
}
}
Isabelle_System.bash("gzip *.patch", cwd = patches_dir.file).check
/* settings */
File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_VSCODIUM_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then
ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/MacOS/Electron"
ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/Resources"
else
ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/electron"
ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/resources"
fi
""")
/* README */
File.write(component_dir.README,
"This is VSCodium " + version + " from " + vscodium_repository +
"""
It has been built from sources using "isabelle build_vscodium". This applies
a few changes required for Isabelle/VSCode, see "patches" directory for a
formal record.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/* Isabelle tool wrappers */
val isabelle_tool1 =
Isabelle_Tool("build_vscodium", "build component for VSCodium",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var platforms = default_platforms
var verbose = false
val getopts = Getopts("""
Usage: build_vscodium [OPTIONS]
Options are:
-D DIR target directory (default ".")
-p NAMES platform families (default: """ + quote(platforms.mkString(",")) + """)
-v verbose
Build VSCodium from sources and turn it into an Isabelle component.
The build platform needs to be Linux with nodejs/yarn, jq, and wine
for targeting Windows.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_vscodium(target_dir = target_dir, platforms = platforms,
verbose = verbose, progress = progress)
})
val isabelle_tool2 =
Isabelle_Tool("vscode_patch", "patch VSCode source tree",
Scala_Project.here,
{ args =>
var base_dir = Path.current
val getopts = Getopts("""
Usage: vscode_patch [OPTIONS]
Options are:
-D DIR base directory (default ".")
Patch original VSCode source tree for use with Isabelle/VSCode.
""",
"D:" -> (arg => base_dir = Path.explode(arg)))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val platform_info = the_platform_info(Platform.family)
platform_info.patch_sources(base_dir)
})
}