diff --git a/src/Pure/Admin/build_csdp.scala b/src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala
+++ b/src/Pure/Admin/build_csdp.scala
@@ -1,198 +1,196 @@
/* Title: Pure/Admin/build_csdp.scala
Author: Makarius
Build Isabelle CSDP component from official download.
*/
package isabelle
object Build_CSDP {
// Note: version 6.2.0 does not quite work for the "sos" proof method
val default_download_url = "https://github.com/coin-or/Csdp/archive/releases/6.1.1.tar.gz"
/* flags */
sealed case class Flags(platform: String, CFLAGS: String = "", LIBS: String = "") {
val changed: List[(String, String)] =
List("CFLAGS" -> CFLAGS, "LIBS" -> LIBS).filter(p => p._2.nonEmpty)
def print: Option[String] =
if (changed.isEmpty) None
else
Some(" * " + platform + ":\n" + changed.map(p => " " + Properties.Eq(p))
.mkString("\n"))
def change(path: Path): Unit = {
def change_line(line: String, p: (String, String)): String =
line.replaceAll(p._1 + "=.*", Properties.Eq(p))
File.change_lines(path) { _.map(line => changed.foldLeft(line)(change_line)) }
}
}
val build_flags: List[Flags] =
List(
Flags("arm64-linux",
CFLAGS = "-O3 -ansi -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include",
LIBS = "-static -L../lib -lsdp -llapack -lblas -lgfortran -lm"),
Flags("x86_64-linux",
CFLAGS = "-O3 -ansi -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include",
LIBS = "-static -L../lib -lsdp -llapack -lblas -lgfortran -lquadmath -lm"),
Flags("x86_64-darwin",
CFLAGS = "-O3 -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include",
LIBS = "-L../lib -lsdp -llapack -lblas -lm"),
Flags("x86_64-windows"))
/* build CSDP */
def build_csdp(
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current,
mingw: MinGW = MinGW.none
): Unit = {
mingw.check
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
val Version = """^[^0-9]*([0-9].*)\.tar.gz$""".r
val archive_name =
download_url match {
case Archive_Name(name) => name
case _ => error("Failed to determine source archive name from " + quote(download_url))
}
val version =
archive_name match {
case Version(version) => version
case _ => error("Failed to determine component version from " + quote(archive_name))
}
val component_name = "csdp-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* platform */
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
val platform_dir =
Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building CSDP for " + platform_name + " ...")
build_flags.find(flags => flags.platform == platform_name) match {
case None => error("No build flags for platform " + quote(platform_name))
case Some(flags) =>
File.find_files(source_dir.file, pred = file => file.getName == "Makefile").
foreach(file => flags.change(File.path(file)))
}
progress.bash(mingw.bash_script("make"), cwd = source_dir.file, echo = verbose).check
/* install */
Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
Isabelle_System.copy_file(source_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
if (Platform.is_windows) {
Executable.libraries_closure(platform_dir + Path.explode("csdp.exe"), mingw = mingw,
filter =
Set("libblas", "liblapack", "libgfortran", "libgcc_s_seh",
"libquadmath", "libwinpthread"))
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_CSDP="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/csdp"
""")
/* README */
File.write(component_dir.README,
"""This is CSDP """ + version + """ from
""" + download_url + """
Makefile flags have been changed for various platforms as follows:
""" + build_flags.flatMap(_.print).mkString("\n\n") + """
The distribution has been built like this:
cd src && make
Only the bare "solver/csdp" program is used for Isabelle.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_csdp", "build prover component from official download", Scala_Project.here,
{ args =>
var target_dir = Path.current
var mingw = MinGW.none
var download_url = default_download_url
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_csdp [OPTIONS]
Options are:
-D DIR target directory (default ".")
-M DIR msys/mingw root specification for Windows
-U URL download URL
(default: """" + default_download_url + """")
-v verbose
Build prover component from official download.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"M:" -> (arg => mingw = MinGW(Path.explode(arg))),
"U:" -> (arg => download_url = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_csdp(download_url = download_url, verbose = verbose, progress = progress,
target_dir = target_dir, mingw = mingw)
})
}
diff --git a/src/Pure/Admin/build_cvc5.scala b/src/Pure/Admin/build_cvc5.scala
--- a/src/Pure/Admin/build_cvc5.scala
+++ b/src/Pure/Admin/build_cvc5.scala
@@ -1,137 +1,135 @@
/* Title: Pure/Admin/build_cvc5.scala
Author: Makarius
Build Isabelle component for cvc5. See also:
- https://cvc5.github.io/
- https://github.com/cvc5/cvc5
*/
package isabelle
object Build_CVC5 {
/* platform information */
sealed case class CVC5_Platform(platform_name: String, download_name: String) {
def is_windows: Boolean = platform_name.endsWith("-windows")
}
val platforms: List[CVC5_Platform] =
List(
CVC5_Platform("arm64-darwin", "cvc5-macOS-arm64"),
CVC5_Platform("x86_64-darwin", "cvc5-macOS"),
CVC5_Platform("x86_64-linux", "cvc5-Linux"),
CVC5_Platform("x86_64-windows", "cvc5-Win64.exe"))
/* build cvc5 */
val default_url = "https://github.com/cvc5/cvc5/releases/download"
val default_version = "1.0.2"
def build_cvc5(
base_url: String = default_url,
version: String = default_version,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
/* component name */
val component = "cvc5-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* download executables */
for (platform <- platforms) {
val url = base_url + "/cvc5-" + version + "/" + platform.download_name
val platform_dir = component_dir.path + Path.explode(platform.platform_name)
val platform_exe = platform_dir + Path.explode("cvc5").exe_if(platform.is_windows)
Isabelle_System.make_directory(platform_dir)
Isabelle_System.download_file(url, platform_exe, progress = progress)
File.set_executable(platform_exe, true)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
CVC5_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"
CVC5_VERSION=""" + Bash.string(version) + """
CVC5_SOLVER="$CVC5_HOME/cvc5"
if [ -e "$CVC5_HOME" ]
then
CVC5_INSTALLED="yes"
fi
""")
/* README */
File.write(component_dir.README,
"""This distribution of cvc5 was assembled from the official downloads
from """ + base_url + """ for 64bit macOS,
Linux, and Windows. There is native support for macOS ARM64, but
Linux ARM64 is missing.
The oldest supported version of macOS is 10.14 Mojave.
The downloaded files were renamed and made executable.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
/* AUTHORS and COPYING */
// download "latest" versions as reasonable approximation
def raw_download(name: String): Unit =
Isabelle_System.download_file("https://raw.githubusercontent.com/cvc5/cvc5/main/" + name,
component_dir.path + Path.explode(name))
raw_download("AUTHORS")
raw_download("COPYING")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_cvc5", "build component for cvc5", Scala_Project.here,
{ args =>
var target_dir = Path.current
var base_url = default_url
var version = default_version
val getopts = Getopts("""
Usage: isabelle build_cvc5 [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
-V VERSION version (default: """" + default_version + """")
Build component for cvc5 solver.
""",
"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_cvc5(base_url = base_url, version = version, target_dir = target_dir,
progress = progress)
})
}
diff --git a/src/Pure/Admin/build_e.scala b/src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala
+++ b/src/Pure/Admin/build_e.scala
@@ -1,140 +1,139 @@
/* Title: Pure/Admin/build_e.scala
Author: Makarius
Build Isabelle E prover component from official downloads.
*/
package isabelle
object Build_E {
/* build E prover */
val default_version = "2.6"
val default_download_url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD"
def build_e(
version: String = default_version,
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val component_name = "e-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
.getOrElse(error("No 64bit platform"))
val platform_dir =
Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_url = download_url + "/V_" + version + "/E.tgz"
val archive_path = tmp_dir + Path.explode("E.tgz")
Isabelle_System.download_file(archive_url, archive_path, progress = progress)
Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = archive_url)
Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building E prover for " + platform_name + " ...")
val build_options = {
val result = Isabelle_System.bash("./configure --help", cwd = source_dir.file)
if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else ""
}
val build_script = "./configure" + build_options + " && make"
Isabelle_System.bash(build_script, cwd = source_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
Isabelle_System.copy_file(source_dir + Path.basic("COPYING"), component_dir.LICENSE)
val install_files = List("epclextract", "eprover", "eprover-ho")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
val path = source_dir + Path.basic("PROVER") + Path.basic(name)
if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
}
Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi",
cwd = platform_dir.file).check
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
E_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
E_VERSION=""" + quote(version) + """
""")
+
/* README */
File.write(component_dir.README,
"This is E prover " + version + " from\n" + archive_url + """
The distribution has been built like this:
cd src && """ + build_script + """
Only a few executables from PROVERS/ have been moved to the platform-specific
Isabelle component directory: x86_64-linux etc.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_e", "build prover component from source distribution", Scala_Project.here,
{ args =>
var target_dir = Path.current
var version = default_version
var download_url = default_download_url
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_e [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL
(default: """" + default_download_url + """")
-V VERSION version (default: """ + default_version + """)
-v verbose
Build prover component from the specified source distribution.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg),
"V:" -> (arg => version = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_e(version = version, download_url = download_url,
verbose = verbose, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_easychair.scala b/src/Pure/Admin/build_easychair.scala
--- a/src/Pure/Admin/build_easychair.scala
+++ b/src/Pure/Admin/build_easychair.scala
@@ -1,97 +1,95 @@
/* 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.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.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(target_dir + Path.basic(component)).create(progress = progress)
Isabelle_System.extract(download_file, component_dir.path, strip = true)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
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,96 +1,94 @@
/* 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 = {
/* component */
val component = "eptcs-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(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.extract(download_file, component_dir.path)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
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,107 +1,105 @@
/* 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.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.extract(download_file, download_dir)
val foiltex_dir = File.get_dir(download_dir, title = download_url)
/* component */
val README = Path.explode("README")
val version = {
val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r
split_lines(File.read(foiltex_dir + README))
.collectFirst({ case Version(v) => v })
.getOrElse(error("Failed to detect version in " + README))
}
val component = "foiltex-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
Isabelle_System.extract(download_file, component_dir.path, strip = true)
Isabelle_System.bash("pdflatex foiltex.ins", cwd = component_dir.path.file).check
(component_dir.path + Path.basic("foiltex.log")).file.delete()
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_FOILTEX_HOME="$COMPONENT"
""")
/* README */
Isabelle_System.move_file(component_dir.README,
component_dir.path + Path.basic("README.flt"))
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_fonts.scala b/src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala
+++ b/src/Pure/Admin/build_fonts.scala
@@ -1,385 +1,383 @@
/* Title: Pure/Admin/build_fonts.scala
Author: Makarius
Build standard Isabelle fonts: DejaVu base + Isabelle symbols.
*/
package isabelle
object Build_Fonts {
/* relevant codepoint ranges */
object Range {
def base_font: Seq[Int] =
(0x0020 to 0x007e) ++ // ASCII
(0x00a0 to 0x024f) ++ // Latin Extended-A/B
(0x0400 to 0x04ff) ++ // Cyrillic
(0x0600 to 0x06ff) ++ // Arabic
Seq(
0x02dd, // hungarumlaut
0x2018, // single quote
0x2019, // single quote
0x201a, // single quote
0x201c, // double quote
0x201d, // double quote
0x201e, // double quote
0x2039, // single guillemet
0x203a, // single guillemet
0x204b, // FOOTNOTE
0x20ac, // Euro
0x2710, // pencil
0xfb01, // ligature fi
0xfb02, // ligature fl
0xfffd, // replacement character
)
def isabelle_font: Seq[Int] =
Seq(
0x05, // X
0x06, // Y
0x07, // EOF
0x7f, // DEL
0xaf, // INVERSE
0xac, // logicalnot
0xb0, // degree
0xb1, // plusminus
0xb7, // periodcentered
0xd7, // multiply
0xf7, // divide
) ++
(0x0370 to 0x03ff) ++ // Greek (pseudo math)
(0x0590 to 0x05ff) ++ // Hebrew (non-mono)
Seq(
0x2010, // hyphen
0x2013, // dash
0x2014, // dash
0x2015, // dash
0x2016, // big parallel
0x2020, // dagger
0x2021, // double dagger
0x2022, // bullet
0x2026, // ellipsis
0x2030, // perthousand
0x2032, // minute
0x2033, // second
0x2038, // caret
0x2040, // sequence concatenation
0x20cd, // currency symbol
) ++
(0x2100 to 0x214f) ++ // Letterlike Symbols
(0x2190 to 0x21ff) ++ // Arrows
(0x2200 to 0x22ff) ++ // Mathematical Operators
(0x2300 to 0x23ff) ++ // Miscellaneous Technical
Seq(
0x2423, // graphic for space
0x2500, // box drawing
0x2501, // box drawing
0x2508, // box drawing
0x2509, // box drawing
0x2550, // box drawing
) ++
(0x25a0 to 0x25ff) ++ // Geometric Shapes
Seq(
0x261b, // ACTION
0x2660, // spade suit
0x2661, // heart suit
0x2662, // diamond suit
0x2663, // club suit
0x266d, // musical flat
0x266e, // musical natural
0x266f, // musical sharp
0x2713, // check mark
0x2717, // ballot X
0x2756, // UNDEFINED
0x2759, // BOLD
0x27a7, // DESCR
0x27e6, // left white square bracket
0x27e7, // right white square bracket
0x27e8, // left angle bracket
0x27e9, // right angle bracket
0x27ea, // left double angle bracket
0x27eb, // right double angle bracket
) ++
(0x27f0 to 0x27ff) ++ // Supplemental Arrows-A
(0x2900 to 0x297f) ++ // Supplemental Arrows-B
(0x2980 to 0x29ff) ++ // Miscellaneous Mathematical Symbols-B
(0x2a00 to 0x2aff) ++ // Supplemental Mathematical Operators
Seq(0x2b1a) ++ // VERBATIM
(0x1d400 to 0x1d7ff) ++ // Mathematical Alphanumeric Symbols
Seq(
0x1f310, // globe with meridians (Symbola font)
0x1f4d3, // notebook (Symbola font)
0x1f5c0, // folder (Symbola font)
0x1f5cf, // page (Symbola font)
)
def isabelle_math_font: Seq[Int] =
(0x21 to 0x2f) ++ // bang .. slash
(0x3a to 0x40) ++ // colon .. atsign
(0x5b to 0x5f) ++ // leftbracket .. underscore
(0x7b to 0x7e) ++ // leftbrace .. tilde
Seq(
0xa9, // copyright
0xae, // registered
)
val vacuous_font: Seq[Int] =
Seq(0x3c) // "<" as template
}
/* font families */
sealed case class Family(
plain: String = "",
bold: String = "",
italic: String = "",
bold_italic: String = ""
) {
val fonts: List[String] =
proper_string(plain).toList :::
proper_string(bold).toList :::
proper_string(italic).toList :::
proper_string(bold_italic).toList
def get(index: Int): String = fonts(index % fonts.length)
}
object Family {
def isabelle_symbols: Family =
Family(
plain = "IsabelleSymbols.sfd",
bold = "IsabelleSymbolsBold.sfd")
def deja_vu_sans_mono: Family =
Family(
plain = "DejaVuSansMono.ttf",
bold = "DejaVuSansMono-Bold.ttf",
italic = "DejaVuSansMono-Oblique.ttf",
bold_italic = "DejaVuSansMono-BoldOblique.ttf")
def deja_vu_sans: Family =
Family(
plain = "DejaVuSans.ttf",
bold = "DejaVuSans-Bold.ttf",
italic = "DejaVuSans-Oblique.ttf",
bold_italic = "DejaVuSans-BoldOblique.ttf")
def deja_vu_serif: Family =
Family(
plain = "DejaVuSerif.ttf",
bold = "DejaVuSerif-Bold.ttf",
italic = "DejaVuSerif-Italic.ttf",
bold_italic = "DejaVuSerif-BoldItalic.ttf")
def vacuous: Family = Family(plain = "Vacuous.sfd")
}
/* hinting */
// see https://www.freetype.org/ttfautohint/doc/ttfautohint.html
private def auto_hint(source: Path, target: Path): Unit = {
Isabelle_System.bash("ttfautohint -i " +
File.bash_path(source) + " " + File.bash_path(target)).check
}
private def make_path(hinted: Boolean = false): Path =
if (hinted) Path.basic("ttf-hinted") else Path.basic("ttf")
private val hinting = List(false, true)
/* build fonts */
private def find_file(dirs: List[Path], name: String): Path = {
val path = Path.explode(name)
dirs.collectFirst({ case dir if (dir + path).is_file => dir + path }) match {
case Some(file) => file
case None =>
error(cat_lines(
("Failed to find font file " + path + " in directories:") ::
dirs.map(dir => " " + dir.toString)))
}
}
val default_download_url =
"https://github.com/dejavu-fonts/dejavu-fonts/releases/download/version_2_37/dejavu-fonts-ttf-2.37.zip"
val default_sources: List[Family] =
List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif)
def build_fonts(
download_url: String = default_download_url,
target_dir: Path = Path.current,
target_prefix: String = "Isabelle",
sources: List[Family] = default_sources,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("ttfautohint")
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.extract(download_file, download_dir)
val dejavu_dir = File.get_dir(download_dir, title = download_url) + Path.basic("ttf")
/* component */
val component_date = Date.Format.alt_date(Date.now())
val component_name = "isabelle_fonts-" + component_date
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
for (hinted <- hinting) {
Isabelle_System.make_directory(component_dir.path + make_path(hinted = hinted))
}
val font_dirs = List(dejavu_dir, Path.explode("~~/Admin/isabelle_fonts"))
for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)
// Isabelle fonts
val fonts =
for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex }
yield {
val isabelle_file = find_file(font_dirs, Family.isabelle_symbols.get(index))
val source_file = find_file(font_dirs, source_font)
val source_names = Fontforge.font_names(source_file)
val font_names = source_names.update(prefix = target_prefix, version = component_date)
Isabelle_System.with_tmp_file("font", "ttf") { tmp_file =>
for (hinted <- hinting) {
val font_file = component_dir.path + make_path(hinted = hinted) + font_names.ttf
progress.echo("Font " + font_file + " ...")
if (hinted) auto_hint(source_file, tmp_file)
else Isabelle_System.copy_file(source_file, tmp_file)
Fontforge.execute(
Fontforge.commands(
Fontforge.open(isabelle_file),
Fontforge.select(Range.isabelle_font),
Fontforge.copy,
Fontforge.close,
Fontforge.open(tmp_file),
Fontforge.select(Range.base_font),
Fontforge.select_invert,
Fontforge.clear,
Fontforge.select(Range.isabelle_font),
Fontforge.paste,
font_names.set,
Fontforge.generate(font_file),
Fontforge.close)
).check
}
}
(font_names.ttf, index)
}
// Vacuous font
{
val vacuous_file = find_file(font_dirs, Family.vacuous.get(0))
val font_dir = component_dir.path + make_path()
val font_names = Fontforge.font_names(vacuous_file)
val font_file = font_dir + font_names.ttf
progress.echo("Font " + font_file + " ...")
val domain =
(for ((name, index) <- fonts if index == 0)
yield Fontforge.font_domain(font_dir + name))
.flatten.distinct.sorted
Fontforge.execute(
Fontforge.commands(
Fontforge.open(vacuous_file),
Fontforge.select(Range.vacuous_font),
Fontforge.copy) +
domain.map(code =>
Fontforge.commands(
Fontforge.select(Seq(code)),
Fontforge.paste))
.mkString("\n", "\n", "\n") +
Fontforge.commands(
Fontforge.generate(font_file),
Fontforge.close)
).check
}
/* settings */
def make_settings(hinted: Boolean = false): String =
"\n isabelle_fonts \\\n" +
(for ((ttf, _) <- fonts) yield
""" "$COMPONENT/""" + make_path(hinted = hinted).file_name + "/" + ttf.file_name + "\"")
.mkString(" \\\n")
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
if grep "isabelle_fonts_hinted.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
then""" + make_settings() + """
else""" + make_settings(hinted = true) + """
fi
isabelle_fonts_hidden "$COMPONENT/""" + make_path().file_name + """/Vacuous.ttf"
""")
/* README */
Isabelle_System.copy_file(
Path.explode("~~/Admin/isabelle_fonts/README"), component_dir.README)
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_fonts", "construct Isabelle fonts", Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_download_url
val getopts = Getopts("""
Usage: isabelle build_fonts [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_download_url + """")
Construct Isabelle fonts from DejaVu font families and Isabelle symbols.
""",
"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_fonts(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,167 +1,165 @@
/* Title: Pure/Admin/build_jdk.scala
Author: Makarius
Build Isabelle jdk component using downloads from Azul.
*/
package isabelle
import java.nio.file.Files
import java.nio.file.attribute.PosixFilePermission
object Build_JDK {
/* platform information */
sealed case class JDK_Platform(name: String, url_template: String) {
override def toString: String = name
def url(base_url: String, jdk_version: String, zulu_version: String): String =
base_url + "/" + url_template.replace("{V}", jdk_version).replace("{Z}", zulu_version)
}
val platforms: List[JDK_Platform] =
List(
JDK_Platform("arm64-darwin", "zulu{Z}-jdk{V}-macosx_aarch64.tar.gz"),
JDK_Platform("arm64-linux", "zulu{Z}-jdk{V}-linux_aarch64.tar.gz"),
JDK_Platform("x86_64-darwin", "zulu{Z}-jdk{V}-macosx_x64.tar.gz"),
JDK_Platform("x86_64-linux", "zulu{Z}-jdk{V}-linux_x64.tar.gz"),
JDK_Platform("x86_64-windows", "zulu{Z}-jdk{V}-win_x64.zip"))
/* build jdk */
val default_base_url = "https://cdn.azul.com/zulu/bin"
val default_jdk_version = "17.0.5"
val default_zulu_version = "17.38.21-ca"
def build_jdk(
target_dir: Path = Path.current,
base_url: String = default_base_url,
jdk_version: String = default_jdk_version,
zulu_version: String = default_zulu_version,
progress: Progress = new Progress,
): Unit = {
if (Platform.is_windows) error("Cannot build on Windows")
/* component */
val component = "jdk-" + jdk_version
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* download */
for (platform <- platforms) {
Isabelle_System.with_tmp_dir("download", component_dir.path.file) { dir =>
val url = platform.url(base_url, jdk_version, zulu_version)
val name = Library.take_suffix(_ != '/', url.toList)._2.mkString
val file = dir + Path.basic(name)
Isabelle_System.download_file(url, file, progress = progress)
val platform_dir = component_dir.path + Path.basic(platform.name)
Isabelle_System.extract(file, platform_dir, strip = true)
}
}
/* permissions */
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)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
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
""")
/* README */
File.write(component_dir.README,
"""This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also
https://www.azul.com/downloads/?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.
""")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_jdk", "build Isabelle jdk component using downloads from Azul",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var base_url = default_base_url
var jdk_version = default_jdk_version
var zulu_version = default_zulu_version
val getopts = Getopts("""
Usage: isabelle build_jdk [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL base URL (default: """" + default_base_url + """")
-V NAME JDK version (default: """" + default_jdk_version + """")
-Z NAME Zulu version (default: """" + default_zulu_version + """")
Build Isabelle jdk component using downloads from Azul.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => base_url = arg),
"V:" -> (arg => jdk_version = arg),
"Z:" -> (arg => zulu_version = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_jdk(target_dir = target_dir, base_url = base_url,
jdk_version = jdk_version, zulu_version = zulu_version, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_jedit.scala b/src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala
+++ b/src/Pure/Admin/build_jedit.scala
@@ -1,543 +1,541 @@
/* Title: Pure/Admin/build_jedit.scala
Author: Makarius
Build component for jEdit text-editor.
*/
package isabelle
import java.nio.charset.Charset
import scala.jdk.CollectionConverters._
object Build_JEdit {
/* modes */
object Mode {
val empty: Mode = new Mode("", "", Nil)
val init: Mode =
empty +
("noWordSep" -> """_'?⇩\^<>""") +
("unalignedOpenBrackets" -> "{[(«‹⟨⌈⌊⦇⟦⦃⦉") +
("unalignedCloseBrackets" -> "⦊⦄⟧⦈⌋⌉⟩›»)]}") +
("tabSize" -> "2") +
("indentSize" -> "2")
val list: List[Mode] = {
val isabelle_news: Mode = init.define("isabelle-news", "Isabelle NEWS")
val isabelle: Mode =
init.define("isabelle", "Isabelle theory") +
("commentStart" -> "(*") +
("commentEnd" -> "*)")
val isabelle_ml: Mode = isabelle.define("isabelle-ml", "Isabelle/ML")
val isabelle_root: Mode = isabelle.define("isabelle-root", "Isabelle session root")
val isabelle_options: Mode = isabelle.define("isabelle-options", "Isabelle options")
val sml: Mode =
init.define("sml", "Standard ML") +
("commentStart" -> "(*") +
("commentEnd" -> "*)") +
("noWordSep" -> "_'")
List(isabelle_news, isabelle, isabelle_ml, isabelle_root, isabelle_options, sml)
}
}
final case class Mode private(name: String, description: String, rev_props: Properties.T) {
override def toString: String = name
def define(a: String, b: String): Mode = new Mode(a, b, rev_props)
def + (entry: Properties.Entry): Mode =
new Mode(name, description, Properties.put(rev_props, entry))
def write(dir: Path): Unit = {
require(name.nonEmpty && description.nonEmpty, "Bad Isabelle/jEdit mode content")
val properties =
rev_props.reverse.map(p =>
Symbol.spaces(4) +
XML.string_of_tree(XML.elem(Markup("PROPERTY", List("NAME" -> p._1, "VALUE" -> p._2)))))
File.write(dir + Path.basic(name).xml,
"""
""" + properties.mkString("\n", "\n", "") + """
""")
}
}
/* build jEdit component */
private val download_jars: List[(String, String)] =
List(
"https://repo1.maven.org/maven2/com/google/code/findbugs/jsr305/3.0.2/jsr305-3.0.2.jar" ->
"jsr305-3.0.2.jar")
private val download_plugins: List[(String, String)] =
List(
"Code2HTML" -> "0.7",
"CommonControls" -> "1.7.4",
"Console" -> "5.1.4",
"ErrorList" -> "2.4.0",
"Highlight" -> "2.5",
"Navigator" -> "2.7",
"SideKick" -> "1.8")
private def exclude_package(name: String): Boolean =
name.startsWith("de.masters_of_disaster.ant") ||
name == "doclet" ||
name == "installer"
def build_jedit(
component_path: Path,
version: String,
original: Boolean = false,
java_home: Path = default_java_home,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("ant", test = "-version")
Isabelle_System.require_command("patch")
val component_dir = Components.Directory(component_path).create(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.extract(source_path, jedit_dir)
/* patched version */
Isabelle_System.copy_dir(jedit_dir, jedit_patched_dir)
val source_dir = jedit_patched_dir + Path.basic("jEdit")
val org_source_dir = source_dir + Path.basic("org")
val tmp_source_dir = tmp_dir + Path.basic("jEdit")
progress.echo("Patching jEdit sources ...")
for {
file <- File.find_files(Path.explode("~~/src/Tools/jEdit/patches").file).sortBy(_.getName)
name = file.getName
if !File.is_backup(name)
} {
progress.bash("patch -p2 < " + File.bash_path(File.path(file)),
cwd = source_dir.file, echo = true).check
}
for { theme <- List("classic", "tango") } {
val path = Path.explode("org/gjt/sp/jedit/icons/themes/" + theme + "/32x32/apps/isabelle.gif")
Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle_transparent-32.gif"),
source_dir + path)
}
progress.echo("Building jEdit ...")
Isabelle_System.copy_dir(source_dir, tmp_source_dir)
progress.bash("env JAVA_HOME=" + File.bash_platform_path(java_home) + " ant",
cwd = tmp_source_dir.file, echo = true).check
Isabelle_System.copy_file(tmp_source_dir + Path.explode("build/jedit.jar"), jedit_patched_dir)
val java_sources =
(for {
file <- File.find_files(org_source_dir.file, file => File.is_java(file.getName))
package_name <- Scala_Project.package_name(File.path(file))
if !exclude_package(package_name)
} yield File.path(component_path.java_path.relativize(file.toPath).toFile).implode).sorted
File.write(component_dir.build_props,
"module = " + jedit_patched + "/jedit.jar\n" +
"no_build = true\n" +
"requirements = env:JEDIT_JARS\n" +
("sources =" :: java_sources.sorted.map(" " + _)).mkString("", " \\\n", "\n"))
}
/* jars */
val jars_dir = Isabelle_System.make_directory(jedit_patched_dir + Path.basic("jars"))
for { (url, name) <- download_jars } {
Isabelle_System.download_file(url, jars_dir + Path.basic(name), progress = progress)
}
for { (name, vers) <- download_plugins } {
Isabelle_System.with_tmp_file("tmp", ext = "zip") { zip_path =>
val url =
"https://sourceforge.net/projects/jedit-plugins/files/" + name + "/" + vers + "/" +
name + "-" + vers + "-bin.zip/download"
Isabelle_System.download_file(url, zip_path, progress = progress)
Isabelle_System.extract(zip_path, jars_dir)
}
}
/* resources */
val keep_encodings = List("ISO-8859-1", "ISO-8859-15", "US-ASCII", "UTF-8", "windows-1252")
val drop_encodings =
Charset.availableCharsets().keySet().asScala.toList.sorted.filterNot(keep_encodings.contains)
File.write(jedit_patched_dir + Path.explode("properties/jEdit.props"),
"""#jEdit properties
autoReloadDialog=false
buffer.deepIndent=false
buffer.encoding=UTF-8-Isabelle
buffer.indentSize=2
buffer.lineSeparator=\n
buffer.maxLineLen=100
buffer.noTabs=true
buffer.sidekick.keystroke-parse=false
buffer.tabSize=2
buffer.undoCount=1000
close-docking-area.shortcut2=C+e C+CIRCUMFLEX
complete-word.shortcut=
console.dock-position=floating
console.encoding=UTF-8
console.font=Isabelle DejaVu Sans Mono
console.fontsize=14
delete-line.shortcut=A+d
delete.shortcut2=C+d
""" + drop_encodings.map(a => "encoding.opt-out." + a + "=true").mkString("\n") + """
encodingDetectors=BOM XML-PI buffer-local-property
end.shortcut=
expand-abbrev.shortcut2=CA+SPACE
expand-folds.shortcut=
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
foldPainter=Circle
gatchan.highlight.overview=false
helpviewer.font=Isabelle DejaVu Serif
helpviewer.fontsize=12
home.shortcut=
hypersearch-results.dock-position=right
insert-newline-indent.shortcut=
insert-newline.shortcut=
isabelle-debugger.dock-position=floating
isabelle-documentation.dock-position=left
isabelle-export-browser.label=Browse theory exports
isabelle-output.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
isabelle-query.dock-position=bottom
isabelle-session-browser.label=Browse session information
isabelle-simplifier-trace.dock-position=floating
isabelle-sledgehammer.dock-position=bottom
isabelle-state.dock-position=right
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
isabelle.complete-word.label=Complete word
isabelle.complete.label=Complete Isabelle text
isabelle.complete.shortcut2=C+b
isabelle.control-bold.label=Control bold
isabelle.control-bold.shortcut=C+e RIGHT
isabelle.control-emph.label=Control emphasized
isabelle.control-emph.shortcut=C+e LEFT
isabelle.control-reset.label=Control reset
isabelle.control-reset.shortcut=C+e BACK_SPACE
isabelle.control-sub.label=Control subscript
isabelle.control-sub.shortcut=C+e DOWN
isabelle.control-sup.label=Control superscript
isabelle.control-sup.shortcut=C+e UP
isabelle.decrease-font-size.label=Decrease font size
isabelle.decrease-font-size.shortcut2=C+SUBTRACT
isabelle.decrease-font-size.shortcut=C+MINUS
isabelle.decrease-font-size2.label=Decrease font size (clone)
isabelle.draft.label=Show draft in browser
isabelle.exclude-word-permanently.label=Exclude word permanently
isabelle.exclude-word.label=Exclude word
isabelle.first-error.label=Go to first error
isabelle.first-error.shortcut=CS+a
isabelle.goto-entity.label=Go to definition of formal entity at caret
isabelle.goto-entity.shortcut=CS+d
isabelle.include-word-permanently.label=Include word permanently
isabelle.include-word.label=Include word
isabelle.increase-font-size.label=Increase font size
isabelle.increase-font-size.shortcut2=C+ADD
isabelle.increase-font-size.shortcut=C+PLUS
isabelle.increase-font-size2.label=Increase font size (clone)
isabelle.increase-font-size2.shortcut=C+EQUALS
isabelle.java-monitor.label=Java/VM monitor
isabelle.last-error.label=Go to last error
isabelle.last-error.shortcut=CS+z
isabelle.message.label=Show message
isabelle.message.shortcut=CS+m
isabelle.newline.label=Newline with indentation of Isabelle keywords
isabelle.newline.shortcut=ENTER
isabelle.next-error.label=Go to next error
isabelle.next-error.shortcut=CS+n
isabelle.options.label=Isabelle options
isabelle.prev-error.label=Go to previous error
isabelle.prev-error.shortcut=CS+p
isabelle.preview.label=Show preview in browser
isabelle.reset-continuous-checking.label=Reset continuous checking
isabelle.reset-font-size.label=Reset font size
isabelle.reset-node-required.label=Reset node required
isabelle.reset-words.label=Reset non-permanent words
isabelle.select-entity.label=Select all occurences of formal entity at caret
isabelle.select-entity.shortcut=CS+ENTER
isabelle.set-continuous-checking.label=Set continuous checking
isabelle.set-node-required.label=Set node required
isabelle.toggle-breakpoint.label=Toggle Breakpoint
isabelle.toggle-continuous-checking.label=Toggle continuous checking
isabelle.toggle-continuous-checking.shortcut=C+e ENTER
isabelle.toggle-node-required.label=Toggle node required
isabelle.toggle-node-required.shortcut=C+e SPACE
isabelle.tooltip.label=Show tooltip
isabelle.tooltip.shortcut=CS+b
isabelle.update-state.label=Update state output
isabelle.update-state.shortcut=S+ENTER
lang.usedefaultlocale=false
largefilemode=full
line-end.shortcut=END
line-home.shortcut=HOME
logo.icon.medium=32x32/apps/isabelle.gif
lookAndFeel=com.formdev.flatlaf.FlatLightLaf
match-bracket.shortcut2=C+9
metal.primary.font=Isabelle DejaVu Sans
metal.primary.fontsize=12
metal.secondary.font=Isabelle DejaVu Sans
metal.secondary.fontsize=12
navigator.showOnToolbar=true
new-file-in-mode.shortcut=
next-bracket.shortcut2=C+e C+9
options.shortcuts.deletekeymap.label=Delete
options.shortcuts.duplicatekeymap.dialog.title=Keymap name
options.shortcuts.duplicatekeymap.label=Duplicate
options.shortcuts.resetkeymap.dialog.title=Reset keymap
options.shortcuts.resetkeymap.label=Reset
options.textarea.lineSpacing=1
plugin-blacklist.MacOSX.jar=true
plugin.MacOSXPlugin.altDispatcher=false
plugin.MacOSXPlugin.disableOption=true
prev-bracket.shortcut2=C+e C+8
print.font=Isabelle DejaVu Sans Mono
print.glyphVector=true
recent-buffer.shortcut2=C+CIRCUMFLEX
restore.remote=false
restore=false
search.subdirs.toggle=true
select-block.shortcut2=C+8
sidekick-tree.dock-position=right
sidekick.auto-complete-popup-get-focus=true
sidekick.buffer-save-parse=true
sidekick.complete-delay=0
sidekick.complete-instant.toggle=false
sidekick.complete-popup.accept-characters=\\t
sidekick.complete-popup.insert-characters=
sidekick.persistentFilter=true
sidekick.showFilter=true
sidekick.splitter.location=721
systrayicon=false
tip.show=false
toggle-full-screen.shortcut2=S+F11
toggle-multi-select.shortcut2=C+NUMBER_SIGN
toggle-rect-select.shortcut2=A+NUMBER_SIGN
twoStageSave=false
vfs.browser.dock-position=left
vfs.favorite.0.type=1
vfs.favorite.0=$ISABELLE_HOME
vfs.favorite.1.type=1
vfs.favorite.1=$ISABELLE_HOME_USER
vfs.favorite.2.type=1
vfs.favorite.2=$JEDIT_HOME
vfs.favorite.3.type=1
vfs.favorite.3=$JEDIT_SETTINGS
vfs.favorite.4.type=1
vfs.favorite.4=isabelle-export:
vfs.favorite.5.type=1
vfs.favorite.5=isabelle-session:
view.antiAlias=subpixel HRGB
view.blockCaret=true
view.caretBlink=false
view.docking.framework=PIDE
view.eolMarkers=false
view.extendedState=0
view.font=Isabelle DejaVu Sans Mono
view.fontsize=18
view.fracFontMetrics=false
view.gutter.font=Isabelle DejaVu Sans Mono
view.gutter.fontsize=12
view.gutter.lineNumbers=false
view.gutter.selectionAreaWidth=18
view.height=850
view.middleMousePaste=true
view.showToolbar=true
view.status.memory.background=#666699
view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
view.thickCaret=true
view.width=1200
xml-insert-closing-tag.shortcut=
""")
val modes_dir = jedit_patched_dir + Path.basic("modes")
Mode.list.foreach(_.write(modes_dir))
File.change_lines(modes_dir + Path.basic("catalog")) { _.flatMap(line =>
if (line.containsSlice("FILE=\"ml.xml\"") ||
line.containsSlice("FILE_NAME_GLOB=\"*.{sml,ml}\"") ||
line.containsSlice("FILE_NAME_GLOB=\"*.ftl\"")) Nil
else if (line.containsSlice("NAME=\"jamon\"")) {
List(
"""""",
"",
"""""",
"",
"""""",
"",
"""""",
"",
"""""",
"",
line)
}
else if (line.containsSlice("NAME=\"sqr\"")) {
List(
"""""",
"",
line)
}
else List(line))
}
/* doc */
val doc_dir = jedit_patched_dir + Path.basic("doc")
download_jedit(doc_dir, "manual-a4.pdf", target_name = "jedit-manual.pdf")
Isabelle_System.copy_file(
doc_dir + Path.basic("CHANGES.txt"), doc_dir + Path.basic("jedit-changes"))
File.write(doc_dir + Path.basic("Contents"),
"""Original jEdit Documentation
jedit-manual jEdit User's Guide
jedit-changes jEdit Version History
""")
/* make patch */
File.write(component_path + Path.basic(jedit).patch,
Isabelle_System.make_patch(component_path, Path.basic(jedit), Path.basic(jedit_patched)))
if (!original) Isabelle_System.rm_tree(jedit_dir)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
JEDIT_HOME="$COMPONENT/""" + jedit_patched + """"
JEDIT_JARS=""" + quote(File.read_dir(jars_dir).map("$JEDIT_HOME/jars/" + _).mkString(":")) + """
JEDIT_JAR="$JEDIT_HOME/jedit.jar"
classpath "$JEDIT_JAR"
JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9"
JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4g -Xss16m"
JEDIT_JAVA_SYSTEM_OPTIONS="-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/doc"
""")
/* README */
File.write(component_dir.README,
"""This is a slightly patched version of jEdit """ + version + """ from
https://sourceforge.net/projects/jedit/files/jedit with some
additional plugins jars from
https://sourceforge.net/projects/jedit-plugins/files
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/** Isabelle tool wrappers **/
val default_version = "5.6.0"
def default_java_home: Path = Path.explode("$JAVA_HOME").expand
val isabelle_tool =
Isabelle_Tool("build_jedit", "build Isabelle component from the jEdit text-editor",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var java_home = default_java_home
var original = false
var version = default_version
val getopts = Getopts("""
Usage: isabelle build_jedit [OPTIONS]
Options are:
-D DIR target directory (default ".")
-J JAVA_HOME Java version for building jedit.jar (e.g. version 11)
-O retain copy of original jEdit directory
-V VERSION jEdit version (default: """ + quote(default_version) + """)
Build auxiliary jEdit component from original sources, with some patches.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"J:" -> (arg => java_home = Path.explode(arg)),
"O" -> (_ => original = true),
"V:" -> (arg => version = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val component_dir = target_dir + Path.basic("jedit-" + Date.Format.alt_date(Date.now()))
val progress = new Console_Progress()
build_jedit(component_dir, version, original = original,
java_home = java_home, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_lipics.scala b/src/Pure/Admin/build_lipics.scala
--- a/src/Pure/Admin/build_lipics.scala
+++ b/src/Pure/Admin/build_lipics.scala
@@ -1,112 +1,110 @@
/* Title: Pure/Admin/build_lipics.scala
Author: Makarius
Build Isabelle component for Dagstuhl LIPIcs style.
See also:
- https://github.com/dagstuhl-publishing/styles
- https://submission.dagstuhl.de/documentation/authors
- https://www.dagstuhl.de/en/publications/lipics
*/
package isabelle
object Build_LIPIcs {
/* files for document preparation */
val document_files: List[Path] =
for (name <- List("cc-by.pdf", "lipics-logo-bw.pdf", "lipics-v2021.cls"))
yield Path.explode("$ISABELLE_LIPICS_HOME/" + name)
/* build lipics component */
val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.2.tar.gz"
def build_lipics(
download_url: String = default_url,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
Isabelle_System.with_tmp_file("download", ext = "tar.gz") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
Isabelle_System.extract(download_file, download_dir, strip = true)
val lipics_dir = download_dir + Path.explode("LIPIcs/authors")
/* component */
val version = {
val Version = """^*.* v(.*)$""".r
val changelog = Path.explode("CHANGELOG.md")
split_lines(File.read(lipics_dir + changelog))
.collectFirst({ case Version(v) => v })
.getOrElse(error("Failed to detect version in " + changelog))
}
val component = "lipics-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
Isabelle_System.copy_dir(lipics_dir, component_dir.path)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_LIPICS_HOME="$COMPONENT/authors"
""")
/* README */
File.write(component_dir.README,
"""This is the Dagstuhl LIPIcs style for authors from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_lipics", "build component for Dagstuhl LIPIcs style",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_url
val getopts = Getopts("""
Usage: isabelle build_lipics [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
Build component for Dagstuhl LIPIcs style.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_lipics(download_url = download_url, target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_llncs.scala b/src/Pure/Admin/build_llncs.scala
--- a/src/Pure/Admin/build_llncs.scala
+++ b/src/Pure/Admin/build_llncs.scala
@@ -1,106 +1,104 @@
/* 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.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.extract(download_file, download_dir)
val llncs_dir = File.get_dir(download_dir, title = download_url)
/* component */
val README_md = Path.explode("README.md")
val version = {
val Version = """^_.* v(.*)_$""".r
split_lines(File.read(llncs_dir + README_md))
.collectFirst({ case Version(v) => v })
.getOrElse(error("Failed to detect version in " + README_md))
}
val component = "llncs-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
Isabelle_System.extract(download_file, component_dir.path, strip = true)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_LLNCS_HOME="$COMPONENT"
""")
/* README */
File.change(component_dir.path + README_md)(_.replace(" ", "\u00a0"))
File.write(component_dir.README,
"""This is the Springer LaTeX LNCS style for authors from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_llncs", "build component for Springer LaTeX LNCS style",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_url
val getopts = Getopts("""
Usage: isabelle build_llncs [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
Build component for Springer LaTeX LNCS style.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_llncs(download_url = download_url, target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_minisat.scala b/src/Pure/Admin/build_minisat.scala
--- a/src/Pure/Admin/build_minisat.scala
+++ b/src/Pure/Admin/build_minisat.scala
@@ -1,152 +1,150 @@
/* Title: Pure/Admin/build_minisat.scala
Author: Makarius
Build Isabelle Minisat from sources.
*/
package isabelle
object Build_Minisat {
val default_download_url = "https://github.com/stp/minisat/archive/releases/2.2.1.tar.gz"
def make_component_name(version: String): String = "minisat-" + version
/* build Minisat */
def build_minisat(
download_url: String = default_download_url,
component_name: String = "",
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
val Version = """^v?([0-9.]+)\.tar.gz$""".r
val archive_name =
download_url match {
case Archive_Name(name) => name
case _ => error("Failed to determine source archive name from " + quote(download_url))
}
val version =
archive_name match {
case Version(version) => version
case _ => error("Failed to determine component version from " + quote(archive_name))
}
val component = proper_string(component_name) getOrElse make_component_name(version)
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* platform */
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
val platform_dir =
Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building Minisat for " + platform_name + " ...")
Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
if (Platform.is_macos) {
File.change(source_dir + Path.explode("Makefile")) {
_.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "")
}
}
progress.bash("make r", source_dir.file, echo = verbose).check
Isabelle_System.copy_file(
source_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
if (Platform.is_windows) {
Isabelle_System.copy_file(Path.explode("/bin/cygwin1.dll"), platform_dir)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
MINISAT_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ISABELLE_MINISAT="$MINISAT_HOME/minisat"
""")
/* README */
File.write(component_dir.README,
"This Isabelle component provides Minisat " + version + """ using the
sources from """.stripMargin + download_url + """
The executables have been built via "make r"; macOS requires to
remove options "--static" and "-Wl,-soname,..." from the Makefile.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_minisat", "build prover component from sources", Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_download_url
var component_name = ""
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_minisat [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL
(default: """" + default_download_url + """")
-n NAME component name (default: """" + make_component_name("VERSION") + """")
-v verbose
Build prover component from official download.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg),
"n:" -> (arg => component_name = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_minisat(download_url = download_url, component_name = component_name,
verbose = verbose, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_pdfjs.scala b/src/Pure/Admin/build_pdfjs.scala
--- a/src/Pure/Admin/build_pdfjs.scala
+++ b/src/Pure/Admin/build_pdfjs.scala
@@ -1,98 +1,96 @@
/* 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 = {
/* component name */
val component = "pdfjs-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(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.extract(archive_file, component_dir.path)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
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_postgresql.scala b/src/Pure/Admin/build_postgresql.scala
--- a/src/Pure/Admin/build_postgresql.scala
+++ b/src/Pure/Admin/build_postgresql.scala
@@ -1,127 +1,125 @@
/* Title: Pure/Admin/build_postgresql.scala
Author: Makarius
Build Isabelle postgresql component from official download.
*/
package isabelle
object Build_PostgreSQL {
/* URLs */
val notable_urls =
List("https://jdbc.postgresql.org", "https://jdbc.postgresql.org/download.html")
val default_download_url = "https://jdbc.postgresql.org/download/postgresql-42.5.0.jar"
/* build postgresql */
def build_postgresql(
download_url: String = default_download_url,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
/* name and version */
def err(): Nothing = error("Malformed jar download URL: " + quote(download_url))
val Name = """^.*/([^/]+)\.jar""".r
val download_name = download_url match { case Name(name) => name case _ => err() }
val Version = """^.[^0-9]*([0-9].*)$""".r
val download_version = download_name match { case Version(version) => version case _ => err() }
/* component */
val component_dir =
Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress)
/* LICENSE */
File.write(component_dir.LICENSE,
"""Copyright (c) 1997, PostgreSQL Global Development Group
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
POSSIBILITY OF SUCH DAMAGE.
""")
/* README */
File.write(component_dir.README,
"""This is PostgreSQL JDBC """ + download_version + """ from
""" + notable_urls.mkString(" and ") + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
/* settings */
- File.write(component_dir.settings,
-"""# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
classpath "$COMPONENT/""" + download_name + """.jar"
""")
/* jar */
val jar = component_dir.path + Path.basic(download_name).ext("jar")
Isabelle_System.download_file(download_url, jar, progress = progress)
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_postgresql", "build Isabelle postgresql component from official download",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_download_url
val getopts = Getopts("""
Usage: isabelle build_postgresql [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL
(default: """" + default_download_url + """")
Build postgresql component from the specified download URL (JAR), see also
""" + notable_urls.mkString(" and "),
"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_postgresql(download_url, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_prismjs.scala b/src/Pure/Admin/build_prismjs.scala
--- a/src/Pure/Admin/build_prismjs.scala
+++ b/src/Pure/Admin/build_prismjs.scala
@@ -1,95 +1,93 @@
/* Title: Pure/Admin/build_prismjs.scala
Author: Makarius
Build Isabelle component for the Prism.js syntax highlighter.
See also:
- https://prismjs.com
- https://www.npmjs.com/package/prismjs
*/
package isabelle
object Build_Prismjs {
/* build prismjs component */
val default_version = "1.29.0"
def build_prismjs(
version: String = default_version,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("npm", test = "help")
/* component name */
val component = "prismjs-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* download */
Isabelle_System.with_tmp_dir("tmp") { tmp_dir =>
Isabelle_System.bash("npm init -y && npm install prismjs@" + Bash.string(version),
cwd = tmp_dir.file).check
Isabelle_System.rm_tree(component_dir.path)
Isabelle_System.copy_dir(tmp_dir + Path.explode("node_modules/prismjs"),
component_dir.path)
Isabelle_System.make_directory(component_dir.etc)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_PRISMJS_HOME="$COMPONENT"
""")
/* README */
File.write(component_dir.README,
"""This is Prism.js """ + version + """ from https://www.npmjs.com/package/prismjs
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_prismjs", "build component for prismjs",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var version = default_version
val getopts = Getopts("""
Usage: isabelle build_prismjs [OPTIONS]
Options are:
-D DIR target directory (default ".")
-V VERSION version (default: """" + default_version + """")
Build component for Prism.js.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"V:" -> (arg => version = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_prismjs(version = version, target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_scala.scala b/src/Pure/Admin/build_scala.scala
--- a/src/Pure/Admin/build_scala.scala
+++ b/src/Pure/Admin/build_scala.scala
@@ -1,169 +1,167 @@
/* Title: Pure/Admin/build_scala.scala
Author: Makarius
Build Isabelle Scala component from official downloads.
*/
package isabelle
object Build_Scala {
/* downloads */
sealed case class Download(
name: String,
version: String,
url: String,
physical_url: String = "",
base_version: String = "3"
) {
def make_url(template: String): String =
template.replace("{V}", version).replace("{B}", base_version)
def proper_url: String = make_url(proper_string(physical_url).getOrElse(url))
def artifact: String =
Library.take_suffix[Char](_ != '/', proper_url.toList)._2.mkString
def get(path: Path, progress: Progress = new Progress): Unit =
Isabelle_System.download_file(proper_url, path, progress = progress)
def print: String =
" * " + name + " " + version +
(if (base_version.nonEmpty) " for Scala " + base_version else "") +
":\n " + make_url(url)
}
val main_download: Download =
Download("scala", "3.2.1", base_version = "",
url = "https://github.com/lampepfl/dotty/releases/download/{V}/scala3-{V}.tar.gz")
val lib_downloads: List[Download] = List(
Download("scala-parallel-collections", "1.0.4",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parallel-collections_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parallel-collections_{B}/{V}/scala-parallel-collections_{B}-{V}.jar"),
Download("scala-parser-combinators", "2.1.1",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parser-combinators_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parser-combinators_{B}/{V}/scala-parser-combinators_{B}-{V}.jar"),
Download("scala-swing", "3.0.0",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-swing_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-swing_{B}/{V}/scala-swing_{B}-{V}.jar"),
Download("scala-xml", "2.1.0",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-xml_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-xml_{B}/{V}/scala-xml_{B}-{V}.jar")
)
/* build Scala component */
def build_scala(
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
/* component */
val component_name = main_download.name + "-" + main_download.version
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* download */
Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path =>
main_download.get(archive_path, progress = progress)
Isabelle_System.extract(archive_path, component_dir.path, strip = true)
}
lib_downloads.foreach(download =>
download.get(component_dir.lib + Path.basic(download.artifact), progress = progress))
File.write(component_dir.LICENSE,
Url.read(Url("https://www.apache.org/licenses/LICENSE-2.0.txt")))
/* classpath */
val classpath: List[String] = {
def no_function(name: String): String = "function " + name + "() {\n:\n}"
val script =
cat_lines(List(
no_function("stty"),
no_function("tput"),
"PROG_HOME=" + File.bash_path(component_dir.path),
File.read(component_dir.path + Path.explode("bin/common"))
.replace("scala_exit_status=127", "scala_exit_status=0"),
"compilerJavaClasspathArgs",
"echo \"$jvm_cp_args\""))
val main_classpath = Path.split(Isabelle_System.bash(script).check.out).map(_.file_name)
val lib_classpath = lib_downloads.map(_.artifact)
main_classpath ::: lib_classpath
}
val interfaces =
classpath.find(_.startsWith("scala3-interfaces"))
.getOrElse(error("Missing jar for scala3-interfaces"))
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
SCALA_HOME="$COMPONENT"
SCALA_INTERFACES="$SCALA_HOME/lib/""" + interfaces + """"
""" + terminate_lines(classpath.map(jar => "classpath \"$SCALA_HOME/lib/" + jar + "\"")))
/* adhoc changes */
val patched_scripts = List("bin/scala", "bin/scalac")
for (name <- patched_scripts) {
File.change(component_dir.path + Path.explode(name)) {
_.replace(""""-Dscala.home=$PROG_HOME"""", """"-Dscala.home=\"$PROG_HOME\""""")
}
}
/* README */
File.write(component_dir.README,
"This distribution of Scala integrates the following parts:\n\n" +
(main_download :: lib_downloads).map(_.print).mkString("\n\n") + """
Minor changes to """ + patched_scripts.mkString(" and ") + """ allow an installation location
with spaces in the directory name.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_scala", "build Isabelle Scala component from official downloads",
Scala_Project.here,
{ args =>
var target_dir = Path.current
val getopts = Getopts("""
Usage: isabelle build_scala [OPTIONS]
Options are:
-D DIR target directory (default ".")
Build Isabelle Scala component from official downloads.
""",
"D:" -> (arg => target_dir = Path.explode(arg)))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_scala(target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_spass.scala b/src/Pure/Admin/build_spass.scala
--- a/src/Pure/Admin/build_spass.scala
+++ b/src/Pure/Admin/build_spass.scala
@@ -1,175 +1,174 @@
/* Title: Pure/Admin/build_spass.scala
Author: Makarius
Build Isabelle SPASS component from unofficial download.
*/
package isabelle
object Build_SPASS {
/* build SPASS */
val default_download_url = "https://www.cs.vu.nl/~jbe248/spass-3.8ds-src.tar.gz"
val standard_version = "3.8ds"
def build_spass(
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current): Unit = {
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
Isabelle_System.require_command("bison")
Isabelle_System.require_command("flex")
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
val Component_Name = """^(.+)-src\.tar.gz$""".r
val Version = """^[^-]+-([^-]+)$""".r
val archive_name =
download_url match {
case Archive_Name(name) => name
case _ => error("Failed to determine source archive name from " + quote(download_url))
}
val component_name =
archive_name match {
case Component_Name(name) => name
case _ => error("Failed to determine component name from " + quote(archive_name))
}
val version =
component_name match {
case Version(version) => version
case _ => error("Failed to determine component version from " + quote(component_name))
}
if (version != standard_version) {
progress.echo_warning("Odd SPASS version " + version + " (expected " + standard_version + ")")
}
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
.getOrElse(error("No 64bit platform"))
val platform_dir =
Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building SPASS for " + platform_name + " ...")
if (Platform.is_windows) {
File.change(source_dir + Path.basic("misc.c")) {
_.replace("""#include "execinfo.h" """, "")
.replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }")
}
}
Isabelle_System.bash("make", cwd = source_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
Isabelle_System.copy_file(source_dir + Path.basic("LICENCE"), component_dir.LICENSE)
val install_files = List("SPASS")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
val path = source_dir + Path.basic(name)
if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
SPASS_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
SPASS_VERSION=""" + quote(version) + """
""")
+
/* README */
File.write(component_dir.README,
"""This distribution of SPASS 3.8ds, described in Blanchette, Popescu, Wand, and
Weidenbach's ITP 2012 paper "More SPASS with Isabelle", has been compiled from
sources available at """ + download_url + """
via "make".
The Windows/Cygwin compilation required commenting out the line
#include "execinfo.h"
in "misc.c" as well as most of the body of the "misc_DumpCore" function.
The latest official SPASS sources can be downloaded from
http://www.spass-prover.org/. Be aware, however, that the official SPASS
releases are not compatible with Isabelle.
Viel SPASS!
Jasmin Blanchette
16-May-2018
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_spass", "build prover component from source distribution",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_download_url
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_spass [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL
(default: """" + default_download_url + """")
-v verbose
Build prover component from the specified source distribution.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_spass(download_url = download_url, verbose = verbose, progress = progress,
target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_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,111 @@
/* Title: Pure/Admin/build_sqlite.scala
Author: Makarius
Build Isabelle sqlite-jdbc component from official download.
*/
package isabelle
object Build_SQLite {
/* build sqlite */
val default_download_url =
"https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.39.4.1/sqlite-jdbc-3.39.4.1.jar"
def build_sqlite(
download_url: String = default_download_url,
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 =
Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress)
/* README */
File.write(component_dir.README,
"This is " + download_name + " from\n" + download_url +
"\n\n Makarius\n " + Date.Format.date(Date.now()) + "\n")
/* settings */
- File.write(component_dir.settings,
-"""# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_SQLITE_HOME="$COMPONENT"
classpath "$ISABELLE_SQLITE_HOME/lib/""" + download_name + """.jar"
""")
/* jar */
val jar = component_dir.lib + Path.basic(download_name).ext("jar")
Isabelle_System.make_directory(jar.dir)
Isabelle_System.download_file(download_url, jar, progress = progress)
Isabelle_System.with_tmp_dir("build") { jar_dir =>
Isabelle_System.extract(jar, jar_dir)
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 + Path.explode(dir))
Isabelle_System.copy_file(jar_dir + Path.explode(file), target)
}
File.set_executable(component_dir.path + 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
var download_url = default_download_url
val getopts = Getopts("""
Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD
Options are:
-D DIR target directory (default ".")
-U URL download URL
(default: """" + default_download_url + """")
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)),
"U:" -> (arg => download_url = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_sqlite(download_url = download_url, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_vampire.scala b/src/Pure/Admin/build_vampire.scala
--- a/src/Pure/Admin/build_vampire.scala
+++ b/src/Pure/Admin/build_vampire.scala
@@ -1,161 +1,159 @@
/* Title: Pure/Admin/build_vampire.scala
Author: Makarius
Build Isabelle Vampire component from official download.
*/
package isabelle
object Build_Vampire {
val default_download_url = "https://github.com/vprover/vampire/archive/refs/tags/v4.6.tar.gz"
val default_jobs = 1
def make_component_name(version: String): String =
"vampire-" + Library.try_unprefix("v", version).getOrElse(version)
/* build Vampire */
def build_vampire(
download_url: String = default_download_url,
jobs: Int = default_jobs,
component_name: String = "",
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
Isabelle_System.require_command("cmake")
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
val Version = """^v?([0-9.]+)\.tar.gz$""".r
val archive_name =
download_url match {
case Archive_Name(name) => name
case _ => error("Failed to determine source archive name from " + quote(download_url))
}
val version =
archive_name match {
case Version(version) => version
case _ => error("Failed to determine component version from " + quote(archive_name))
}
val component = proper_string(component_name) getOrElse make_component_name(version)
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* platform */
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
val platform_dir =
Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building Vampire for " + platform_name + " ...")
Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir.path)
val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
val cmake_out =
progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""",
cwd = source_dir.file, echo = verbose).check.out
val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
val binary =
split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
.getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
progress.bash("make -j" + jobs, cwd = source_dir.file, echo = verbose).check
Isabelle_System.copy_file(source_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
platform_dir + Path.basic("vampire").platform_exe)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire"
""")
/* README */
File.write(component_dir.README,
"This Isabelle component provides Vampire " + version + """using the
original sources from """.stripMargin + download_url + """
The executables have been built via "cmake . && make"
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_vampire", "build prover component from official download",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_download_url
var jobs = default_jobs
var component_name = ""
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_vampire [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL
(default: """" + default_download_url + """")
-j NUMBER parallel jobs for make (default: """ + default_jobs + """)
-n NAME component name (default: """" + make_component_name("VERSION") + """")
-v verbose
Build prover component from official download.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg),
"j:" -> (arg => jobs = Value.Nat.parse(arg)),
"n:" -> (arg => component_name = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_vampire(download_url = download_url, component_name = component_name,
jobs = jobs, verbose = verbose, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_verit.scala b/src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala
+++ b/src/Pure/Admin/build_verit.scala
@@ -1,154 +1,152 @@
/* Title: Pure/Admin/build_csdp.scala
Author: Makarius
Build Isabelle veriT component from official download.
*/
package isabelle
object Build_VeriT {
val default_download_url = "https://verit.loria.fr/rmx/2021.06.2/verit-2021.06.2-rmx.tar.gz"
/* build veriT */
def build_verit(
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current,
mingw: MinGW = MinGW.none
): Unit = {
mingw.check
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
val Version = """^[^-]+-(.+)\.tar.gz$""".r
val archive_name =
download_url match {
case Archive_Name(name) => name
case _ => error("Failed to determine source archive name from " + quote(download_url))
}
val version =
archive_name match {
case Version(version) => version
case _ => error("Failed to determine component version from " + quote(archive_name))
}
val component_name = "verit-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* platform */
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
val platform_dir =
Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building veriT for " + platform_name + " ...")
val configure_options =
if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else ""
progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"),
cwd = source_dir.file, echo = verbose).check
/* install */
Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
val exe_path = Path.basic("veriT").platform_exe
Isabelle_System.copy_file(source_dir + exe_path, platform_dir)
Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_VERIT="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/veriT"
""")
/* README */
File.write(component_dir.README,
"""This is veriT """ + version + """ from
""" + download_url + """
It has been built from sources like this:
cd src
./configure
make
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_verit", "build prover component from official download",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var mingw = MinGW.none
var download_url = default_download_url
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_verit [OPTIONS]
Options are:
-D DIR target directory (default ".")
-M DIR msys/mingw root specification for Windows
-U URL download URL
(default: """" + default_download_url + """")
-v verbose
Build prover component from official download.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"M:" -> (arg => mingw = MinGW(Path.explode(arg))),
"U:" -> (arg => download_url = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_verit(download_url = download_url, verbose = verbose, progress = progress,
target_dir = target_dir, mingw = mingw)
})
}
diff --git a/src/Pure/Admin/build_zipperposition.scala b/src/Pure/Admin/build_zipperposition.scala
--- a/src/Pure/Admin/build_zipperposition.scala
+++ b/src/Pure/Admin/build_zipperposition.scala
@@ -1,122 +1,120 @@
/* Title: Pure/Admin/build_zipperposition.scala
Author: Makarius
Build Isabelle Zipperposition component from OPAM repository.
*/
package isabelle
object Build_Zipperposition {
val default_version = "2.1"
/* build Zipperposition */
def build_zipperposition(
version: String = default_version,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
Isabelle_System.with_tmp_dir("build") { build_dir =>
if (Platform.is_linux) Isabelle_System.require_command("patchelf")
/* component */
val component_name = "zipperposition-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* platform */
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
val platform_dir =
Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* build */
progress.echo("OCaml/OPAM setup ...")
progress.bash("isabelle ocaml_setup", echo = verbose).check
progress.echo("Building Zipperposition for " + platform_name + " ...")
progress.bash(cwd = build_dir.file, echo = verbose,
script = "isabelle_opam install -y --destdir=" + File.bash_path(build_dir) +
" zipperposition=" + Bash.string(version)).check
/* install */
Isabelle_System.copy_file(build_dir + Path.explode("doc/zipperposition/LICENSE"),
component_dir.path)
val prg_path = Path.basic("zipperposition")
val exe_path = prg_path.platform_exe
Isabelle_System.copy_file(build_dir + Path.basic("bin") + prg_path, platform_dir + exe_path)
if (!Platform.is_windows) {
Executable.libraries_closure(
platform_dir + exe_path, filter = Set("libgmp"), patchelf = true)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ZIPPERPOSITION_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
""")
/* README */
File.write(component_dir.README,
"""This is Zipperposition """ + version + """ from the OCaml/OPAM repository.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_zipperposition", "build prover component from OPAM repository",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var version = default_version
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_zipperposition [OPTIONS]
Options are:
-D DIR target directory (default ".")
-V VERSION version (default: """" + default_version + """")
-v verbose
Build prover component from OPAM repository.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"V:" -> (arg => version = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_zipperposition(version = version, verbose = verbose, progress = progress,
target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_zstd.scala b/src/Pure/Admin/build_zstd.scala
--- a/src/Pure/Admin/build_zstd.scala
+++ b/src/Pure/Admin/build_zstd.scala
@@ -1,114 +1,112 @@
/* Title: Pure/Admin/build_zstd.scala
Author: Makarius
Build Isabelle zstd-jni component from official download.
*/
package isabelle
object Build_Zstd {
/* platforms */
sealed case class Platform_Info(name: String, template: String, exe: Boolean = false) {
def install(jar_dir: Path, component_dir: Path, version: String): Unit = {
val source = jar_dir + Path.explode(template.replace("{V}", version))
val target = Isabelle_System.make_directory(component_dir + Path.basic(name))
Isabelle_System.copy_file(source, target)
if (exe) File.set_executable(target + source.base, true)
}
}
private val platforms =
List(
Platform_Info("arm64-darwin", "darwin/aarch64/libzstd-jni-{V}.dylib"),
Platform_Info("x86_64-darwin", "darwin/x86_64/libzstd-jni-{V}.dylib"),
Platform_Info("arm64-linux", "linux/aarch64/libzstd-jni-{V}.so"),
Platform_Info("x86_64-linux", "linux/amd64/libzstd-jni-{V}.so"),
Platform_Info("x86_64-windows", "win/amd64/libzstd-jni-{V}.dll", exe = true))
/* build zstd */
val license_url = "https://raw.githubusercontent.com/luben/zstd-jni/master/LICENSE"
val default_download_url = "https://repo1.maven.org/maven2/com/github/luben/zstd-jni"
val default_version = "1.5.2-5"
def build_zstd(
target_dir: Path = Path.current,
download_url: String = default_download_url,
version: String = default_version,
progress: Progress = new Progress,
): Unit = {
/* component */
val component_name = "zstd-jni-" + version
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
File.write(component_dir.README,
"This is " + component_name + " from\n" + download_url +
"\n\n Makarius\n " + Date.Format.date(Date.now()) + "\n")
Isabelle_System.download_file(license_url, component_dir.LICENSE, progress = progress)
/* jar */
val jar_name = component_name + ".jar"
val jar = component_dir.path + Path.basic(jar_name)
Isabelle_System.download_file(
download_url + "/" + version + "/" + jar_name, jar, progress = progress)
Isabelle_System.with_tmp_dir("build") { jar_dir =>
Isabelle_System.extract(jar, jar_dir)
for (platform <- platforms) platform.install(jar_dir, component_dir.path, version)
}
/* settings */
- File.write(component_dir.settings,
-"""# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_ZSTD_HOME="$COMPONENT"
classpath "$ISABELLE_ZSTD_HOME/""" + jar_name + """"
""")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_zstd", "build Isabelle zstd-jni component from official download",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_download_url
var version = default_version
val getopts = Getopts("""
Usage: isabelle build_zstd [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """ + quote(default_download_url) + """)
-V VERSION version (default: """ + quote(default_version) + """)
Build zstd-jni component from the specified download base URL and VERSION,
see also https://github.com/luben/zstd-jni
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg),
"V:" -> (arg => version = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_zstd(target_dir = target_dir, download_url = download_url,
version = version, progress = progress)
})
}
diff --git a/src/Pure/System/components.scala b/src/Pure/System/components.scala
--- a/src/Pure/System/components.scala
+++ b/src/Pure/System/components.scala
@@ -1,370 +1,373 @@
/* Title: Pure/System/components.scala
Author: Makarius
Isabelle system components.
*/
package isabelle
import java.io.{File => JFile}
object Components {
/* archive name */
object Archive {
val suffix: String = ".tar.gz"
def apply(name: String): String =
if (name == "") error("Bad component name: " + quote(name))
else name + suffix
def unapply(archive: String): Option[String] = {
for {
name0 <- Library.try_unsuffix(suffix, archive)
name <- proper_string(name0)
} yield name
}
def get_name(archive: String): String =
unapply(archive) getOrElse
error("Bad component archive name (expecting .tar.gz): " + quote(archive))
}
/* component collections */
def default_component_repository: String =
Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
def admin(dir: Path): Path = dir + Path.explode("Admin/components")
def contrib(dir: Path = Path.current, name: String = ""): Path =
dir + Path.explode("contrib") + Path.explode(name)
def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = {
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
Isabelle_System.extract(archive, dir)
name
}
def resolve(base_dir: Path, names: List[String],
target_dir: Option[Path] = None,
copy_dir: Option[Path] = None,
progress: Progress = new Progress
): Unit = {
Isabelle_System.make_directory(base_dir)
for (name <- names) {
val archive_name = Archive(name)
val archive = base_dir + Path.explode(archive_name)
if (!archive.is_file) {
val remote = Components.default_component_repository + "/" + archive_name
Isabelle_System.download_file(remote, archive, progress = progress)
}
for (dir <- copy_dir) {
Isabelle_System.make_directory(dir)
Isabelle_System.copy_file(archive, dir)
}
unpack(target_dir getOrElse base_dir, archive, progress = progress)
}
}
private val platforms_family: Map[Platform.Family.Value, Set[String]] =
Map(
Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"),
Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"),
Platform.Family.macos ->
Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"),
Platform.Family.windows ->
Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows"))
private val platforms_all: Set[String] =
Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2)
def purge(dir: Path, platform: Platform.Family.Value): Unit = {
val purge_set = platforms_all -- platforms_family(platform)
File.find_files(dir.file,
(file: JFile) => file.isDirectory && purge_set(file.getName),
include_dirs = true).foreach(Isabelle_System.rm_tree)
}
/* component directories */
def directories(): List[Path] =
Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS"))
/* component directory content */
object Directory {
def apply(path: Path): Directory = new Directory(path.absolute)
}
class Directory private(val path: Path) {
override def toString: String = path.toString
def etc: Path = path + Path.basic("etc")
def src: Path = path + Path.basic("src")
def lib: Path = path + Path.basic("lib")
def settings: Path = etc + Path.basic("settings")
def components: Path = etc + Path.basic("components")
def build_props: Path = etc + Path.basic("build.props")
def README: Path = path + Path.basic("README")
def LICENSE: Path = path + Path.basic("LICENSE")
def create(progress: Progress = new Progress): Directory = {
progress.echo("Creating component directory " + path)
Isabelle_System.new_directory(path)
Isabelle_System.make_directory(etc)
this
}
def check: Boolean = settings.is_file || components.is_file
def read_components(): List[String] =
split_lines(File.read(components)).filter(_.nonEmpty)
def write_components(lines: List[String]): Unit =
File.write(components, terminate_lines(lines))
+
+ def write_settings(text: String): Unit =
+ File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text)
}
/* component repository content */
val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) {
override def toString: String = digest.shasum(name)
}
def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
(proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
Word.explode(line) match {
case Nil => None
case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name))
case _ => error("Bad components.sha1 entry: " + quote(line))
})
def write_components_sha1(entries: List[SHA1_Digest]): Unit =
File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n"))
/** manage user components **/
val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components")
def read_components(): List[String] =
if (components_path.is_file) Library.trim_split_lines(File.read(components_path))
else Nil
def write_components(lines: List[String]): Unit = {
Isabelle_System.make_directory(components_path.dir)
File.write(components_path, Library.terminate_lines(lines))
}
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
val path = path0.expand.absolute
if (!Directory(path).check && !Sessions.is_session_dir(path)) {
error("Bad component directory: " + path)
}
val lines1 = read_components()
val lines2 =
lines1.filter(line =>
line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path))
val lines3 = if (add) lines2 ::: List(path.implode) else lines2
if (lines1 != lines3) write_components(lines3)
val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed"
progress.echo(prefix + " component " + path)
}
/* main entry point */
def main(args: Array[String]): Unit = {
Command_Line.tool {
for (arg <- args) {
val add =
if (arg.startsWith("+")) true
else if (arg.startsWith("-")) false
else error("Bad argument: " + quote(arg))
val path = Path.explode(arg.substring(1))
update_components(add, path, progress = new Console_Progress)
}
}
}
/** build and publish components **/
def build_components(
options: Options,
components: List[Path],
progress: Progress = new Progress,
publish: Boolean = false,
force: Boolean = false,
update_components_sha1: Boolean = false
): Unit = {
val archives: List[Path] =
for (path <- components) yield {
path.file_name match {
case Archive(_) => path
case name =>
if (!path.is_dir) error("Bad component directory: " + path)
else if (!Directory(path).check) {
error("Malformed component directory: " + path +
"\n (requires etc/settings or etc/components)")
}
else {
val component_path = path.expand
val archive_dir = component_path.dir
val archive_name = Archive(name)
val archive = archive_dir + Path.explode(archive_name)
if (archive.is_file && !force) {
error("Component archive already exists: " + archive)
}
progress.echo("Packaging " + archive_name)
Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
dir = archive_dir).check
archive
}
}
}
if ((publish && archives.nonEmpty) || update_components_sha1) {
val server = options.string("isabelle_components_server")
if (server.isEmpty) error("Undefined option isabelle_components_server")
using(SSH.open_session(options, server)) { ssh =>
val components_dir = Path.explode(options.string("isabelle_components_dir"))
val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
error("Bad remote directory: " + dir)
}
if (publish) {
for (archive <- archives) {
val archive_name = archive.file_name
val name = Archive.get_name(archive_name)
val remote_component = components_dir + archive.base
val remote_contrib = contrib_dir + Path.explode(name)
// component archive
if (ssh.is_file(remote_component) && !force) {
error("Remote component archive already exists: " + remote_component)
}
progress.echo("Uploading " + archive_name)
ssh.write_file(remote_component, archive)
// contrib directory
val is_standard_component =
Isabelle_System.with_tmp_dir("component") { tmp_dir =>
Isabelle_System.extract(archive, tmp_dir)
Directory(tmp_dir + Path.explode(name)).check
}
if (is_standard_component) {
if (ssh.is_dir(remote_contrib)) {
if (force) ssh.rm_tree(remote_contrib)
else error("Remote component directory already exists: " + remote_contrib)
}
progress.echo("Unpacking remote " + archive_name)
ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " +
ssh.bash_path(remote_component)).check
}
else {
progress.echo_warning("No unpacking of non-standard component: " + archive_name)
}
}
}
// remote SHA1 digests
if (update_components_sha1) {
val lines =
for {
entry <- ssh.read_dir(components_dir)
if ssh.is_file(components_dir + Path.basic(entry)) &&
entry.endsWith(Archive.suffix)
}
yield {
progress.echo("Digesting remote " + entry)
ssh.execute("cd " + ssh.bash_path(components_dir) +
"; sha1sum " + Bash.string(entry)).check.out
}
write_components_sha1(read_components_sha1(lines))
}
}
}
// local SHA1 digests
{
val new_entries =
for (archive <- archives)
yield {
val name = archive.file_name
progress.echo("Digesting local " + name)
SHA1_Digest(SHA1.digest(archive), name)
}
val new_names = new_entries.map(_.name).toSet
write_components_sha1(
new_entries :::
read_components_sha1().filterNot(entry => new_names.contains(entry.name)))
}
}
/* Isabelle tool wrapper */
private val relevant_options =
List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir")
val isabelle_tool =
Isabelle_Tool("build_components", "build and publish Isabelle components",
Scala_Project.here,
{ args =>
var publish = false
var update_components_sha1 = false
var force = false
var options = Options.init()
def show_options: String =
cat_lines(relevant_options.flatMap(options.get).map(_.print))
val getopts = Getopts("""
Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
Options are:
-P publish on SSH server (see options below)
-f force: overwrite existing component archives and directories
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-u update all SHA1 keys in Isabelle repository Admin/components
Build and publish Isabelle components as .tar.gz archives on SSH server,
depending on system options:
""" + Library.indent_lines(2, show_options) + "\n",
"P" -> (_ => publish = true),
"f" -> (_ => force = true),
"o:" -> (arg => options = options + arg),
"u" -> (_ => update_components_sha1 = true))
val more_args = getopts(args)
if (more_args.isEmpty && !update_components_sha1) getopts.usage()
val progress = new Console_Progress
build_components(options, more_args.map(Path.explode), progress = progress,
publish = publish, force = force, update_components_sha1 = update_components_sha1)
})
}
diff --git a/src/Pure/Tools/dotnet_setup.scala b/src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala
+++ b/src/Pure/Tools/dotnet_setup.scala
@@ -1,203 +1,202 @@
/* Title: Pure/Tools/dotnet_setup.scala
Author: Makarius
Dynamic setup of dotnet component.
*/
package isabelle
object Dotnet_Setup {
/* platforms */
sealed case class Platform_Info(
family: Platform.Family.Value,
name: String,
os: String = "",
arch: String = "x64",
ext: String = "sh",
exec: String = "bash",
check: () => Unit = () => ())
val all_platforms =
List(
Platform_Info(Platform.Family.linux_arm, "arm64-linux", os = "linux", arch = "arm64"),
Platform_Info(Platform.Family.linux, "x86_64-linux", os = "linux"),
Platform_Info(Platform.Family.macos, "arm64-darwin", os = "osx", arch = "arm64"),
Platform_Info(Platform.Family.macos, "x86_64-darwin", os = "osx"),
Platform_Info(Platform.Family.windows, "x86_64-windows",
ext = "ps1",
exec = "powershell -ExecutionPolicy ByPass",
check = () => Isabelle_System.require_command("powershell", "-NoProfile -Command Out-Null")))
def check_platform_spec(spec: String): String = {
val all_specs =
Library.distinct(all_platforms.map(_.family.toString) ::: all_platforms.map(_.name))
if (all_specs.contains(spec)) spec
else {
error("Bad platform specification " + quote(spec) +
"\n expected " + commas_quote(all_specs))
}
}
/* dotnet download and setup */
def default_platform: String = {
val self = Isabelle_Platform.self
proper_string(self.ISABELLE_WINDOWS_PLATFORM64).getOrElse(
proper_string(self.ISABELLE_APPLE_PLATFORM64).getOrElse(
self.ISABELLE_PLATFORM64))
}
def default_target_dir: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
def default_install_url: String = "https://dot.net/v1/dotnet-install"
def default_version: String = "6.0.402"
def dotnet_setup(
platform_spec: String = default_platform,
target_dir: Path = default_target_dir,
install_url: String = default_install_url,
version: String = default_version,
force: Boolean = false,
dry_run: Boolean = false,
verbose: Boolean = false,
progress: Progress = new Progress
): Unit = {
check_platform_spec(platform_spec)
for {
platform <- all_platforms
if platform.family.toString == platform_spec || platform.name == platform_spec
} {
progress.expose_interrupt()
/* component directory */
val component_dir =
Components.Directory(
target_dir + Path.explode(if (version.isEmpty) "dotnet-latest" else "dotnet-" + version))
if (!dry_run) {
progress.echo("Component " + component_dir)
Isabelle_System.make_directory(component_dir.etc)
- File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_DOTNET_ROOT="$COMPONENT"
if [ -n "$ISABELLE_WINDOWS_PLATFORM64" -a -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_WINDOWS_PLATFORM64" ]; then
ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_WINDOWS_PLATFORM64/dotnet.exe"
elif [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_APPLE_PLATFORM64" ]; then
ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_APPLE_PLATFORM64/dotnet"
elif [ -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_PLATFORM64" ]; then
ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_PLATFORM64/dotnet"
fi
DOTNET_CLI_TELEMETRY_OPTOUT="true"
DOTNET_CLI_HOME="$(platform_path "$ISABELLE_HOME_USER/dotnet")"
""")
File.write(component_dir.README,
"""This installation of Dotnet has been produced via "isabelle dotnet_setup".
Makarius
""" + Date.Format.date(Date.now()) + "\n")
for (old <- proper_string(Isabelle_System.getenv("ISABELLE_DOTNET_ROOT"))) {
Components.update_components(false, Path.explode(old))
}
Components.update_components(true, component_dir.path)
}
/* platform directory */
Isabelle_System.with_tmp_file("install", ext = platform.ext) { install =>
Isabelle_System.download_file(install_url + "." + platform.ext, install)
val platform_dir = component_dir.path + Path.explode(platform.name)
if (platform_dir.is_dir && !force) {
progress.echo_warning("Platform " + platform.name + " already installed")
}
else {
progress.echo("Platform " + platform.name + " ...")
platform.check()
if (platform_dir.is_dir && force) Isabelle_System.rm_tree(platform_dir)
val script =
platform.exec + " " + File.bash_platform_path(install) +
(if (version.nonEmpty) " -Version " + Bash.string(version) else "") +
" -Architecture " + Bash.string(platform.arch) +
(if (platform.os.nonEmpty) " -OS " + Bash.string(platform.os) else "") +
" -InstallDir " + Bash.string(platform.name) +
(if (dry_run) " -DryRun" else "") +
" -NoPath"
progress.bash(script, echo = verbose,
cwd = if (dry_run) null else component_dir.path.file).check
for (exe <- File.find_files(platform_dir.file, pred = _.getName.endsWith(".exe"))) {
File.set_executable(File.path(exe), true)
}
}
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("dotnet_setup", "dynamic setup of dotnet component (for Fsharp)",
Scala_Project.here,
{ args =>
var target_dir = default_target_dir
var install_url = default_install_url
var version = default_version
var force = false
var dry_run = false
var platforms = List(default_platform)
var verbose = false
val getopts = Getopts("""
Usage: isabelle dotnet_setup [OPTIONS]
Options are:
-D DIR target directory (default: """ + default_target_dir.expand + """)
-I URL URL for install script without extension
(default: """ + quote(default_install_url) + """)
-V VERSION version (empty means "latest", default: """ + quote(default_version) + """)
-f force fresh installation of specified platforms
-n dry run: try download without installation
-p PLATFORMS comma-separated list of platform specifications,
as family or formal name (default: """ + quote(default_platform) + """)
-v verbose
Download the Dotnet / Fsharp platform and configure it as Isabelle component.
See also:
https://fsharp.org
https://learn.microsoft.com/en-us/dotnet/core/tools/dotnet-install-script
https://learn.microsoft.com/en-us/dotnet/core/tools/telemetry
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"I:" -> (arg => install_url = arg),
"V:" -> (arg => version = arg),
"f" -> (_ => force = true),
"n" -> (_ => dry_run = true),
"p:" -> (arg => platforms = Library.space_explode(',', arg).map(check_platform_spec)),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
for (platform <- platforms) {
dotnet_setup(platform_spec = platform, target_dir = target_dir, install_url = install_url,
version = version, force = force, dry_run = dry_run, verbose = verbose, progress = progress)
}
})
}
diff --git a/src/Tools/VSCode/src/build_vscode_extension.scala b/src/Tools/VSCode/src/build_vscode_extension.scala
--- a/src/Tools/VSCode/src/build_vscode_extension.scala
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala
@@ -1,246 +1,244 @@
/* Title: Tools/VSCode/src/build_vscode_extension.scala
Author: Makarius
Build the Isabelle/VSCode extension as component.
*/
package isabelle.vscode
import isabelle._
object Build_VSCode {
/* build grammar */
def default_logic: String = Isabelle_System.getenv("ISABELLE_LOGIC")
def build_grammar(options: Options, build_dir: Path,
logic: String = default_logic,
dirs: List[Path] = Nil,
progress: Progress = new Progress
): Unit = {
val keywords =
Sessions.base_info(options, logic, dirs = dirs).check_errors.base.overall_syntax.keywords
val output_path = build_dir + Path.explode("isabelle-grammar.json")
progress.echo(output_path.expand.implode)
val (minor_keywords, operators) =
keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier)
def major_keywords(pred: String => Boolean): List[String] =
(for {
k <- keywords.major.iterator
kind <- keywords.kinds.get(k)
if pred(kind)
} yield k).toList
val keywords1 =
major_keywords(k => k != Keyword.THY_END && k != Keyword.PRF_ASM && k != Keyword.PRF_ASM_GOAL)
val keywords2 = minor_keywords ::: major_keywords(Set(Keyword.THY_END))
val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL))
def grouped_names(as: List[String]): String =
JSON.Format("\\b(" + as.sorted.map(Library.escape_regex).mkString("|") + ")\\b")
File.write_backup(output_path, """{
"name": "Isabelle",
"scopeName": "source.isabelle",
"fileTypes": ["thy"],
"uuid": """ + JSON.Format(UUID.random().toString) + """,
"repository": {
"comment": {
"patterns": [
{
"name": "comment.block.isabelle",
"begin": "\\(\\*",
"patterns": [{ "include": "#comment" }],
"end": "\\*\\)"
}
]
},
"cartouche": {
"patterns": [
{
"name": "string.quoted.other.multiline.isabelle",
"begin": "(?:\\\\|‹)",
"patterns": [{ "include": "#cartouche" }],
"end": "(?:\\\\|›)"
}
]
}
},
"patterns": [
{
"include": "#comment"
},
{
"include": "#cartouche"
},
{
"name": "keyword.control.isabelle",
"match": """ + grouped_names(keywords1) + """
},
{
"name": "keyword.other.unit.isabelle",
"match": """ + grouped_names(keywords2) + """
},
{
"name": "keyword.operator.isabelle",
"match": """ + grouped_names(operators) + """
},
{
"name": "entity.name.type.isabelle",
"match": """ + grouped_names(keywords3) + """
},
{
"name": "constant.numeric.isabelle",
"match": "\\b\\d*\\.?\\d+\\b"
},
{
"name": "string.quoted.double.isabelle",
"begin": "\"",
"patterns": [
{
"name": "constant.character.escape.isabelle",
"match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """
}
],
"end": "\""
},
{
"name": "string.quoted.backtick.isabelle",
"begin": "`",
"patterns": [
{
"name": "constant.character.escape.isabelle",
"match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """
}
],
"end": "`"
},
{
"name": "string.quoted.verbatim.isabelle",
"begin": """ + JSON.Format("""\{\*""") + """,
"patterns": [
{ "match": """ + JSON.Format("""[^*]+|\*(?!\})""") + """ }
],
"end": """ + JSON.Format("""\*\}""") + """
}
]
}
""")
}
/* build extension */
def build_extension(options: Options,
target_dir: Path = Path.current,
logic: String = default_logic,
dirs: List[Path] = Nil,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("node")
Isabelle_System.require_command("yarn")
Isabelle_System.require_command("vsce")
/* component */
val component_name = "vscode_extension-" + Date.Format.alt_date(Date.now())
val component_dir =
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* build */
val vsix_name =
Isabelle_System.with_tmp_dir("build") { build_dir =>
val manifest_text = File.read(VSCode_Main.extension_dir + VSCode_Main.MANIFEST)
val manifest_entries = split_lines(manifest_text).filter(_.nonEmpty)
val manifest_shasum: String = {
val a = SHA1.digest(manifest_text).shasum("")
val bs =
for (entry <- manifest_entries)
yield SHA1.digest(VSCode_Main.extension_dir + Path.explode(entry)).shasum(entry)
terminate_lines(a :: bs)
}
for (entry <- manifest_entries) {
val path = Path.explode(entry)
Isabelle_System.copy_file(VSCode_Main.extension_dir + path,
Isabelle_System.make_directory(build_dir + path.dir))
}
File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum)
build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)
val result =
progress.bash("yarn && vsce package", cwd = build_dir.file, echo = true).check
val Pattern = """.*Packaged:.*(isabelle-.*\.vsix).*""".r
val vsix_name =
result.out_lines.collectFirst({ case Pattern(name) => name })
.getOrElse(error("Failed to guess resulting .vsix file name"))
Isabelle_System.copy_file(build_dir + Path.basic(vsix_name), component_dir.path)
vsix_name
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_VSCODE_VSIX="$COMPONENT/""" + vsix_name + "\"\n")
/* README */
File.write(component_dir.README,
"""This the Isabelle/VSCode extension as VSIX package
It has been produced from the sources in $ISABELLE_HOME/src/Tools/extension/.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_vscode_extension", "build Isabelle/VSCode extension module",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var dirs: List[Path] = Nil
var logic = default_logic
val getopts = Getopts("""
Usage: isabelle build_vscode_extension
Options are:
-D DIR target directory (default ".")
-d DIR include session directory
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
Build the Isabelle/VSCode extension as component, for inclusion into the
local VSCodium configuration.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"l:" -> (arg => logic = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val options = Options.init()
val progress = new Console_Progress()
build_extension(options, target_dir = target_dir, logic = logic, dirs = dirs,
progress = progress)
})
}
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,464 +1,462 @@
/* 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(dir: Path, progress: Progress = new Progress): Unit = {
Isabelle_System.with_tmp_file("download") { download_file =>
Isabelle_System.download_file(vscodium_download + "/" + version + "/" + download_name,
download_file, progress = progress)
progress.echo("Extract ...")
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")
}
}
/* 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(target_dir + Path.explode(component_name)).create(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:
-
+ component_dir.write_settings("""
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)
})
}