diff --git a/src/Pure/Admin/build_csdp.scala b/src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala
+++ b/src/Pure/Admin/build_csdp.scala
@@ -1,201 +1,201 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
/* platform */
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
- val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
+ val platform_dir =
+ Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
val source_name = File.get_dir(tmp_dir)
Isabelle_System.bash(
"tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
- cwd = component_dir.file).check
+ cwd = component_dir.path.file).check
/* build */
progress.echo("Building CSDP for " + platform_name + " ...")
val build_dir = tmp_dir + Path.basic(source_name)
build_flags.find(flags => flags.platform == platform_name) match {
case None => error("No build flags for platform " + quote(platform_name))
case Some(flags) =>
File.find_files(build_dir.file, pred = file => file.getName == "Makefile").
foreach(file => flags.change(File.path(file)))
}
progress.bash(mingw.bash_script("make"), cwd = build_dir.file, echo = verbose).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir)
+ Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
Isabelle_System.copy_file(build_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
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 */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_CSDP="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/csdp"
""")
/* README */
- File.write(component_dir + Path.basic("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,138 +1,137 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
/* download executables */
for (platform <- platforms) {
val url = base_url + "/cvc5-" + version + "/" + platform.download_name
- val platform_dir = component_dir + Path.explode(platform.platform_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 */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
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 + Path.basic("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.explode(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,141 +1,141 @@
/* Title: Pure/Admin/build_e.scala
Author: Makarius
Build Isabelle E prover component from official downloads.
*/
package isabelle
object Build_E {
/* build E prover */
val default_version = "2.6"
val default_download_url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD"
def build_e(
version: String = default_version,
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val component_name = "e-" + version
- val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
.getOrElse(error("No 64bit platform"))
- val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
+ val platform_dir =
+ Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_url = download_url + "/V_" + version + "/E.tgz"
val archive_path = tmp_dir + Path.explode("E.tgz")
Isabelle_System.download_file(archive_url, archive_path, progress = progress)
Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
- Isabelle_System.bash("tar xzf " + archive_path + " && mv E src", cwd = component_dir.file).check
+ Isabelle_System.bash("tar xzf " + archive_path + " && mv E src",
+ cwd = component_dir.path.file).check
/* build */
progress.echo("Building E prover for " + platform_name + " ...")
val build_dir = tmp_dir + Path.basic("E")
val build_options = {
val result = Isabelle_System.bash("./configure --help", cwd = build_dir.file)
if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else ""
}
val build_script = "./configure" + build_options + " && make"
Isabelle_System.bash(build_script,
cwd = build_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.basic("COPYING"),
- component_dir + Path.basic("LICENSE"))
+ Isabelle_System.copy_file(build_dir + Path.basic("COPYING"), component_dir.LICENSE)
val install_files = List("epclextract", "eprover", "eprover-ho")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
val path = build_dir + Path.basic("PROVER") + Path.basic(name)
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 */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
E_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
E_VERSION=""" + quote(version) + """
""")
/* README */
- File.write(component_dir + Path.basic("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,108 +1,108 @@
/* Title: Pure/Admin/build_easychair.scala
Author: Makarius
Build Isabelle component for Easychair LaTeX style.
See also https://easychair.org/publications/for_authors
*/
package isabelle
object Build_Easychair {
/* build easychair component */
val default_url = "https://easychair.org/publications/easychair.zip"
def build_easychair(
download_url: String = default_url,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("unzip", test = "-h")
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
cwd = download_dir.file).check
val easychair_dir =
File.read_dir(download_dir) match {
case List(name) => download_dir + Path.explode(name)
case bad =>
error("Expected exactly one directory entry in " + download_file +
bad.mkString("\n", "\n ", ""))
}
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
- component_dir.file.delete
- Isabelle_System.copy_dir(easychair_dir, component_dir)
+ Isabelle_System.rm_tree(component_dir.path)
+ Isabelle_System.copy_dir(easychair_dir, component_dir.path)
+ Isabelle_System.make_directory(component_dir.etc)
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_EASYCHAIR_HOME="$COMPONENT"
""")
/* README */
- File.write(component_dir + Path.basic("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,101 +1,100 @@
/* Title: Pure/Admin/build_eptcs.scala
Author: Makarius
Build Isabelle component for EPTCS LaTeX style.
See also:
- http://style.eptcs.org
- https://github.com/EPTCS/style/releases
*/
package isabelle
object Build_EPTCS {
/* build eptcs component */
val default_url = "https://github.com/EPTCS/style/releases/download"
val default_version = "1.7.0"
def build_eptcs(
base_url: String = default_url,
version: String = default_version,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("unzip", test = "-h")
/* component */
val component = "eptcs-" + version
- val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
/* download */
val download_url = base_url + "/v" + version + "/eptcsstyle.zip"
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.download_file(download_url, download_file, progress = progress)
Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
- cwd = component_dir.file).check
+ cwd = component_dir.path.file).check
}
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_EPTCS_HOME="$COMPONENT"
""")
/* README */
- File.write(component_dir + Path.basic("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,117 +1,117 @@
/* Title: Pure/Admin/build_foiltex.scala
Author: Makarius
Build Isabelle component for FoilTeX.
See also https://ctan.org/pkg/foiltex
*/
package isabelle
object Build_Foiltex {
/* build FoilTeX component */
val default_url = "https://mirrors.ctan.org/macros/latex/contrib/foiltex.zip"
def build_foiltex(
download_url: String = default_url,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("unzip", test = "-h")
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
cwd = download_dir.file).check
val foiltex_dir =
File.read_dir(download_dir) match {
case List(name) => download_dir + Path.explode(name)
case bad =>
error("Expected exactly one directory entry in " + download_file +
bad.mkString("\n", "\n ", ""))
}
val README = Path.explode("README")
val README_flt = Path.explode("README.flt")
Isabelle_System.move_file(foiltex_dir + README, foiltex_dir + README_flt)
Isabelle_System.bash("pdflatex foiltex.ins", cwd = foiltex_dir.file).check
/* component */
val version = {
val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r
split_lines(File.read(foiltex_dir + README_flt))
.collectFirst({ case Version(v) => v })
.getOrElse(error("Failed to detect version in " + README_flt))
}
val component = "foiltex-" + version
- val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
- component_dir.file.delete
- Isabelle_System.copy_dir(foiltex_dir, component_dir)
+ Isabelle_System.rm_tree(component_dir.path)
+ Isabelle_System.copy_dir(foiltex_dir, component_dir.path)
+ Isabelle_System.make_directory(component_dir.etc)
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_FOILTEX_HOME="$COMPONENT"
""")
/* README */
- File.write(component_dir + Path.basic("README"),
+ File.write(component_dir.README,
"""This is FoilTeX from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_foiltex", "build component for FoilTeX",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_url
val getopts = Getopts("""
Usage: isabelle build_foiltex [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
Build component for FoilTeX: slides in LaTeX.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_foiltex(download_url = download_url, target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_fonts.scala b/src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala
+++ b/src/Pure/Admin/build_fonts.scala
@@ -1,364 +1,364 @@
/* 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 hinted_path(hinted: Boolean): 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_sources: List[Family] =
List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif)
val default_target_dir: Path = Path.explode("isabelle_fonts")
def build_fonts(
sources: List[Family] = default_sources,
source_dirs: List[Path] = Nil,
target_prefix: String = "Isabelle",
target_version: String = "",
target_dir: Path = default_target_dir,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("ttfautohint")
progress.echo("Directory " + target_dir)
hinting.foreach(hinted => Isabelle_System.make_directory(target_dir + hinted_path(hinted)))
val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts"))
for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)
// Isabelle fonts
val targets =
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 target_names = source_names.update(prefix = target_prefix, version = target_version)
Isabelle_System.with_tmp_file("font", "ttf") { tmp_file =>
for (hinted <- hinting) {
val target_file = target_dir + hinted_path(hinted) + target_names.ttf
progress.echo("Font " + target_file.toString + " ...")
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,
target_names.set,
Fontforge.generate(target_file),
Fontforge.close)
).check
}
}
(target_names.ttf, index)
}
// Vacuous font
{
val vacuous_file = find_file(font_dirs, Family.vacuous.get(0))
val target_names = Fontforge.font_names(vacuous_file)
val target_file = target_dir + hinted_path(false) + target_names.ttf
progress.echo("Font " + target_file.toString + " ...")
val domain =
(for ((name, index) <- targets if index == 0)
yield Fontforge.font_domain(target_dir + hinted_path(false) + 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(target_file),
Fontforge.close)
).check
}
// etc/settings
- val settings_path = Components.settings(target_dir)
+ val settings_path = Components.Directory(target_dir).settings
Isabelle_System.make_directory(settings_path.dir)
def fonts_settings(hinted: Boolean): String =
"\n isabelle_fonts \\\n" +
(for ((target, _) <- targets) yield
""" "$COMPONENT/""" + hinted_path(hinted).file_name + "/" + target.file_name + "\"")
.mkString(" \\\n")
File.write(settings_path,
"""# -*- shell-script -*- :mode=shellscript:
if grep "isabelle_fonts_hinted.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
then""" + fonts_settings(false) + """
else""" + fonts_settings(true) + """
fi
isabelle_fonts_hidden "$COMPONENT/""" + hinted_path(false).file_name + """/Vacuous.ttf"
""")
// README
Isabelle_System.copy_file(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir)
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_fonts", "construct Isabelle fonts", Scala_Project.here,
{ args =>
var source_dirs: List[Path] = Nil
val getopts = Getopts("""
Usage: isabelle build_fonts [OPTIONS]
Options are:
-d DIR additional source directory
Construct Isabelle fonts from DejaVu font families and Isabelle symbols.
""",
"d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val target_version = Date.Format.alt_date(Date.now())
val target_dir = Path.explode("isabelle_fonts-" + target_version)
val progress = new Console_Progress
build_fonts(source_dirs = source_dirs, target_dir = target_dir,
target_version = target_version, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_jcef.scala b/src/Pure/Admin/build_jcef.scala
--- a/src/Pure/Admin/build_jcef.scala
+++ b/src/Pure/Admin/build_jcef.scala
@@ -1,173 +1,172 @@
/* Title: Pure/Admin/build_jcef.scala
Author: Makarius
Build Isabelle component for Java Chromium Embedded Framework (JCEF).
See also:
- https://github.com/jcefmaven/jcefbuild
- https://github.com/chromiumembedded/java-cef
*/
package isabelle
object Build_JCEF {
/* platform information */
sealed case class JCEF_Platform(
platform_name: String, archive: String, lib: String, library: String)
private val linux_library =
"""ISABELLE_JCEF_LIBRARY="$ISABELLE_JCEF_LIB/libcef.so"
export LD_LIBRARY_PATH="$ISABELLE_JCEF_LIB:$JAVA_HOME/lib:$LD_LIBRARY_PATH""""
private val macos_library =
"""export JAVA_LIBRARY_PATH="$ISABELLE_JCEF_HOME/bin/jcef_app.app/Contents/Java:$ISABELLE_JCEF_LIB:$JAVA_LIBRARY_PATH""""
private val windows_library =
"""export PATH="$ISABELLE_JCEF_LIB:$PATH""""
val platforms: List[JCEF_Platform] =
List(
JCEF_Platform("x86_64-linux", "linux-amd64.tar.gz", "bin/lib/linux64", linux_library),
JCEF_Platform("arm64-linux", "linux-arm64.tar.gz", "bin/lib/linux64", linux_library),
JCEF_Platform("x86_64-darwin", "macosx-amd64.tar.gz",
"bin/jcef_app.app/Contents/Frameworks/Chromium Embedded Framework.framework/Libraries", macos_library),
JCEF_Platform("arm64-darwin", "macosx-arm64.tar.gz",
"bin/jcef_app.app/Contents/Frameworks/Chromium Embedded Framework.framework/Libraries", macos_library),
JCEF_Platform("x86_64-windows", "windows-amd64.tar.gz", "bin/lib/win64", windows_library))
/* build JCEF */
val default_url = "https://github.com/jcefmaven/jcefbuild/releases/download"
val default_version = "1.0.18"
def build_jcef(
base_url: String = default_url,
version: String = default_version,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
/* component name */
val component = "jcef-" + version
- val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
/* download and assemble platforms */
val platform_settings: List[String] =
for (platform <- platforms) yield {
Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_file =>
val url = base_url + "/" + version + "/" + platform.archive
Isabelle_System.download_file(url, archive_file, progress = progress)
- val platform_dir = component_dir + Path.explode(platform.platform_name)
+ val platform_dir = component_dir.path + Path.explode(platform.platform_name)
Isabelle_System.make_directory(platform_dir)
Isabelle_System.gnutar("-xzf " + File.bash_path(archive_file), dir = platform_dir).check
for {
file <- File.find_files(platform_dir.file).iterator
name = file.getName
if File.is_dll(name) || File.is_exe(name)
} File.set_executable(File.path(file), true)
val classpath =
File.find_files(platform_dir.file, pred = file => File.is_jar(file.getName))
.flatMap(file => File.relative_path(platform_dir, File.path(file)))
.map(jar => " " + quote("$ISABELLE_JCEF_HOME/" + jar.implode))
.mkString(" \\\n")
" " + platform.platform_name + ")\n" +
" " + "classpath \\\n" + classpath + "\n" +
" " + "ISABELLE_JCEF_LIB=\"$ISABELLE_JCEF_HOME/" + platform.lib + "\"\n" +
" " + platform.library + "\n" +
" " + ";;"
}
}
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_JCEF_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"
if [ -d "$COMPONENT/$ISABELLE_JCEF_PLATFORM" ]
then
ISABELLE_JCEF_HOME="$COMPONENT/$ISABELLE_JCEF_PLATFORM"
ISABELLE_JCEF_LIBRARY=""
case "$ISABELLE_JCEF_PLATFORM" in
""" + cat_lines(platform_settings) + """
esac
fi
""")
/* README */
- File.write(component_dir + Path.basic("README"),
+ File.write(component_dir.README,
"""This distribution of Java Chromium Embedded Framework (JCEF)
has been assembled from the binary builds from
https://github.com/jcefmaven/jcefbuild/releases/tag/""" +version + """
Examples invocations:
* Command-line
isabelle env bash -c 'isabelle java -Djava.library.path="$(platform_path "$ISABELLE_JCEF_LIB")" tests.detailed.MainFrame'
* Scala REPL (e.g. Isabelle/jEdit Console)
import isabelle._
System.setProperty("java.library.path", File.platform_path(Path.explode("$ISABELLE_JCEF_LIB")))
org.cef.CefApp.startup(Array())
GUI_Thread.later { val frame = new tests.detailed.MainFrame(false, false, false, Array()); frame.setSize(1200,900); frame.setVisible(true) }
* Demo websites
https://mozilla.github.io/pdf.js/web/viewer.html
https://www.w3schools.com/w3css/w3css_demo.asp
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_jcef", "build component for Java Chromium Embedded Framework",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var base_url = default_url
var version = default_version
val getopts = Getopts("""
Usage: isabelle build_jcef [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
-V VERSION version (default: """" + default_version + """")
Build component for Java Chromium Embedded Framework.
""",
"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_jcef(base_url = base_url, version = version, 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,235 +1,234 @@
/* Title: Pure/Admin/build_jdk.scala
Author: Makarius
Build Isabelle jdk component from original platform installations.
*/
package isabelle
import java.io.{File => JFile}
import java.nio.file.Files
import java.nio.file.attribute.PosixFilePermission
import scala.util.matching.Regex
object Build_JDK {
/* platform and version information */
sealed case class JDK_Platform(
platform_name: String,
platform_regex: Regex,
exe: String = "java",
macos_home: Boolean = false,
jdk_version: String = ""
) {
override def toString: String = platform_name
def platform_path: Path = Path.explode(platform_name)
def detect(jdk_dir: Path): Option[JDK_Platform] = {
val major_version = {
val Major_Version = """.*jdk(\d+).*$""".r
val jdk_name = jdk_dir.file.getName
jdk_name match {
case Major_Version(s) => s
case _ => error("Cannot determine major version from " + quote(jdk_name))
}
}
val path = jdk_dir + Path.explode("bin") + Path.explode(exe)
if (path.is_file) {
val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out
if (platform_regex.matches(file_descr)) {
val Version = ("^(" + major_version + """[0-9.+]+)(?:-LTS)?$""").r
val version_lines =
Isabelle_System.bash("strings " + File.bash_path(path)).check
.out_lines.flatMap({ case Version(s) => Some(s) case _ => None })
version_lines match {
case List(jdk_version) => Some(copy(jdk_version = jdk_version))
case _ => error("Expected unique version within executable " + path)
}
}
else None
}
else None
}
}
val templates: List[JDK_Platform] =
List(
JDK_Platform("arm64-darwin", """.*Mach-O 64-bit.*arm64.*""".r, macos_home = true),
JDK_Platform("arm64-linux", """.*ELF 64-bit.*ARM aarch64.*""".r),
JDK_Platform("x86_64-darwin", """.*Mach-O 64-bit.*x86[-_]64.*""".r, macos_home = true),
JDK_Platform("x86_64-linux", """.*ELF 64-bit.*x86[-_]64.*""".r),
JDK_Platform("x86_64-windows", """.*PE32\+ executable.*x86[-_]64.*""".r, exe = "java.exe"))
/* README */
def readme(jdk_version: String): String =
"""This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also
https://www.azul.com/downloads/zulu-community/?package=jdk
The main license is GPL2, but some modules are covered by other (more liberal)
licenses, see legal/* for details.
Linux, Windows, macOS all work uniformly, depending on platform-specific
subdirectories.
"""
/* settings */
val settings: String =
"""# -*- shell-script -*- :mode=shellscript:
case "$ISABELLE_PLATFORM_FAMILY" in
linux)
ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
windows)
ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64"
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
macos)
if [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$COMPONENT/$ISABELLE_APPLE_PLATFORM64" ]
then
ISABELLE_JAVA_PLATFORM="$ISABELLE_APPLE_PLATFORM64"
else
ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
fi
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
esac
"""
/* extract archive */
def extract_archive(dir: Path, archive: Path): JDK_Platform = {
try {
val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp"))
if (archive.get_ext == "zip") {
Isabelle_System.bash(
"unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check
}
else {
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
}
val dir_entry =
File.read_dir(tmp_dir) match {
case List(s) => s
case _ => error("Archive contains multiple directories")
}
val jdk_dir = tmp_dir + Path.explode(dir_entry)
val platform =
templates.view.flatMap(_.detect(jdk_dir))
.headOption.getOrElse(error("Failed to detect JDK platform"))
val platform_dir = dir + platform.platform_path
if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
Isabelle_System.move_file(jdk_dir, platform_dir)
platform
}
catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) }
}
/* build jdk */
def build_jdk(
archives: List[Path],
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
if (Platform.is_windows) error("Cannot build jdk on Windows")
Isabelle_System.with_tmp_dir("jdk") { dir =>
progress.echo("Extracting ...")
val platforms = archives.map(extract_archive(dir, _))
val jdk_version =
platforms.map(_.jdk_version).distinct match {
case List(version) => version
case Nil => error("No archives")
case versions =>
error("Archives contain multiple JDK versions: " + commas_quote(versions))
}
templates.filterNot(p1 => platforms.exists(p2 => p1.platform_name == p2.platform_name))
match {
case Nil =>
case missing => error("Missing platforms: " + commas_quote(missing.map(_.platform_name)))
}
val jdk_name = "jdk-" + jdk_version
val jdk_path = Path.explode(jdk_name)
- val component_dir = dir + jdk_path
+ val component_dir = Components.Directory.create(dir + jdk_path, progress = progress)
- Isabelle_System.make_directory(component_dir + Path.explode("etc"))
- File.write(Components.settings(component_dir), settings)
- File.write(component_dir + Path.explode("README"), readme(jdk_version))
+ File.write(component_dir.settings, settings)
+ File.write(component_dir.README, readme(jdk_version))
for (platform <- platforms) {
- Isabelle_System.move_file(dir + platform.platform_path, component_dir)
+ Isabelle_System.move_file(dir + platform.platform_path, component_dir.path)
}
- for (file <- File.find_files(component_dir.file, include_dirs = true)) {
+ for (file <- File.find_files(component_dir.path.file, include_dirs = true)) {
val path = file.toPath
val perms = Files.getPosixFilePermissions(path)
perms.add(PosixFilePermission.OWNER_READ)
perms.add(PosixFilePermission.GROUP_READ)
perms.add(PosixFilePermission.OTHERS_READ)
perms.add(PosixFilePermission.OWNER_WRITE)
if (file.isDirectory) {
perms.add(PosixFilePermission.OWNER_WRITE)
perms.add(PosixFilePermission.OWNER_EXECUTE)
perms.add(PosixFilePermission.GROUP_EXECUTE)
perms.add(PosixFilePermission.OTHERS_EXECUTE)
}
Files.setPosixFilePermissions(path, perms)
}
progress.echo("Archiving ...")
Isabelle_System.gnutar(
"-czf " + File.bash_path(target_dir + jdk_path.tar.gz) + " " + jdk_name, dir = dir).check
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives",
Scala_Project.here,
{ args =>
var target_dir = Path.current
val getopts = Getopts("""
Usage: isabelle build_jdk [OPTIONS] ARCHIVES...
Options are:
-D DIR target directory (default ".")
Build jdk component from tar.gz archives, with original jdk archives
for Linux, Windows, and macOS.
""",
"D:" -> (arg => target_dir = Path.explode(arg)))
val more_args = getopts(args)
if (more_args.isEmpty) getopts.usage()
val archives = more_args.map(Path.explode)
val progress = new Console_Progress()
build_jdk(archives = archives, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_jedit.scala b/src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala
+++ b/src/Pure/Admin/build_jedit.scala
@@ -1,546 +1,544 @@
/* Title: Pure/Admin/build_jedit.scala
Author: Makarius
Build component for jEdit text-editor.
*/
package isabelle
import java.nio.charset.Charset
import scala.jdk.CollectionConverters._
object Build_JEdit {
/* modes */
object Mode {
val empty: Mode = new Mode("", "", Nil)
val init: Mode =
empty +
("noWordSep" -> """_'?⇩\^<>""") +
("unalignedOpenBrackets" -> "{[(«‹⟨⌈⌊⦇⟦⦃⦉") +
("unalignedCloseBrackets" -> "⦊⦄⟧⦈⌋⌉⟩›»)]}") +
("tabSize" -> "2") +
("indentSize" -> "2")
val list: List[Mode] = {
val isabelle_news: Mode = init.define("isabelle-news", "Isabelle NEWS")
val isabelle: Mode =
init.define("isabelle", "Isabelle theory") +
("commentStart" -> "(*") +
("commentEnd" -> "*)")
val isabelle_ml: Mode = isabelle.define("isabelle-ml", "Isabelle/ML")
val isabelle_root: Mode = isabelle.define("isabelle-root", "Isabelle session root")
val isabelle_options: Mode = isabelle.define("isabelle-options", "Isabelle options")
val sml: Mode =
init.define("sml", "Standard ML") +
("commentStart" -> "(*") +
("commentEnd" -> "*)") +
("noWordSep" -> "_'")
List(isabelle_news, isabelle, isabelle_ml, isabelle_root, isabelle_options, sml)
}
}
final case class Mode private(name: String, description: String, rev_props: Properties.T) {
override def toString: String = name
def define(a: String, b: String): Mode = new Mode(a, b, rev_props)
def + (entry: Properties.Entry): Mode =
new Mode(name, description, Properties.put(rev_props, entry))
def write(dir: Path): Unit = {
require(name.nonEmpty && description.nonEmpty, "Bad Isabelle/jEdit mode content")
val properties =
rev_props.reverse.map(p =>
Symbol.spaces(4) +
XML.string_of_tree(XML.elem(Markup("PROPERTY", List("NAME" -> p._1, "VALUE" -> p._2)))))
File.write(dir + Path.basic(name).xml,
"""
""" + properties.mkString("\n", "\n", "") + """
""")
}
}
/* build jEdit component */
private val download_jars: List[(String, String)] =
List(
"https://repo1.maven.org/maven2/com/google/code/findbugs/jsr305/3.0.2/jsr305-3.0.2.jar" ->
"jsr305-3.0.2.jar")
private val download_plugins: List[(String, String)] =
List(
"Code2HTML" -> "0.7",
"CommonControls" -> "1.7.4",
"Console" -> "5.1.4",
"ErrorList" -> "2.4.0",
"Highlight" -> "2.5",
"Navigator" -> "2.7",
"SideKick" -> "1.8")
private def exclude_package(name: String): Boolean =
name.startsWith("de.masters_of_disaster.ant") ||
name == "doclet" ||
name == "installer"
def build_jedit(
- component_dir: Path,
+ component_path: Path,
version: String,
original: Boolean = false,
java_home: Path = default_java_home,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("ant", test = "-version")
Isabelle_System.require_command("patch")
Isabelle_System.require_command("unzip", test = "-h")
- Isabelle_System.new_directory(component_dir)
-
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
+ val component_dir = Components.Directory.create(component_path, progress = progress)
/* jEdit directory */
val jedit = "jedit" + version
val jedit_patched = jedit + "-patched"
- val jedit_dir = Isabelle_System.make_directory(component_dir + Path.basic(jedit))
- val jedit_patched_dir = component_dir + Path.basic(jedit_patched)
+ val jedit_dir = Isabelle_System.make_directory(component_path + Path.basic(jedit))
+ val jedit_patched_dir = component_path + Path.basic(jedit_patched)
def download_jedit(dir: Path, name: String, target_name: String = ""): Path = {
val jedit_name = jedit + name
val url =
"https://sourceforge.net/projects/jedit/files/jedit/" +
version + "/" + jedit_name + "/download"
val path = dir + Path.basic(proper_string(target_name) getOrElse jedit_name)
Isabelle_System.download_file(url, path, progress = progress)
path
}
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* original version */
val install_path = download_jedit(tmp_dir, "install.jar")
Isabelle_System.bash("""export CLASSPATH=""
isabelle_java java -Duser.home=""" + File.bash_platform_path(tmp_dir) +
" -jar " + File.bash_platform_path(install_path) + " auto " +
File.bash_platform_path(jedit_dir) + " unix-script=off unix-man=off").check
val source_path = download_jedit(tmp_dir, "source.tar.bz2")
Isabelle_System.gnutar("-xjf " + File.bash_path(source_path), dir = jedit_dir).check
/* patched version */
Isabelle_System.copy_dir(jedit_dir, jedit_patched_dir)
val source_dir = jedit_patched_dir + Path.basic("jEdit")
val org_source_dir = source_dir + Path.basic("org")
val tmp_source_dir = tmp_dir + Path.basic("jEdit")
progress.echo("Patching jEdit sources ...")
for {
file <- File.find_files(Path.explode("~~/src/Tools/jEdit/patches").file).iterator
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_dir.java_path.relativize(file.toPath).toFile).implode
+ } yield File.path(component_path.java_path.relativize(file.toPath).toFile).implode
- File.write(etc_dir + Path.explode("build.props"),
+ File.write(component_dir.build_props,
"module = " + jedit_patched + "/jedit.jar\n" +
"no_build = true\n" +
"requirements = env:JEDIT_JARS\n" +
("sources =" :: java_sources.sorted.map(" " + _)).mkString("", " \\\n", "\n"))
}
/* jars */
val jars_dir = Isabelle_System.make_directory(jedit_patched_dir + Path.basic("jars"))
for { (url, name) <- download_jars } {
Isabelle_System.download_file(url, jars_dir + Path.basic(name), progress = progress)
}
for { (name, vers) <- download_plugins } {
Isabelle_System.with_tmp_file("tmp", ext = "zip") { zip_path =>
val url =
"https://sourceforge.net/projects/jedit-plugins/files/" + name + "/" + vers + "/" +
name + "-" + vers + "-bin.zip/download"
Isabelle_System.download_file(url, zip_path, progress = progress)
Isabelle_System.bash("unzip -x " + File.bash_path(zip_path), cwd = jars_dir.file).check
}
}
/* resources */
val keep_encodings = List("ISO-8859-1", "ISO-8859-15", "US-ASCII", "UTF-8", "windows-1252")
val drop_encodings =
Charset.availableCharsets().keySet().asScala.toList.sorted.filterNot(keep_encodings.contains)
File.write(jedit_patched_dir + Path.explode("properties/jEdit.props"),
"""#jEdit properties
autoReloadDialog=false
buffer.deepIndent=false
buffer.encoding=UTF-8-Isabelle
buffer.indentSize=2
buffer.lineSeparator=\n
buffer.maxLineLen=100
buffer.noTabs=true
buffer.sidekick.keystroke-parse=false
buffer.tabSize=2
buffer.undoCount=1000
close-docking-area.shortcut2=C+e C+CIRCUMFLEX
complete-word.shortcut=
console.dock-position=floating
console.encoding=UTF-8
console.font=Isabelle DejaVu Sans Mono
console.fontsize=14
delete-line.shortcut=A+d
delete.shortcut2=C+d
""" + drop_encodings.map(a => "encoding.opt-out." + a + "=true").mkString("\n") + """
encodingDetectors=BOM XML-PI buffer-local-property
end.shortcut=
expand-abbrev.shortcut2=CA+SPACE
expand-folds.shortcut=
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
foldPainter=Circle
gatchan.highlight.overview=false
helpviewer.font=Isabelle DejaVu Serif
helpviewer.fontsize=12
home.shortcut=
hypersearch-results.dock-position=right
insert-newline-indent.shortcut=
insert-newline.shortcut=
isabelle-debugger.dock-position=floating
isabelle-documentation.dock-position=left
isabelle-export-browser.label=Browse theory exports
isabelle-output.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
isabelle-query.dock-position=bottom
isabelle-session-browser.label=Browse session information
isabelle-simplifier-trace.dock-position=floating
isabelle-sledgehammer.dock-position=bottom
isabelle-state.dock-position=right
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
isabelle.complete-word.label=Complete word
isabelle.complete.label=Complete Isabelle text
isabelle.complete.shortcut2=C+b
isabelle.control-bold.label=Control bold
isabelle.control-bold.shortcut=C+e RIGHT
isabelle.control-emph.label=Control emphasized
isabelle.control-emph.shortcut=C+e LEFT
isabelle.control-reset.label=Control reset
isabelle.control-reset.shortcut=C+e BACK_SPACE
isabelle.control-sub.label=Control subscript
isabelle.control-sub.shortcut=C+e DOWN
isabelle.control-sup.label=Control superscript
isabelle.control-sup.shortcut=C+e UP
isabelle.decrease-font-size.label=Decrease font size
isabelle.decrease-font-size.shortcut2=C+SUBTRACT
isabelle.decrease-font-size.shortcut=C+MINUS
isabelle.decrease-font-size2.label=Decrease font size (clone)
isabelle.draft.label=Show draft in browser
isabelle.exclude-word-permanently.label=Exclude word permanently
isabelle.exclude-word.label=Exclude word
isabelle.first-error.label=Go to first error
isabelle.first-error.shortcut=CS+a
isabelle.goto-entity.label=Go to definition of formal entity at caret
isabelle.goto-entity.shortcut=CS+d
isabelle.include-word-permanently.label=Include word permanently
isabelle.include-word.label=Include word
isabelle.increase-font-size.label=Increase font size
isabelle.increase-font-size.shortcut2=C+ADD
isabelle.increase-font-size.shortcut=C+PLUS
isabelle.increase-font-size2.label=Increase font size (clone)
isabelle.increase-font-size2.shortcut=C+EQUALS
isabelle.java-monitor.label=Java/VM monitor
isabelle.last-error.label=Go to last error
isabelle.last-error.shortcut=CS+z
isabelle.message.label=Show message
isabelle.message.shortcut=CS+m
isabelle.newline.label=Newline with indentation of Isabelle keywords
isabelle.newline.shortcut=ENTER
isabelle.next-error.label=Go to next error
isabelle.next-error.shortcut=CS+n
isabelle.options.label=Isabelle options
isabelle.prev-error.label=Go to previous error
isabelle.prev-error.shortcut=CS+p
isabelle.preview.label=Show preview in browser
isabelle.reset-continuous-checking.label=Reset continuous checking
isabelle.reset-font-size.label=Reset font size
isabelle.reset-node-required.label=Reset node required
isabelle.reset-words.label=Reset non-permanent words
isabelle.select-entity.label=Select all occurences of formal entity at caret
isabelle.select-entity.shortcut=CS+ENTER
isabelle.set-continuous-checking.label=Set continuous checking
isabelle.set-node-required.label=Set node required
isabelle.toggle-breakpoint.label=Toggle Breakpoint
isabelle.toggle-continuous-checking.label=Toggle continuous checking
isabelle.toggle-continuous-checking.shortcut=C+e ENTER
isabelle.toggle-node-required.label=Toggle node required
isabelle.toggle-node-required.shortcut=C+e SPACE
isabelle.tooltip.label=Show tooltip
isabelle.tooltip.shortcut=CS+b
isabelle.update-state.label=Update state output
isabelle.update-state.shortcut=S+ENTER
lang.usedefaultlocale=false
largefilemode=full
line-end.shortcut=END
line-home.shortcut=HOME
logo.icon.medium=32x32/apps/isabelle.gif
lookAndFeel=com.formdev.flatlaf.FlatLightLaf
match-bracket.shortcut2=C+9
metal.primary.font=Isabelle DejaVu Sans
metal.primary.fontsize=12
metal.secondary.font=Isabelle DejaVu Sans
metal.secondary.fontsize=12
navigator.showOnToolbar=true
new-file-in-mode.shortcut=
next-bracket.shortcut2=C+e C+9
options.shortcuts.deletekeymap.label=Delete
options.shortcuts.duplicatekeymap.dialog.title=Keymap name
options.shortcuts.duplicatekeymap.label=Duplicate
options.shortcuts.resetkeymap.dialog.title=Reset keymap
options.shortcuts.resetkeymap.label=Reset
options.textarea.lineSpacing=1
plugin-blacklist.MacOSX.jar=true
plugin.MacOSXPlugin.altDispatcher=false
plugin.MacOSXPlugin.disableOption=true
prev-bracket.shortcut2=C+e C+8
print.font=Isabelle DejaVu Sans Mono
print.glyphVector=true
recent-buffer.shortcut2=C+CIRCUMFLEX
restore.remote=false
restore=false
search.subdirs.toggle=true
select-block.shortcut2=C+8
sidekick-tree.dock-position=right
sidekick.auto-complete-popup-get-focus=true
sidekick.buffer-save-parse=true
sidekick.complete-delay=0
sidekick.complete-instant.toggle=false
sidekick.complete-popup.accept-characters=\\t
sidekick.complete-popup.insert-characters=
sidekick.persistentFilter=true
sidekick.showFilter=true
sidekick.splitter.location=721
systrayicon=false
tip.show=false
toggle-full-screen.shortcut2=S+F11
toggle-multi-select.shortcut2=C+NUMBER_SIGN
toggle-rect-select.shortcut2=A+NUMBER_SIGN
twoStageSave=false
vfs.browser.dock-position=left
vfs.favorite.0.type=1
vfs.favorite.0=$ISABELLE_HOME
vfs.favorite.1.type=1
vfs.favorite.1=$ISABELLE_HOME_USER
vfs.favorite.2.type=1
vfs.favorite.2=$JEDIT_HOME
vfs.favorite.3.type=1
vfs.favorite.3=$JEDIT_SETTINGS
vfs.favorite.4.type=1
vfs.favorite.4=isabelle-export:
vfs.favorite.5.type=1
vfs.favorite.5=isabelle-session:
view.antiAlias=subpixel HRGB
view.blockCaret=true
view.caretBlink=false
view.docking.framework=PIDE
view.eolMarkers=false
view.extendedState=0
view.font=Isabelle DejaVu Sans Mono
view.fontsize=18
view.fracFontMetrics=false
view.gutter.font=Isabelle DejaVu Sans Mono
view.gutter.fontsize=12
view.gutter.lineNumbers=false
view.gutter.selectionAreaWidth=18
view.height=850
view.middleMousePaste=true
view.showToolbar=true
view.status.memory.background=#666699
view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
view.thickCaret=true
view.width=1200
xml-insert-closing-tag.shortcut=
""")
val modes_dir = jedit_patched_dir + Path.basic("modes")
Mode.list.foreach(_.write(modes_dir))
File.change_lines(modes_dir + Path.basic("catalog")) { _.flatMap(line =>
if (line.containsSlice("FILE=\"ml.xml\"") ||
line.containsSlice("FILE_NAME_GLOB=\"*.{sml,ml}\"") ||
line.containsSlice("FILE_NAME_GLOB=\"*.ftl\"")) Nil
else if (line.containsSlice("NAME=\"jamon\"")) {
List(
"""""",
"",
"""""",
"",
"""""",
"",
"""""",
"",
"""""",
"",
line)
}
else if (line.containsSlice("NAME=\"sqr\"")) {
List(
"""""",
"",
line)
}
else List(line))
}
/* doc */
val doc_dir = jedit_patched_dir + Path.basic("doc")
download_jedit(doc_dir, "manual-a4.pdf", target_name = "jedit-manual.pdf")
Isabelle_System.copy_file(
doc_dir + Path.basic("CHANGES.txt"), doc_dir + Path.basic("jedit-changes"))
File.write(doc_dir + Path.basic("Contents"),
"""Original jEdit Documentation
jedit-manual jEdit User's Guide
jedit-changes jEdit Version History
""")
/* make patch */
- File.write(component_dir + Path.basic(jedit).patch,
- Isabelle_System.make_patch(component_dir, Path.basic(jedit), Path.basic(jedit_patched)))
+ 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(etc_dir + Path.explode("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
JEDIT_HOME="$COMPONENT/""" + jedit_patched + """"
JEDIT_JARS=""" + quote(File.read_dir(jars_dir).map("$JEDIT_HOME/jars/" + _).mkString(":")) + """
JEDIT_JAR="$JEDIT_HOME/jedit.jar"
classpath "$JEDIT_JAR"
JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9"
JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4g -Xss16m"
JEDIT_JAVA_SYSTEM_OPTIONS="-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/doc"
""")
/* README */
- File.write(component_dir + Path.basic("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,114 +1,113 @@
/* Title: Pure/Admin/build_lipics.scala
Author: Makarius
Build Isabelle component for Dagstuhl LIPIcs style.
See also:
- https://github.com/dagstuhl-publishing/styles
- https://submission.dagstuhl.de/documentation/authors
- https://www.dagstuhl.de/en/publications/lipics
*/
package isabelle
object Build_LIPIcs {
/* files for document preparation */
val document_files: List[Path] =
for (name <- List("cc-by.pdf", "lipics-logo-bw.pdf", "lipics-v2021.cls"))
yield Path.explode("$ISABELLE_LIPICS_HOME/" + name)
/* build lipics component */
val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.2.tar.gz"
def build_lipics(
download_url: String = default_url,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
Isabelle_System.with_tmp_file("download", ext = "tar.gz") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
Isabelle_System.gnutar("-xzf " + File.bash_path(download_file),
dir = download_dir, strip = 1).check
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 = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
- Isabelle_System.copy_dir(lipics_dir, component_dir)
+ Isabelle_System.copy_dir(lipics_dir, component_dir.path)
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_LIPICS_HOME="$COMPONENT/authors"
""")
/* README */
- File.write(component_dir + Path.basic("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,117 +1,117 @@
/* Title: Pure/Admin/build_llncs.scala
Author: Makarius
Build Isabelle component for Springer LaTeX LNCS style.
See also:
- https://ctan.org/pkg/llncs?lang=en
- https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines
*/
package isabelle
object Build_LLNCS {
/* build llncs component */
val default_url = "https://mirrors.ctan.org/macros/latex/contrib/llncs.zip"
def build_llncs(
download_url: String = default_url,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("unzip", test = "-h")
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
cwd = download_dir.file).check
val llncs_dir =
File.read_dir(download_dir) match {
case List(name) => download_dir + Path.explode(name)
case bad =>
error("Expected exactly one directory entry in " + download_file +
bad.mkString("\n", "\n ", ""))
}
val readme = Path.explode("README.md")
File.change(llncs_dir + readme)(_.replace(" ", "\u00a0"))
/* component */
val version = {
val Version = """^_.* v(.*)_$""".r
split_lines(File.read(llncs_dir + readme))
.collectFirst({ case Version(v) => v })
.getOrElse(error("Failed to detect version in " + readme))
}
val component = "llncs-" + version
- val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
- component_dir.file.delete
- Isabelle_System.copy_dir(llncs_dir, component_dir)
+ Isabelle_System.rm_tree(component_dir.path)
+ Isabelle_System.copy_dir(llncs_dir, component_dir.path)
+ Isabelle_System.make_directory(component_dir.etc)
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_LLNCS_HOME="$COMPONENT"
""")
/* README */
- File.write(component_dir + Path.basic("README"),
+ File.write(component_dir.README,
"""This is the Springer LaTeX LNCS style for authors from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_llncs", "build component for Springer LaTeX LNCS style",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_url
val getopts = Getopts("""
Usage: isabelle build_llncs [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
Build component for Springer LaTeX LNCS style.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_llncs(download_url = download_url, target_dir = target_dir, progress = progress)
})
}
diff --git a/src/Pure/Admin/build_minisat.scala b/src/Pure/Admin/build_minisat.scala
--- a/src/Pure/Admin/build_minisat.scala
+++ b/src/Pure/Admin/build_minisat.scala
@@ -1,155 +1,155 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
/* platform */
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
- val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
+ val platform_dir =
+ Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
val source_name = File.get_dir(tmp_dir)
Isabelle_System.bash(
"tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
- cwd = component_dir.file).check
+ cwd = component_dir.path.file).check
/* build */
progress.echo("Building Minisat for " + platform_name + " ...")
val build_dir = tmp_dir + Path.basic(source_name)
- Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir)
+ Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
if (Platform.is_macos) {
File.change(build_dir + Path.explode("Makefile")) {
_.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "")
}
}
progress.bash("make r", build_dir.file, echo = verbose).check
Isabelle_System.copy_file(
build_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 */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
MINISAT_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ISABELLE_MINISAT="$MINISAT_HOME/minisat"
""")
/* README */
- File.write(component_dir + Path.basic("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,103 +1,102 @@
/* Title: Pure/Admin/build_pdfjs.scala
Author: Makarius
Build Isabelle component for Mozilla PDF.js.
See also:
- https://github.com/mozilla/pdf.js
- https://github.com/mozilla/pdf.js/releases
- https://github.com/mozilla/pdf.js/wiki/Setup-PDF.js-in-a-website
*/
package isabelle
object Build_PDFjs {
/* build pdfjs component */
val default_url = "https://github.com/mozilla/pdf.js/releases/download"
val default_version = "2.14.305"
def build_pdfjs(
base_url: String = default_url,
version: String = default_version,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("unzip", test = "-h")
/* component name */
val component = "pdfjs-" + version
- val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
/* download */
val download_url = base_url + "/v" + version
Isabelle_System.with_tmp_file("archive", ext = "zip") { archive_file =>
Isabelle_System.download_file(download_url + "/pdfjs-" + version + "-legacy-dist.zip",
archive_file, progress = progress)
Isabelle_System.bash("unzip -x " + File.bash_path(archive_file),
- cwd = component_dir.file).check
+ cwd = component_dir.path.file).check
}
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_PDFJS_HOME="$COMPONENT"
""")
/* README */
- File.write(component_dir + Path.basic("README"),
+ File.write(component_dir.README,
"""This is PDF.js from
""" + download_url + """
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_pdfjs", "build component for Mozilla PDF.js",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var base_url = default_url
var version = default_version
val getopts = Getopts("""
Usage: isabelle build_pdfjs [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL (default: """" + default_url + """")
-V VERSION version (default: """" + default_version + """")
Build component for PDF.js.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => base_url = arg),
"V:" -> (arg => version = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_pdfjs(base_url = base_url, version = version, target_dir = target_dir,
progress = progress)
})
}
diff --git a/src/Pure/Admin/build_polyml.scala b/src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala
+++ b/src/Pure/Admin/build_polyml.scala
@@ -1,267 +1,266 @@
/* Title: Pure/Admin/build_polyml.scala
Author: Makarius
Build Poly/ML from sources.
*/
package isabelle
import scala.util.matching.Regex
object Build_PolyML {
/** platform-specific build **/
sealed case class Platform_Info(
options: List[String] = Nil,
setup: String = "",
libs: Set[String] = Set.empty)
private val platform_info = Map(
"linux" ->
Platform_Info(
options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
libs = Set("libgmp")),
"darwin" ->
Platform_Info(
options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"),
setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
libs = Set("libpolyml", "libgmp")),
"windows" ->
Platform_Info(
options =
List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
setup = MinGW.environment_export,
libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread")))
def build_polyml(
root: Path,
sha1_root: Option[Path] = None,
progress: Progress = new Progress,
arch_64: Boolean = false,
options: List[String] = Nil,
mingw: MinGW = MinGW.none
): Unit = {
if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
error("Bad Poly/ML root directory: " + root)
val platform = Isabelle_Platform.self
val polyml_platform =
(if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name
val sha1_platform = platform.arch_64 + "-" + platform.os_name
val info =
platform_info.getOrElse(platform.os_name,
error("Bad OS platform: " + quote(platform.os_name)))
if (platform.is_linux) Isabelle_System.require_command("chrpath")
/* bash */
def bash(
cwd: Path, script: String,
redirect: Boolean = false,
echo: Boolean = false
): Process_Result = {
val script1 =
if (platform.is_arm && platform.is_macos) {
"arch -arch arm64 bash -c " + Bash.string(script)
}
else mingw.bash_script(script)
progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo)
}
/* configure and make */
val configure_options =
List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") :::
info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit"))
bash(root,
info.setup + "\n" +
"""
[ -f Makefile ] && make distclean
{
./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
rm -rf target
make && make install
} || { echo "Build failed" >&2; exit 2; }
""", redirect = true, echo = true).check
/* sha1 library */
val sha1_files =
if (sha1_root.isDefined) {
val dir1 = sha1_root.get
bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check
val dir2 = dir1 + Path.explode(sha1_platform)
File.read_dir(dir2).map(entry => dir2 + Path.basic(entry))
}
else Nil
/* install */
val platform_dir = Path.explode(polyml_platform)
Isabelle_System.rm_tree(platform_dir)
Isabelle_System.make_directory(platform_dir)
for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir)
for {
d <- List("target/bin", "target/lib")
dir = root + Path.explode(d)
entry <- File.read_dir(dir)
} Isabelle_System.move_file(dir + Path.explode(entry), platform_dir)
Executable.libraries_closure(
platform_dir + Path.basic("poly").platform_exe, mingw = mingw, filter = info.libs)
/* polyc: directory prefix */
val Header = "#! */bin/sh".r
File.change_lines(platform_dir + Path.explode("polyc")) {
case Header() :: lines =>
val lines1 =
lines.map(line =>
if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
else line)
"#!/usr/bin/env bash" :: lines1
case lines =>
error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
}
}
/** skeleton for component **/
private def extract_sources(source_archive: Path, component_dir: Path): Unit = {
if (source_archive.get_ext == "zip") {
Isabelle_System.bash(
"unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check
}
else {
Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
}
val src_dir = component_dir + Path.explode("src")
File.read_dir(component_dir) match {
case List(s) => Isabelle_System.move_file(component_dir + Path.basic(s), src_dir)
case _ => error("Source archive contains multiple directories")
}
val lines = split_lines(File.read(src_dir + Path.explode("RootX86.ML")))
val ml_files =
for {
line <- lines
rest <- Library.try_unprefix("use", line)
} yield "ML_file" + rest
File.write(src_dir + Path.explode("ROOT.ML"),
"""(* Poly/ML Compiler root file.
When this file is open in the Prover IDE, the ML files of the Poly/ML
compiler can be explored interactively. This is a separate copy: it does
not affect the running ML session. *)
""" + ml_files.mkString("\n", "\n", "\n"))
}
def build_polyml_component(
source_archive: Path,
- component_dir: Path,
+ component_path: Path,
sha1_root: Option[Path] = None
): Unit = {
- Isabelle_System.new_directory(component_dir)
- extract_sources(source_archive, component_dir)
+ val component_dir = Components.Directory.create(component_path)
+ extract_sources(source_archive, component_path)
- Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/README"), component_dir)
-
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
- Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/settings"), etc_dir)
+ Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/settings"), component_dir.etc)
+ Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/README"), component_dir.path)
sha1_root match {
case Some(dir) =>
- Mercurial.repository(dir).archive(File.standard_path(component_dir + Path.explode("sha1")))
+ Mercurial.repository(dir)
+ .archive(File.standard_path(component_dir.path + Path.explode("sha1")))
case None =>
}
}
/** Isabelle tool wrappers **/
val isabelle_tool1 =
Isabelle_Tool("build_polyml", "build Poly/ML from sources", Scala_Project.here,
{ args =>
var mingw = MinGW.none
var arch_64 = false
var sha1_root: Option[Path] = None
val getopts = Getopts("""
Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
Options are:
-M DIR msys/mingw root specification for Windows
-m ARCH processor architecture (32 or 64, default: """ +
(if (arch_64) "64" else "32") + """)
-s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1
Build Poly/ML in the ROOT directory of its sources, with additional
CONFIGURE_OPTIONS (e.g. --without-gmp).
""",
"M:" -> (arg => mingw = MinGW(Path.explode(arg))),
"m:" ->
{
case "32" => arch_64 = false
case "64" => arch_64 = true
case bad => error("Bad processor architecture: " + quote(bad))
},
"s:" -> (arg => sha1_root = Some(Path.explode(arg))))
val more_args = getopts(args)
val (root, options) =
more_args match {
case root :: options => (Path.explode(root), options)
case Nil => getopts.usage()
}
build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
arch_64 = arch_64, options = options, mingw = mingw)
})
val isabelle_tool2 =
Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component",
Scala_Project.here,
{ args =>
var sha1_root: Option[Path] = None
val getopts = Getopts("""
Usage: isabelle build_polyml_component [OPTIONS] SOURCE_ARCHIVE COMPONENT_DIR
Options are:
-s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1
Make skeleton for Poly/ML component, based on official source archive
(zip or tar.gz).
""",
"s:" -> (arg => sha1_root = Some(Path.explode(arg))))
val more_args = getopts(args)
val (source_archive, component_dir) =
more_args match {
case List(archive, dir) => (Path.explode(archive), Path.explode(dir))
case _ => getopts.usage()
}
build_polyml_component(source_archive, component_dir, sha1_root = sha1_root)
})
}
diff --git a/src/Pure/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,129 +1,127 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(download_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(download_name), progress = progress)
/* LICENSE */
- File.write(component_dir + Path.basic("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 + Path.basic("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 */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
-
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
classpath "$COMPONENT/""" + download_name + """.jar"
""")
/* jar */
- val jar = component_dir + Path.basic(download_name).ext("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,95 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), 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
- component_dir.file.delete()
+ Isabelle_System.rm_tree(component_dir.path)
Isabelle_System.copy_dir(tmp_dir + Path.explode("node_modules/prismjs"),
- component_dir)
+ component_dir.path)
+ Isabelle_System.make_directory(component_dir.etc)
}
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_PRISMJS_HOME="$COMPONENT"
""")
/* README */
- File.write(component_dir + Path.basic("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,176 +1,174 @@
/* Title: Pure/Admin/build_scala.scala
Author: Makarius
Build Isabelle Scala component from official downloads.
*/
package isabelle
object Build_Scala {
/* downloads */
sealed case class Download(
name: String,
version: String,
url: String,
physical_url: String = "",
base_version: String = "3"
) {
def make_url(template: String): String =
template.replace("{V}", version).replace("{B}", base_version)
def proper_url: String = make_url(proper_string(physical_url).getOrElse(url))
def artifact: String =
Library.take_suffix[Char](_ != '/', proper_url.toList)._2.mkString
def get(path: Path, progress: Progress = new Progress): Unit =
Isabelle_System.download_file(proper_url, path, progress = progress)
def get_unpacked(dir: Path, strip: Int = 0, progress: Progress = new Progress): Unit =
Isabelle_System.with_tmp_file("archive"){ archive_path =>
get(archive_path, progress = progress)
progress.echo("Unpacking " + artifact)
Isabelle_System.gnutar(
"-xzf " + File.bash_path(archive_path), dir = dir, strip = strip).check
}
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.0", 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 = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
/* download */
- main_download.get_unpacked(component_dir, strip = 1, progress = progress)
+ main_download.get_unpacked(component_dir.path, strip = 1, progress = progress)
- val lib_dir = component_dir + Path.explode("lib")
lib_downloads.foreach(download =>
- download.get(lib_dir + Path.basic(download.artifact), progress = progress))
+ download.get(component_dir.lib + Path.basic(download.artifact), progress = progress))
- File.write(component_dir + Path.basic("LICENSE"),
+ 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),
- File.read(component_dir + Path.explode("bin/common"))
+ "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 */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
SCALA_HOME="$COMPONENT"
SCALA_INTERFACES="$SCALA_HOME/lib/""" + interfaces + """"
""" + terminate_lines(classpath.map(jar => "classpath \"$SCALA_HOME/lib/" + jar + "\"")))
/* adhoc changes */
val patched_scripts = List("bin/scala", "bin/scalac")
for (name <- patched_scripts) {
- File.change(component_dir + Path.explode(name)) {
+ File.change(component_dir.path + Path.explode(name)) {
_.replace(""""-Dscala.home=$PROG_HOME"""", """"-Dscala.home=\"$PROG_HOME\""""")
}
}
/* README */
- File.write(component_dir + Path.basic("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,179 +1,178 @@
/* Title: Pure/Admin/build_spass.scala
Author: Makarius
Build Isabelle SPASS component from unofficial download.
*/
package isabelle
object Build_SPASS {
/* build SPASS */
val default_download_url = "https://www.cs.vu.nl/~jbe248/spass-3.8ds-src.tar.gz"
val standard_version = "3.8ds"
def build_spass(
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current): Unit = {
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
Isabelle_System.require_command("bison")
Isabelle_System.require_command("flex")
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
val Component_Name = """^(.+)-src\.tar.gz$""".r
val Version = """^[^-]+-([^-]+)$""".r
val (archive_name, archive_base_name) =
download_url match {
case Archive_Name(name) => (name, Library.perhaps_unsuffix(".tar.gz", 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 = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
.getOrElse(error("No 64bit platform"))
- val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
+ val platform_dir =
+ Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
Isabelle_System.bash(
"tar xzf " + archive_path + " && mv " + Bash.string(archive_base_name) + " src",
- cwd = component_dir.file).check
+ cwd = component_dir.path.file).check
/* build */
progress.echo("Building SPASS for " + platform_name + " ...")
val build_dir = tmp_dir + Path.basic(archive_base_name)
if (Platform.is_windows) {
File.change(build_dir + Path.basic("misc.c")) {
_.replace("""#include "execinfo.h" """, "")
.replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }")
}
}
Isabelle_System.bash("make",
cwd = build_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.basic("LICENCE"),
- component_dir + Path.basic("LICENSE"))
+ Isabelle_System.copy_file(build_dir + Path.basic("LICENCE"), component_dir.LICENSE)
val install_files = List("SPASS")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
val path = build_dir + Path.basic(name)
if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
}
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
SPASS_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
SPASS_VERSION=""" + quote(version) + """
""")
/* README */
- File.write(component_dir + Path.basic("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 */
def build_sqlite(
download_url: String,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
val Download_Name = """^.*/([^/]+)\.jar""".r
val download_name =
download_url match {
case Download_Name(download_name) => download_name
case _ => error("Malformed jar download URL: " + quote(download_url))
}
/* component */
- val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(download_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(download_name), progress = progress)
/* README */
- File.write(component_dir + Path.basic("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 */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
-
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_SQLITE_HOME="$COMPONENT"
classpath "$ISABELLE_SQLITE_HOME/""" + download_name + """.jar"
""")
/* jar */
- val jar = component_dir + Path.basic(download_name).ext("jar")
+ val jar = component_dir.path + Path.basic(download_name).ext("jar")
Isabelle_System.download_file(download_url, jar, progress = progress)
Isabelle_System.with_tmp_dir("build") { jar_dir =>
progress.echo("Unpacking " + jar)
Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute),
cwd = jar_dir.file).check
val jar_files =
List(
"META-INF/maven/org.xerial/sqlite-jdbc/LICENSE" -> ".",
"META-INF/maven/org.xerial/sqlite-jdbc/LICENSE.zentus" -> ".",
"org/sqlite/native/Linux/aarch64/libsqlitejdbc.so" -> "arm64-linux",
"org/sqlite/native/Linux/x86_64/libsqlitejdbc.so" -> "x86_64-linux",
"org/sqlite/native/Mac/aarch64/libsqlitejdbc.jnilib" -> "arm64-darwin",
"org/sqlite/native/Mac/x86_64/libsqlitejdbc.jnilib" -> "x86_64-darwin",
"org/sqlite/native/Windows/x86_64/sqlitejdbc.dll" -> "x86_64-windows")
for ((file, dir) <- jar_files) {
- val target = Isabelle_System.make_directory(component_dir + Path.explode(dir))
+ 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.explode("x86_64-windows/sqlitejdbc.dll"), true)
+ 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
val getopts = Getopts("""
Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD
Options are:
-D DIR target directory (default ".")
Build sqlite-jdbc component from the specified download URL (JAR), see also
https://github.com/xerial/sqlite-jdbc and
https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
""",
"D:" -> (arg => target_dir = Path.explode(arg)))
val more_args = getopts(args)
val download_url =
more_args match {
case List(download_url) => download_url
case _ => getopts.usage()
}
val progress = new Console_Progress()
build_sqlite(download_url, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_vampire.scala b/src/Pure/Admin/build_vampire.scala
--- a/src/Pure/Admin/build_vampire.scala
+++ b/src/Pure/Admin/build_vampire.scala
@@ -1,164 +1,164 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component), progress = progress)
/* platform */
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
- val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
+ val platform_dir =
+ Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
val source_name = File.get_dir(tmp_dir)
Isabelle_System.bash(
"tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
- cwd = component_dir.file).check
+ cwd = component_dir.path.file).check
/* build */
progress.echo("Building Vampire for " + platform_name + " ...")
val build_dir = tmp_dir + Path.basic(source_name)
- Isabelle_System.copy_file(build_dir + Path.explode("LICENCE"), component_dir)
+ Isabelle_System.copy_file(build_dir + Path.explode("LICENCE"), component_dir.path)
val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
val cmake_out =
progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""",
cwd = build_dir.file, echo = verbose).check.out
val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
val binary =
split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
.getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
platform_dir + Path.basic("vampire").platform_exe)
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire"
""")
/* README */
- File.write(component_dir + Path.basic("README"),
+ File.write(component_dir.README,
"This Isabelle component provides Vampire " + version + """using the
original sources from """.stripMargin + download_url + """
The executables have been built via "cmake . && make"
Makarius
""" + Date.Format.date(Date.now()) + "\n")
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_vampire", "build prover component from official download",
Scala_Project.here,
{ args =>
var target_dir = Path.current
var download_url = default_download_url
var jobs = default_jobs
var component_name = ""
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_vampire [OPTIONS]
Options are:
-D DIR target directory (default ".")
-U URL download URL
(default: """" + default_download_url + """")
-j NUMBER parallel jobs for make (default: """ + default_jobs + """)
-n NAME component name (default: """" + make_component_name("VERSION") + """")
-v verbose
Build prover component from official download.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => download_url = arg),
"j:" -> (arg => jobs = Value.Nat.parse(arg)),
"n:" -> (arg => component_name = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_vampire(download_url = download_url, component_name = component_name,
jobs = jobs, verbose = verbose, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_verit.scala b/src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala
+++ b/src/Pure/Admin/build_verit.scala
@@ -1,157 +1,157 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
/* platform */
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
error("No 64bit platform")
- val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
+ val platform_dir =
+ Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
val source_name = File.get_dir(tmp_dir)
Isabelle_System.bash(
"tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
- cwd = component_dir.file).check
+ cwd = component_dir.path.file).check
/* build */
progress.echo("Building veriT for " + platform_name + " ...")
val configure_options =
if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else ""
val build_dir = tmp_dir + Path.basic(source_name)
progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"),
cwd = build_dir.file, echo = verbose).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir)
+ Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
val exe_path = Path.basic("veriT").platform_exe
Isabelle_System.copy_file(build_dir + exe_path, platform_dir)
Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw)
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_VERIT="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/veriT"
""")
/* README */
- File.write(component_dir + Path.basic("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,122 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component_name), 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.basic(platform_name))
+ 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)
+ 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 */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ZIPPERPOSITION_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
""")
/* README */
- File.write(component_dir + Path.basic("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,119 +1,116 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
- File.write(component_dir + Path.basic("README"),
+ 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 + Path.basic("LICENSE"), progress = progress)
+ Isabelle_System.download_file(license_url, component_dir.LICENSE, progress = progress)
/* jar */
val jar_name = component_name + ".jar"
- val jar = component_dir + Path.basic(jar_name)
+ 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 =>
progress.echo("Unpacking " + jar)
Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute),
cwd = jar_dir.file).check
- for (platform <- platforms) platform.install(jar_dir, component_dir, version)
+ for (platform <- platforms) platform.install(jar_dir, component_dir.path, version)
}
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
-
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
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,349 +1,374 @@
/* Title: Pure/System/components.scala
Author: Makarius
Isabelle system components.
*/
package isabelle
import java.io.{File => JFile}
object Components {
/* archive name */
object Archive {
val suffix: String = ".tar.gz"
def apply(name: String): String =
if (name == "") error("Bad component name: " + quote(name))
else name + suffix
def unapply(archive: String): Option[String] = {
for {
name0 <- Library.try_unsuffix(suffix, archive)
name <- proper_string(name0)
} yield name
}
def get_name(archive: String): String =
unapply(archive) getOrElse
error("Bad component archive name (expecting .tar.gz): " + quote(archive))
}
/* component collections */
def default_component_repository: String =
Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
def admin(dir: Path): Path = dir + Path.explode("Admin/components")
def contrib(dir: Path = Path.current, name: String = ""): Path =
dir + Path.explode("contrib") + Path.explode(name)
def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = {
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
name
}
def resolve(base_dir: Path, names: List[String],
target_dir: Option[Path] = None,
copy_dir: Option[Path] = None,
progress: Progress = new Progress
): Unit = {
Isabelle_System.make_directory(base_dir)
for (name <- names) {
val archive_name = Archive(name)
val archive = base_dir + Path.explode(archive_name)
if (!archive.is_file) {
val remote = Components.default_component_repository + "/" + archive_name
Isabelle_System.download_file(remote, archive, progress = progress)
}
for (dir <- copy_dir) {
Isabelle_System.make_directory(dir)
Isabelle_System.copy_file(archive, dir)
}
unpack(target_dir getOrElse base_dir, archive, progress = progress)
}
}
private val platforms_family: Map[Platform.Family.Value, Set[String]] =
Map(
Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"),
Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"),
Platform.Family.macos ->
Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"),
Platform.Family.windows ->
Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows"))
private val platforms_all: Set[String] =
Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2)
def purge(dir: Path, platform: Platform.Family.Value): Unit = {
val purge_set = platforms_all -- platforms_family(platform)
File.find_files(dir.file,
(file: JFile) => file.isDirectory && purge_set(file.getName),
include_dirs = true).foreach(Isabelle_System.rm_tree)
}
/* component directories */
def directories(): List[Path] =
Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS"))
/* component directory content */
+ object Directory {
+ def apply(path: Path): Directory = new Directory(path.absolute)
+
+ def create(path: Path, progress: Progress = new Progress): Directory = {
+ val component_dir = new Directory(path.absolute)
+ progress.echo("Creating component directory " + component_dir.path)
+ Isabelle_System.new_directory(component_dir.path)
+ Isabelle_System.make_directory(component_dir.etc)
+ component_dir
+ }
+ }
+
+ class Directory private(val path: Path) {
+ override def toString: String = path.toString
+
+ def etc: Path = path + Path.basic("etc")
+ def src: Path = path + Path.basic("src")
+ def lib: Path = path + Path.basic("lib")
+ def settings: Path = etc + Path.basic("settings")
+ def components: Path = etc + Path.basic("components")
+ def build_props: Path = etc + Path.basic("build.props")
+ def README: Path = path + Path.basic("README")
+ def LICENSE: Path = path + Path.basic("LICENSE")
+ }
+
def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings")
def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components")
def check_dir(dir: Path): Boolean =
settings(dir).is_file || components(dir).is_file
def read_components(dir: Path): List[String] =
split_lines(File.read(components(dir))).filter(_.nonEmpty)
def write_components(dir: Path, lines: List[String]): Unit =
File.write(components(dir), terminate_lines(lines))
/* component repository content */
val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) {
override def toString: String = digest.shasum(name)
}
def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
(proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
Word.explode(line) match {
case Nil => None
case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name))
case _ => error("Bad components.sha1 entry: " + quote(line))
})
def write_components_sha1(entries: List[SHA1_Digest]): Unit =
File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n"))
/** manage user components **/
val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components")
def read_components(): List[String] =
if (components_path.is_file) Library.trim_split_lines(File.read(components_path))
else Nil
def write_components(lines: List[String]): Unit = {
Isabelle_System.make_directory(components_path.dir)
File.write(components_path, Library.terminate_lines(lines))
}
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
val path = path0.expand.absolute
if (!check_dir(path) && !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 (!check_dir(path)) {
error("Malformed component directory: " + path +
"\n (requires " + settings() + " or " + Components.components() + ")")
}
else {
val component_path = path.expand
val archive_dir = component_path.dir
val archive_name = Archive(name)
val archive = archive_dir + Path.explode(archive_name)
if (archive.is_file && !force) {
error("Component archive already exists: " + archive)
}
progress.echo("Packaging " + archive_name)
Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
dir = archive_dir).check
archive
}
}
}
if ((publish && archives.nonEmpty) || update_components_sha1) {
val server = options.string("isabelle_components_server")
if (server.isEmpty) error("Undefined option isabelle_components_server")
using(SSH.open_session(options, server)) { ssh =>
val components_dir = Path.explode(options.string("isabelle_components_dir"))
val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
error("Bad remote directory: " + dir)
}
if (publish) {
for (archive <- archives) {
val archive_name = archive.file_name
val name = Archive.get_name(archive_name)
val remote_component = components_dir + archive.base
val remote_contrib = contrib_dir + Path.explode(name)
// component archive
if (ssh.is_file(remote_component) && !force) {
error("Remote component archive already exists: " + remote_component)
}
progress.echo("Uploading " + archive_name)
ssh.write_file(remote_component, archive)
// contrib directory
val is_standard_component =
Isabelle_System.with_tmp_dir("component") { tmp_dir =>
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
check_dir(tmp_dir + Path.explode(name))
}
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,203 @@
/* 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 =
- target_dir + Path.explode(if (version.isEmpty) "dotnet-latest" else "dotnet-" + version)
+ Components.Directory(
+ target_dir + Path.explode(if (version.isEmpty) "dotnet-latest" else "dotnet-" + version))
if (!dry_run) {
- progress.echo("Component " + component_dir.expand)
+ progress.echo("Component " + component_dir)
+ Isabelle_System.make_directory(component_dir.etc)
- val settings_path = component_dir + Path.explode("etc/settings")
- Isabelle_System.make_directory(settings_path.dir)
- File.write(settings_path, """# -*- shell-script -*- :mode=shellscript:
+ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript:
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 + Path.explode("README"),
+ 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)
+ 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.explode(platform.name)
+ 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.file).check
+ 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,247 +1,246 @@
/* 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 = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.basic(component_name), 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)
+ Isabelle_System.copy_file(build_dir + Path.basic(vsix_name), component_dir.path)
vsix_name
}
/* settings */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
- File.write(etc_dir + Path.basic("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_VSCODE_VSIX="$COMPONENT/""" + vsix_name + "\"\n")
/* README */
- File.write(component_dir + Path.basic("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,477 +1,476 @@
/* Title: Tools/VSCode/src/build_vscodium.scala
Author: Makarius
Build the Isabelle system component for VSCodium: cross-compilation for all
platforms.
*/
package isabelle.vscode
import isabelle._
import java.security.MessageDigest
import java.util.Base64
object Build_VSCodium {
/* global parameters */
lazy val version: String = Isabelle_System.getenv_strict("ISABELLE_VSCODE_VERSION")
val vscodium_repository = "https://github.com/VSCodium/vscodium.git"
val vscodium_download = "https://github.com/VSCodium/vscodium/releases/download"
private val resources = Path.explode("resources")
/* Isabelle symbols (static subset only) */
def make_symbols(): File.Content = {
val symbols = Symbol.Symbols.load(static = true)
val symbols_js =
JSON.Format.pretty_print(
for (entry <- symbols.entries) yield
JSON.Object(
"symbol" -> entry.symbol,
"name" -> entry.name,
"abbrevs" -> entry.abbrevs) ++
JSON.optional("code", entry.code))
File.content(Path.explode("symbols.json"), symbols_js)
}
def make_isabelle_encoding(header: String): File.Content = {
val symbols = Symbol.Symbols.load(static = true)
val symbols_js =
JSON.Format.pretty_print(
for (entry <- symbols.entries; code <- entry.code)
yield JSON.Object("symbol" -> entry.symbol, "code" -> code))
val path = Path.explode("isabelle_encoding.ts")
val body =
File.read(Path.explode("$ISABELLE_VSCODE_HOME/patches") + path)
.replace("[/*symbols*/]", symbols_js)
File.content(path, header + "\n" + body)
}
/* platform info */
sealed case class Platform_Info(
platform: Platform.Family.Value,
download_template: String,
build_name: String,
env: List[String]
) {
def is_linux: Boolean = platform == Platform.Family.linux
def download_name: String = "VSCodium-" + download_template.replace("{VERSION}", version)
def download_zip: Boolean = File.is_zip(download_name)
def download(dir: Path, progress: Progress = new Progress): Unit = {
if (download_zip) Isabelle_System.require_command("unzip", test = "-h")
Isabelle_System.with_tmp_file("download") { download_file =>
Isabelle_System.download_file(vscodium_download + "/" + version + "/" + download_name,
download_file, progress = progress)
progress.echo("Extract ...")
if (download_zip) {
Isabelle_System.bash("unzip -x " + File.bash_path(download_file), cwd = dir.file).check
}
else {
Isabelle_System.gnutar("-xzf " + File.bash_path(download_file), dir = dir).check
}
}
}
def get_vscodium_repository(build_dir: Path, progress: Progress = new Progress): Unit = {
progress.echo("Getting VSCodium repository ...")
Isabelle_System.bash(
List(
"set -e",
"git clone -n " + Bash.string(vscodium_repository) + " .",
"git checkout -q " + Bash.string(version)
).mkString("\n"), cwd = build_dir.file).check
progress.echo("Getting VSCode repository ...")
Isabelle_System.bash(environment + "\n" + "./get_repo.sh", cwd = build_dir.file).check
}
def platform_dir(dir: Path): Path = {
val platform_name =
if (platform == Platform.Family.windows) Platform.Family.native(platform)
else Platform.Family.standard(platform)
dir + Path.explode(platform_name)
}
def build_dir(dir: Path): Path = dir + Path.explode(build_name)
def environment: String =
(("MS_TAG=" + Bash.string(version)) :: "SHOULD_BUILD=yes" :: "VSCODE_ARCH=x64" :: env)
.map(s => "export " + s + "\n").mkString
def patch_sources(base_dir: Path): String = {
val dir = base_dir + Path.explode("vscode")
Isabelle_System.with_copy_dir(dir, dir.orig) {
// macos icns
for (name <- Seq("build/lib/electron.js", "build/lib/electron.ts")) {
File.change(dir + Path.explode(name), strict = true) {
_.replace("""'resources/darwin/' + icon + '.icns'""",
"""'resources/darwin/' + icon.toLowerCase() + '.icns'""")
}
}
// isabelle_encoding.ts
{
val common_dir = dir + Path.explode("src/vs/workbench/services/textfile/common")
val header =
split_lines(File.read(common_dir + Path.explode("encoding.ts")))
.takeWhile(_.trim.nonEmpty)
make_isabelle_encoding(cat_lines(header)).write(common_dir)
}
// explicit patches
{
val patches_dir = Path.explode("$ISABELLE_VSCODE_HOME/patches")
for (name <- Seq("cli", "isabelle_encoding", "no_ocaml_icons")) {
val path = patches_dir + Path.explode(name).patch
Isabelle_System.bash("patch -p1 < " + File.bash_path(path), cwd = dir.file).check
}
}
Isabelle_System.make_patch(base_dir, dir.base.orig, dir.base)
}
}
def patch_resources(base_dir: Path): String = {
val dir = base_dir + resources
val patch =
Isabelle_System.with_copy_dir(dir, dir.orig) {
val fonts_dir = dir + Path.explode("app/out/vs/base/browser/ui/fonts")
HTML.init_fonts(fonts_dir.dir)
make_symbols().write(fonts_dir)
val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css")
val checksum1 = file_checksum(workbench_css)
File.append(workbench_css, "\n\n" + HTML.fonts_css_dir(prefix = "../base/browser/ui"))
val checksum2 = file_checksum(workbench_css)
val file_name = workbench_css.file_name
File.change_lines(dir + Path.explode("app/product.json")) { _.map(line =>
if (line.containsSlice(file_name) && line.contains(checksum1)) {
line.replace(checksum1, checksum2)
}
else line)
}
Isabelle_System.make_patch(dir.dir, dir.orig.base, dir.base)
}
val app_dir = dir + Path.explode("app")
val vscodium_app_dir = dir + Path.explode("vscodium")
Isabelle_System.move_file(app_dir, vscodium_app_dir)
Isabelle_System.make_directory(app_dir)
if ((vscodium_app_dir + resources).is_dir) {
Isabelle_System.copy_dir(vscodium_app_dir + resources, app_dir)
}
patch
}
def init_resources(base_dir: Path): Path = {
val dir = base_dir + resources
if (platform == Platform.Family.macos) {
Isabelle_System.symlink(Path.explode("VSCodium.app/Contents/Resources"), dir)
}
dir
}
def setup_node(target_dir: Path, progress: Progress): Unit = {
Isabelle_System.with_tmp_dir("download") { download_dir =>
download(download_dir, progress = progress)
val dir1 = init_resources(download_dir)
val dir2 = init_resources(target_dir)
for (name <- Seq("app/node_modules.asar", "app/node_modules.asar.unpacked")) {
val path = Path.explode(name)
Isabelle_System.rm_tree(dir2 + path)
Isabelle_System.copy_dir(dir1 + path, dir2 + path)
}
}
}
def setup_electron(dir: Path): Unit = {
val electron = Path.explode("electron")
platform match {
case Platform.Family.linux | Platform.Family.linux_arm =>
Isabelle_System.move_file(dir + Path.explode("codium"), dir + electron)
case Platform.Family.windows =>
Isabelle_System.move_file(dir + Path.explode("VSCodium.exe"), dir + electron.exe)
Isabelle_System.move_file(
dir + Path.explode("VSCodium.VisualElementsManifest.xml"),
dir + Path.explode("electron.VisualElementsManifest.xml"))
case Platform.Family.macos =>
}
}
def setup_executables(dir: Path): Unit = {
Isabelle_System.rm_tree(dir + Path.explode("bin"))
if (platform == Platform.Family.windows) {
val files =
File.find_files(dir.file, pred = { file =>
val name = file.getName
File.is_dll(name) || File.is_exe(name) || File.is_node(name)
})
files.foreach(file => File.set_executable(File.path(file), true))
Isabelle_System.bash("chmod -R o-w " + File.bash_path(dir)).check
}
}
}
// see https://github.com/microsoft/vscode/blob/main/build/gulpfile.vscode.js
// function computeChecksum(filename)
private def file_checksum(path: Path): String = {
val digest = MessageDigest.getInstance("MD5")
digest.update(Bytes.read(path).array)
Bytes(Base64.getEncoder.encode(digest.digest()))
.text.replaceAll("=", "")
}
private val platform_infos: Map[Platform.Family.Value, Platform_Info] =
Iterator(
Platform_Info(Platform.Family.linux, "linux-x64-{VERSION}.tar.gz", "VSCode-linux-x64",
List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True")),
Platform_Info(Platform.Family.linux_arm, "linux-arm64-{VERSION}.tar.gz", "VSCode-linux-arm64",
List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True", "VSCODE_ARCH=arm64")),
Platform_Info(Platform.Family.macos, "darwin-x64-{VERSION}.zip", "VSCode-darwin-x64",
List("OS_NAME=osx")),
Platform_Info(Platform.Family.windows, "win32-x64-{VERSION}.zip", "VSCode-win32-x64",
List("OS_NAME=windows",
"SHOULD_BUILD_ZIP=no",
"SHOULD_BUILD_EXE_SYS=no",
"SHOULD_BUILD_EXE_USR=no",
"SHOULD_BUILD_MSI=no",
"SHOULD_BUILD_MSI_NOUP=no")))
.map(info => info.platform -> info).toMap
def the_platform_info(platform: Platform.Family.Value): Platform_Info =
platform_infos.getOrElse(platform, error("No platform info for " + quote(platform.toString)))
def linux_platform_info: Platform_Info =
the_platform_info(Platform.Family.linux)
/* check system */
def check_system(platforms: List[Platform.Family.Value]): Unit = {
if (Platform.family != Platform.Family.linux) error("Not a Linux/x86_64 system")
Isabelle_System.require_command("git")
Isabelle_System.require_command("node")
Isabelle_System.require_command("yarn")
Isabelle_System.require_command("jq")
if (platforms.contains(Platform.Family.windows)) {
Isabelle_System.require_command("wine")
}
if (platforms.exists(platform => the_platform_info(platform).download_zip)) {
Isabelle_System.require_command("unzip", test = "-h")
}
}
/* original repository clones and patches */
def vscodium_patch(verbose: Boolean = false, progress: Progress = new Progress): String = {
val platform_info = linux_platform_info
check_system(List(platform_info.platform))
Isabelle_System.with_tmp_dir("build") { build_dir =>
platform_info.get_vscodium_repository(build_dir, progress = progress)
val vscode_dir = build_dir + Path.explode("vscode")
progress.echo("Prepare ...")
Isabelle_System.with_copy_dir(vscode_dir, vscode_dir.orig) {
progress.bash(
List(
"set -e",
platform_info.environment,
"./prepare_vscode.sh",
// enforce binary diff of code.xpm
"cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm"
).mkString("\n"), cwd = build_dir.file, echo = verbose).check
Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base,
diff_options = "--exclude=.git --exclude=node_modules")
}
}
}
/* build vscodium */
def default_platforms: List[Platform.Family.Value] = Platform.Family.list
def build_vscodium(
target_dir: Path = Path.current,
platforms: List[Platform.Family.Value] = default_platforms,
verbose: Boolean = false,
progress: Progress = new Progress
): Unit = {
check_system(platforms)
/* component */
val component_name = "vscodium-" + version
- val component_dir = Isabelle_System.new_directory(target_dir + Path.explode(component_name))
- progress.echo("Component " + component_dir)
+ val component_dir =
+ Components.Directory.create(target_dir + Path.explode(component_name), progress = progress)
/* patches */
progress.echo("\n* Building patches:")
- val patches_dir = Isabelle_System.new_directory(component_dir + Path.explode("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)
+ Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
}
- val platform_dir = platform_info.platform_dir(component_dir)
+ 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 */
- val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
- File.write(etc_dir + Path.explode("settings"),
+ File.write(component_dir.settings,
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_VSCODIUM_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then
ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/MacOS/Electron"
ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/Resources"
else
ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/electron"
ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/resources"
fi
""")
/* README */
- File.write(component_dir + Path.explode("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)
})
}