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,207 +1,207 @@
/* 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 => " " + p._1 + "=" + p._2)
.mkString("\n"))
def change(path: Path)
{
def change_line(line: String, entry: (String, String)): String =
line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2)
File.change(path, s =>
split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n"))
}
}
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)
{
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)
/* 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))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download(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
/* 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 */
- File.copy(build_dir + Path.explode("LICENSE"), component_dir)
- File.copy(build_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
+ Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir)
+ 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"),
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_CSDP="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/csdp"
""")
/* README */
File.write(component_dir + Path.basic("README"),
"""This is CSDP """ + version + """ from
""" + download_url + """
Makefile flags have been changed for various platforms as follows:
""" + build_flags.flatMap(_.print).mkString("\n\n") + """
The distribution has been built like this:
cd src && make
Only the bare "solver/csdp" program is used for Isabelle.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
})
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_csdp", "build prover component from official download", Scala_Project.here,
args =>
{
var target_dir = Path.current
var mingw = MinGW.none
var download_url = default_download_url
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_csdp [OPTIONS]
Options are:
-D DIR target directory (default ".")
-M DIR msys/mingw root specification for Windows
-U URL download URL
(default: """" + default_download_url + """")
-v verbose
Build prover component from official download.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"M:" -> (arg => mingw = MinGW(Path.explode(arg))),
"U:" -> (arg => download_url = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_csdp(download_url = download_url, verbose = verbose, progress = progress,
target_dir = target_dir, mingw = mingw)
})
}
diff --git a/src/Pure/Admin/build_e.scala b/src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala
+++ b/src/Pure/Admin/build_e.scala
@@ -1,144 +1,145 @@
/* 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.5"
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)
{
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 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))
/* download source */
val archive_url = download_url + "/V_" + version + "/E.tgz"
val archive_path = tmp_dir + Path.explode("E.tgz")
Isabelle_System.download(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
/* 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 */
- File.copy(build_dir + Path.basic("COPYING"), component_dir + Path.basic("LICENSE"))
+ Isabelle_System.copy_file(build_dir + Path.basic("COPYING"),
+ component_dir + Path.basic("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) File.copy(path, platform_dir)
+ 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"),
"""# -*- shell-script -*- :mode=shellscript:
E_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
E_VERSION=""" + quote(version) + """
""")
/* README */
File.write(component_dir + Path.basic("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_fonts.scala b/src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala
+++ b/src/Pure/Admin/build_fonts.scala
@@ -1,363 +1,363 @@
/* 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
0x2020, // dagger
0x2021, // double dagger
0x2022, // bullet
0x2026, // ellipsis
0x2030, // perthousand
0x2032, // minute
0x2033, // second
0x2038, // caret
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
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)
{
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)
{
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 File.copy(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 = Isabelle_System.make_directory(Components.settings(target_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
- File.copy(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir)
+ 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("uuuuMMdd")(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_jdk.scala b/src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala
+++ b/src/Pure/Admin/build_jdk.scala
@@ -1,239 +1,241 @@
/* 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.pattern.matcher(file_descr).matches) {
val Version = ("^(" + major_version + """\.[0-9.]+\+\d+)(?:-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)
- File.move(jdk_dir, 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)
{
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
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))
- for (platform <- platforms) File.move(dir + platform.platform_path, component_dir)
+ for (platform <- platforms) {
+ Isabelle_System.move_file(dir + platform.platform_path, component_dir)
+ }
for (file <- File.find_files(component_dir.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.ext("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_polyml.scala b/src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala
+++ b/src/Pure/Admin/build_polyml.scala
@@ -1,270 +1,270 @@
/* 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("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include",
"CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64",
"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)
{
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 platform_arch =
if (arch_64) platform.arch_64
else if (platform.is_intel) "x86_64_32"
else platform.arch_32
val polyml_platform = platform_arch + "-" + 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 =
{
progress.bash(mingw.bash_script(script), 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 compiler && make compiler && 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) File.copy(file, 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)
- } File.move(dir + Path.explode(entry), platform_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(platform_dir + Path.explode("polyc"), txt =>
split_lines(txt) match {
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)
cat_lines("#!/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)
{
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) => File.move(component_dir + Path.basic(s), src_dir)
+ 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,
sha1_root: Option[Path] = None)
{
Isabelle_System.new_directory(component_dir)
extract_sources(source_archive, component_dir)
- File.copy(Path.explode("~~/Admin/polyml/README"), component_dir)
+ Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/README"), component_dir)
val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
- File.copy(Path.explode("~~/Admin/polyml/settings"), etc_dir)
+ Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/settings"), etc_dir)
sha1_root match {
case Some(dir) =>
Mercurial.repository(dir).archive(File.standard_path(component_dir + 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 = Isabelle_Platform.self.is_arm
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_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,925 +1,927 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release
{
/** release info **/
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
name: String)
{
def path: Path = Path.explode(name)
}
class Release private[Build_Release](
progress: Progress,
val date: Date,
val dist_name: String,
val dist_dir: Path,
val dist_version: String,
val ident: String)
{
val isabelle_dir: Path = dist_dir + Path.explode(dist_name)
val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
def other_isabelle(dir: Path): Other_Isabelle =
Other_Isabelle(dir + Path.explode(dist_name),
isabelle_identifier = dist_name + "-build",
progress = progress)
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
}
}
/** generated content **/
/* patch release */
private val getsettings_path = Path.explode("lib/scripts/getsettings")
private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
def patch_release(release: Release, is_official: Boolean)
{
val dir = release.isabelle_dir
for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
{
File.change(dir + Path.explode(name),
_.replace("val is_identified = false", "val is_identified = true")
.replace("val is_official = false", "val is_official = " + is_official))
}
File.change(dir + getsettings_path,
_.replace("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
.replace("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
File.change(dir + Path.explode("lib/html/library_index_header.template"),
_.replace("{ISABELLE}", release.dist_name))
for {
name <-
List(
"src/Pure/System/distribution.ML",
"src/Pure/System/distribution.scala",
"lib/Tools/version") }
{
File.change(dir + Path.explode(name), _.replace("repository version", release.dist_version))
}
File.change(dir + Path.explode("README"),
_.replace("some repository version of Isabelle", release.dist_version))
}
/* ANNOUNCE */
def make_announce(release: Release)
{
File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
"""
IMPORTANT NOTE
==============
This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
""")
}
/* NEWS */
def make_news(other_isabelle: Other_Isabelle, dist_version: String)
{
val target = other_isabelle.isabelle_home + Path.explode("doc")
val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts"))
other_isabelle.copy_fonts(target_fonts)
HTML.write_document(target, "NEWS.html",
List(HTML.title("NEWS (" + dist_version + ")")),
List(
HTML.chapter("NEWS"),
HTML.source(
Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
}
/* bundled components */
class Bundled(platform: Option[Platform.Family.Value] = None)
{
def detect(s: String): Boolean =
s.startsWith("#bundled") && !s.startsWith("#bundled ")
def apply(name: String): String =
"#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
private val Pattern1 = ("""^#bundled:(.*)$""").r
private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
def unapply(s: String): Option[String] =
s match {
case Pattern1(name) => Some(name)
case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
case _ => None
}
}
def record_bundled_components(dir: Path)
{
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
default_platform_families.flatMap(platform =>
List(platform.toString, "bundled-" + platform.toString).
map((_, new Bundled(platform = Some(platform)))))
File.append(Components.components(dir),
terminate_lines("#bundled components" ::
(for {
(catalog, bundled) <- catalogs.iterator
path = Components.admin(dir) + Path.basic(catalog)
if path.is_file
line <- split_lines(File.read(path))
if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
} yield bundled(line)).toList))
}
def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
{
val Bundled = new Bundled(platform = Some(platform))
val components =
for {
Bundled(name) <- Components.read_components(dir)
if !name.startsWith("jedit_build")
} yield name
val jdk_component =
components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
(components, jdk_component)
}
def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String])
{
def contrib_name(name: String): String =
Components.contrib(name = name).implode
val Bundled = new Bundled(platform = Some(platform))
Components.write_components(dir,
Components.read_components(dir).flatMap(line =>
line match {
case Bundled(name) =>
if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
}) ::: more_names.map(contrib_name))
}
def make_contrib(dir: Path)
{
Isabelle_System.make_directory(Components.contrib(dir))
File.write(Components.contrib(dir, "README"),
"""This directory contains add-on components that contribute to the main
Isabelle distribution. Separate licensing conditions apply, see each
directory individually.
""")
}
/** build release **/
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
private def execute_tar(dir: Path, args: String): Unit =
Isabelle_System.gnutar(args, dir = dir).check
/* build heaps on remote server */
private def remote_build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path)
{
val server_option = "build_host_" + platform.toString
options.string(server_option) match {
case SSH.Target(user, host) =>
using(SSH.open_session(options, host = host, user = user))(ssh =>
{
Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar =>
{
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
ssh.with_tmp_dir(remote_dir =>
{
val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val remote_commands =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
"./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
"tar -cf tmp.tar heaps")
ssh.execute(remote_commands.mkString(" && ")).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
})
execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
})
})
case s => error("Bad " + server_option + ": " + quote(s))
}
}
/* Isabelle application */
def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n")
{
val title = "# Java runtime options"
File.write(path, (title :: options).map(_ + line_ending).mkString)
}
def make_isabelle_app(
platform: Platform.Family.Value,
isabelle_target: Path,
isabelle_name: String,
jdk_component: String,
classpath: List[Path],
dock_icon: Boolean = false)
{
val script = """#!/usr/bin/env bash
#
# Author: Makarius
#
# Main Isabelle application script.
# minimal Isabelle environment
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
unset "JAVA_TOOL_OPTIONS"
#paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
unset XMODIFIERS
COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """"
source "$COMPONENT/etc/settings"
# main
declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options"))
"$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup"
exec "$ISABELLE_JDK_HOME/bin/java" \
"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
-classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \
"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
""" + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \
""" else "") + """isabelle.Main "$@"
"""
val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
File.write(script_path, script)
File.set_executable(script_path, true)
val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app")
- File.move(
+ Isabelle_System.move_file(
component_dir + Path.explode(Platform.standard_platform(platform)) + Path.explode("Isabelle"),
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(component_dir)
}
def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String)
{
File.write(path, """
CFBundleDevelopmentRegion
English
CFBundleIconFile
isabelle.icns
CFBundleIdentifier
de.tum.in.isabelle
CFBundleDisplayName
""" + isabelle_name + """
CFBundleInfoDictionaryVersion
6.0
CFBundleName
""" + isabelle_name + """
CFBundlePackageType
APPL
CFBundleShortVersionString
""" + isabelle_name + """
CFBundleSignature
????
CFBundleVersion
""" + isabelle_rev + """
NSHumanReadableCopyright
LSMinimumSystemVersion
10.11
LSApplicationCategoryType
public.app-category.developer-tools
NSHighResolutionCapable
true
NSSupportsAutomaticGraphicsSwitching
true
CFBundleDocumentTypes
CFBundleTypeExtensions
thy
CFBundleTypeIconFile
theory.icns
CFBundleTypeName
Isabelle theory file
CFBundleTypeRole
Editor
LSTypeIsPackage
""")
}
/* main */
private val default_platform_families: List[Platform.Family.Value] =
List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
def build_release(base_dir: Path,
options: Options,
components_base: Path = Components.default_components_base,
progress: Progress = new Progress,
rev: String = "",
afp_rev: String = "",
official_release: Boolean = false,
proper_release_name: Option[String] = None,
platform_families: List[Platform.Family.Value] = default_platform_families,
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_sessions: List[String] = Nil,
build_library: Boolean = false,
parallel_jobs: Int = 1): Release =
{
val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
val release =
{
val date = Date.now()
val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
val ident =
try { hg.id(version) }
catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
val dist_version =
proper_release_name match {
case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
}
new Release(progress, date, dist_name, dist_dir, dist_version, ident)
}
/* make distribution */
if (release.isabelle_archive.is_file) {
progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
val archive_ident =
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val getsettings = Path.explode(release.dist_name) + getsettings_path
execute_tar(tmp_dir, "-xzf " +
File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
split_lines(File.read(tmp_dir + getsettings))
.collectFirst({ case ISABELLE_ID(ident) => ident })
.getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive))
})
if (release.ident != archive_ident) {
error("Mismatch of release identification " + release.ident +
" vs. archive " + archive_ident)
}
}
else {
progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
Isabelle_System.make_directory(release.dist_dir)
if (release.isabelle_dir.is_dir)
error("Directory " + release.isabelle_dir + " already exists")
progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
(release.isabelle_dir + Path.explode(name)).file.delete
}
progress.echo_warning("Preparing distribution " + quote(release.dist_name))
patch_release(release, proper_release_name.isDefined && official_release)
if (proper_release_name.isEmpty) make_announce(release)
make_contrib(release.isabelle_dir)
execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(release.isabelle_dir)
/* build tools and documentation */
val other_isabelle = release.other_isabelle(release.dist_dir)
other_isabelle.init_settings(
other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
other_isabelle.resolve_components(echo = true)
try {
val export_classpath =
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
try {
other_isabelle.bash(
"./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
make_news(other_isabelle, release.dist_version)
for (name <- List("Admin", "browser_info", "heaps")) {
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
}
other_isabelle.cleanup()
progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
def execute_dist_name(script: String): Unit =
Isabelle_System.bash(script, cwd = release.dist_dir.file,
env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
execute_dist_name("""
set -e
chmod -R a+r "$DIST_NAME"
chmod -R u+w "$DIST_NAME"
chmod -R g=o "$DIST_NAME"
find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
""")
execute_tar(release.dist_dir, "-czf " +
File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
execute_dist_name("""
set -e
mv "$DIST_NAME" "${DIST_NAME}-old"
mkdir "$DIST_NAME"
mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
"${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
mkdir "$DIST_NAME/doc"
mv "${DIST_NAME}-old/doc/"*.pdf \
"${DIST_NAME}-old/doc/"*.html \
"${DIST_NAME}-old/doc/"*.css \
"${DIST_NAME}-old/doc/fonts" \
"${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
rm -rf "${DIST_NAME}-old"
""")
}
/* make application bundles */
val bundle_infos = platform_families.map(release.bundle_info)
for (bundle_info <- bundle_infos) {
val isabelle_name = release.dist_name
val platform = bundle_info.platform
progress.echo("\nApplication bundle for " + platform)
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
// release archive
execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
val other_isabelle = release.other_isabelle(tmp_dir)
val isabelle_target = other_isabelle.isabelle_home
// bundled components
progress.echo("Bundled components:")
val contrib_dir = Components.contrib(isabelle_target)
val (bundled_components, jdk_component) =
get_bundled_components(isabelle_target, platform)
Components.resolve(components_base, bundled_components,
target_dir = Some(contrib_dir),
copy_dir = Some(release.dist_dir + Path.explode("contrib")),
progress = progress)
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
Components.purge(contrib_dir, platform)
activate_components(isabelle_target, platform, more_components_names)
// Java parameters
val java_options: List[String] =
(for {
variable <-
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_OPTIONS")
opt <- Word.explode(other_isabelle.getenv(variable))
}
yield {
val s = "-Dapple.awt.application.name="
if (opt.startsWith(s)) s + isabelle_name else opt
}) ::: List("-Disabelle.jedit_server=" + isabelle_name)
val classpath: List[Path] =
{
val base = isabelle_target.absolute
Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
{
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
}
}) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
progress.echo("Building heaps ...")
remote_build_heaps(options, platform, build_sessions, isabelle_target)
}
// application bundling
platform match {
case Platform.Family.linux =>
File.change(isabelle_target + jedit_options,
_.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
File.change(isabelle_target + jedit_props,
_.replaceAll("console.fontsize=.*", "console.fontsize=18")
.replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
.replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
.replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
.replaceAll("view.fontsize=.*", "view.fontsize=24")
.replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
make_isabelle_options(
isabelle_target + Path.explode("Isabelle.options"), java_options)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath)
val archive_name = isabelle_name + "_linux.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
Bash.string(isabelle_name))
case Platform.Family.macos =>
File.change(isabelle_target + jedit_props,
_.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
.replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
// macOS application bundle
val app_contents = isabelle_target + Path.explode("Contents")
for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
- File.copy(isabelle_target + Path.explode(icon),
+ Isabelle_System.copy_file(isabelle_target + Path.explode(icon),
Isabelle_System.make_directory(app_contents + Path.explode("Resources")))
}
make_isabelle_plist(
app_contents + Path.explode("Info.plist"), isabelle_name, release.ident)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
classpath, dock_icon = true)
val isabelle_options = Path.explode("Isabelle.options")
make_isabelle_options(
isabelle_target + isabelle_options,
java_options ::: List("-Disabelle.app=true"))
// application archive
val archive_name = isabelle_name + "_macos.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
val isabelle_app = Path.explode(isabelle_name + ".app")
- File.move(tmp_dir + Path.explode(isabelle_name), tmp_dir + isabelle_app)
+ Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name),
+ tmp_dir + isabelle_app)
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
File.bash_path(isabelle_app))
case Platform.Family.windows =>
File.change(isabelle_target + jedit_props,
_.replaceAll("foldPainter=.*", "foldPainter=Square"))
// application launcher
- File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
+ Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
val app_template = Path.explode("~~/Admin/Windows/launch4j")
make_isabelle_options(
isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
java_options, line_ending = "\r\n")
val isabelle_xml = Path.explode("isabelle.xml")
val isabelle_exe = Path.explode(isabelle_name + ".exe")
File.write(tmp_dir + isabelle_xml,
File.read(app_template + isabelle_xml)
.replace("{ISABELLE_NAME}", isabelle_name)
.replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
.replace("{ICON}",
File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
.replace("{SPLASH}",
File.platform_path(app_template + Path.explode("isabelle.bmp")))
.replace("{CLASSPATH}",
cat_lines(classpath.map(cp =>
" %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
.replace("\\jdk\\", "\\" + jdk_component + "\\"))
execute(tmp_dir,
"\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
- File.copy(app_template + Path.explode("manifest.xml"),
+ Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
isabelle_target + isabelle_exe.ext("manifest"))
// Cygwin setup
val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
- File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
+ Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"),
+ isabelle_target)
val cygwin_mirror =
File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
val cygwin_bat = Path.explode("Cygwin-Setup.bat")
File.write(isabelle_target + cygwin_bat,
File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror))
File.set_executable(isabelle_target + cygwin_bat, true)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
- File.copy(cygwin_template + path,
+ Isabelle_System.copy_file(cygwin_template + path,
isabelle_target + Path.explode("contrib/cygwin") + path)
}
execute(isabelle_target,
"""find . -type f -not -name "*.exe" -not -name "*.dll" """ +
(if (Platform.is_macos) "-perm +100" else "-executable") +
" -print0 > contrib/cygwin/isabelle/executables")
execute(isabelle_target,
"""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
"""> contrib/cygwin/isabelle/symlinks""")
execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
// executable archive (self-extracting 7z)
val archive_name = isabelle_name + ".7z"
val exe_archive = tmp_dir + Path.explode(archive_name)
exe_archive.file.delete
progress.echo("Packaging " + archive_name + " ...")
execute(tmp_dir,
"7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
val sfx_txt =
File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt"))
.replace("{ISABELLE_NAME}", isabelle_name)
Bytes.write(release.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.set_executable(release.dist_dir + isabelle_exe, true)
}
})
progress.echo("DONE")
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
if (release.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident,
HTML.text("Isabelle/" + release.ident))
val afp_link =
HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev))
HTML.write_document(dir, "index.html",
List(HTML.title(release.dist_name)),
List(
HTML.section(release.dist_name),
HTML.subsection("Platforms"),
HTML.itemize(
website_platform_bundles.map({ case (bundle, bundle_info) =>
List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })),
HTML.subsection("Repositories"),
HTML.itemize(
List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
for ((bundle, _) <- website_platform_bundles)
- File.copy(release.dist_dir + Path.explode(bundle), dir)
+ Isabelle_System.copy_file(release.dist_dir + Path.explode(bundle), dir)
}
/* HTML library */
if (build_library) {
if (release.isabelle_library_archive.is_file) {
progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
}
else {
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val bundle =
release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle = release.other_isabelle(tmp_dir)
Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
other_isabelle.isabelle_home_user.file.delete
execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
" " + Bash.string(release.dist_name + "/browser_info"))
})
}
}
release
}
/** command line entry point **/
def main(args: Array[String])
{
Command_Line.tool {
var afp_rev = ""
var components_base: Path = Components.default_components_base
var official_release = false
var proper_release_name: Option[String] = None
var website: Option[Path] = None
var build_sessions: List[String] = Nil
var more_components: List[Path] = Nil
var parallel_jobs = 1
var build_library = false
var options = Options.init()
var platform_families = default_platform_families
var rev = ""
val getopts = Getopts("""
Usage: Admin/build_release [OPTIONS] BASE_DIR
Options are:
-A REV corresponding AFP changeset id
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-O official release (not release-candidate)
-R RELEASE proper release with name
-W WEBSITE produce minimal website in given directory
-b SESSIONS build platform-specific session images (separated by commas)
-c ARCHIVE clean bundling with additional component .tar.gz archive
-j INT maximum number of parallel jobs (default 1)
-l build library
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NAMES platform families (default: """ + default_platform_families.mkString(",") + """)
-r REV Mercurial changeset id (default: RELEASE or tip)
Build Isabelle release in base directory, using the local repository clone.
""",
"A:" -> (arg => afp_rev = arg),
"C:" -> (arg => components_base = Path.explode(arg)),
"O" -> (_ => official_release = true),
"R:" -> (arg => proper_release_name = Some(arg)),
"W:" -> (arg => website = Some(Path.explode(arg))),
"b:" -> (arg => build_sessions = space_explode(',', arg)),
"c:" -> (arg =>
{
val path = Path.explode(arg)
Components.Archive.get_name(path.file_name)
more_components = more_components ::: List(path)
}),
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
"l" -> (_ => build_library = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
"r:" -> (arg => rev = arg))
val more_args = getopts(args)
val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() }
val progress = new Console_Progress()
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
build_release(Path.explode(base_dir), options, components_base = components_base,
progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release,
proper_release_name = proper_release_name, website = website,
platform_families =
if (platform_families.isEmpty) default_platform_families
else platform_families,
more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs)
}
}
}
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,180 @@
/* 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)
{
Isabelle_System.with_tmp_dir("build")(tmp_dir =>
{
Isabelle_System.require_command("bison", "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 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))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download(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
/* 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 */
- File.copy(build_dir + Path.basic("LICENCE"), component_dir + Path.basic("LICENSE"))
+ Isabelle_System.copy_file(build_dir + Path.basic("LICENCE"),
+ component_dir + Path.basic("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) File.copy(path, platform_dir)
+ 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"),
"""# -*- shell-script -*- :mode=shellscript:
SPASS_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
SPASS_VERSION=""" + quote(version) + """
""")
/* README */
File.write(component_dir + Path.basic("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,115 +1,115 @@
/* 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)
{
val Download_Name = """^.*/([^/]+)\.jar""".r
val download_name =
download_url match {
case Download_Name(download_name) => download_name
case _ => error("Malformed jar download URL: " + quote(download_url))
}
/* component */
val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(download_name))
progress.echo("Component " + component_dir)
/* README */
File.write(component_dir + Path.basic("README"),
"This is " + download_name + " from\n" + download_url +
"\n\n Makarius\n " + Date.Format.date(Date.now()) + "\n")
/* settings */
val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
File.write(etc_dir + Path.basic("settings"),
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_SQLITE_HOME="$COMPONENT"
classpath "$ISABELLE_SQLITE_HOME/""" + download_name + """.jar"
""")
/* jar */
val jar = component_dir + Path.basic(download_name).ext("jar")
Isabelle_System.download(download_url, jar, progress = progress)
Isabelle_System.with_tmp_dir("sqlite")(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))
- File.copy(jar_dir + Path.explode(file), target)
+ Isabelle_System.copy_file(jar_dir + Path.explode(file), target)
}
File.set_executable(component_dir + Path.explode("x86_64-windows/sqlitejdbc.dll"), true)
})
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_sqlite", "build Isabelle sqlite-jdbc component from official download",
Scala_Project.here, args =>
{
var target_dir = Path.current
val getopts = Getopts("""
Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD
Options are:
-D DIR target directory (default ".")
Build sqlite-jdbc component from the specified download URL (JAR), see also
https://github.com/xerial/sqlite-jdbc and
https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
""",
"D:" -> (arg => target_dir = Path.explode(arg)))
val more_args = getopts(args)
val download_url =
more_args match {
case List(download_url) => download_url
case _ => getopts.usage()
}
val progress = new Console_Progress()
build_sqlite(download_url, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/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,171 +1,171 @@
/* Title: Pure/Admin/build_vampire.scala
Author: Makarius
Build Isabelle Vampire component from repository.
*/
package isabelle
object Build_Vampire
{
val default_repository = "https://github.com/vprover/vampire.git"
val default_version1 = "4.5.1"
val default_version2 = "df87588848db"
val default_jobs = 1
def make_component_name(version: String) = "vampire-" + version
/* build Vampire */
def build_vampire(
repository: String = default_repository,
version1: String = default_version1,
version2: String = default_version2,
jobs: Int = default_jobs,
component_name: String = "",
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current)
{
Isabelle_System.require_command("git", "cmake")
Isabelle_System.with_tmp_dir("build")(tmp_dir =>
{
/* component and platform */
val component = proper_string(component_name) getOrElse make_component_name(version1)
val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
progress.echo("Component " + component_dir)
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))
/* clone repository */
progress.echo("Cloning repository " + repository)
progress.bash("git clone " + Bash.string(repository) + " vampire",
cwd = tmp_dir.file, echo = verbose).check
val source_dir = tmp_dir + Path.explode("vampire")
- File.copy(source_dir + Path.explode("LICENCE"), component_dir)
+ Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir)
/* build versions */
for { (rev, exe) <- List(version1 -> "vampire", version2 -> "vampire_polymorphic") } {
progress.echo("Building " + exe + " (rev " + rev + ")")
progress.bash("git checkout --quiet --detach " + Bash.string(rev),
cwd = source_dir.file, echo = verbose).check
val build_dir = source_dir + Path.explode("build")
Isabelle_System.rm_tree(build_dir)
Isabelle_System.make_directory(build_dir)
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
- File.copy(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
+ Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
platform_dir + Path.basic(exe).platform_exe)
}
/* settings */
val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
File.write(etc_dir + Path.basic("settings"),
"""# -*- shell-script -*- :mode=shellscript:
VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire"
ISABELLE_VAMPIRE_POLYMORPHIC="$VAMPIRE_HOME/vampire_polymorphic"
VAMPIRE_EXTRA_OPTIONS=""
""")
/* README */
File.write(component_dir + Path.basic("README"),
"This Isabelle component provides two versions of Vampire from\n" + repository + """
* vampire: standard version (regular stable release)
* vampire_polymorphic: special version for polymorphic FOL and HOL
(intermediate repository version)
The executables have been built like this:
git checkout COMMIT
cmake .
make
The precise commit id is revealed by executing "vampire --version".
Makarius
""" + Date.Format.date(Date.now()) + "\n")
})
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_vampire", "build prover component from repository", Scala_Project.here,
args =>
{
var target_dir = Path.current
var repository = default_repository
var version1 = default_version1
var version2 = default_version2
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 repository (default: """" + default_repository + """")
-V REV1 standard version (default: """" + default_version1 + """")
-W REV2 polymorphic version (default: """" + default_version2 + """")
-j NUMBER parallel jobs for make (default: """ + default_jobs + """)
-n NAME component name (default: """" + make_component_name("REV1") + """")
-v verbose
Build prover component from official download.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => repository = arg),
"V:" -> (arg => version1 = arg),
"W:" -> (arg => version2 = 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(repository = repository, version1 = version1, version2 = version2,
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,159 +1,159 @@
/* 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/2020.10/verit-2020.10-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)
{
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)
/* 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))
/* download source */
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download(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
/* 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 */
- File.copy(build_dir + Path.explode("LICENSE"), component_dir)
+ Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir)
val exe_path = Path.basic("veriT").platform_exe
- File.copy(build_dir + exe_path, platform_dir)
+ 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"),
"""# -*- shell-script -*- :mode=shellscript:
ISABELLE_VERIT="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/veriT"
""")
/* README */
File.write(component_dir + Path.basic("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,123 +1,124 @@
/* Title: Pure/Admin/build_zipperposition.scala
Author: Makarius
Build Isabelle Zipperposition component from OPAM repository.
*/
package isabelle
object Build_Zipperposition
{
val default_version = "2.0"
/* build Zipperposition */
def build_zipperposition(
version: String = default_version,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current)
{
Isabelle_System.with_tmp_dir("build")(build_dir =>
{
if (!Platform.is_windows) 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)
/* 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))
/* 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 */
- File.copy(build_dir + Path.explode("doc/zipperposition/LICENSE"), component_dir)
+ Isabelle_System.copy_file(build_dir + Path.explode("doc/zipperposition/LICENSE"),
+ component_dir)
val prg_path = Path.basic("zipperposition")
val exe_path = prg_path.platform_exe
- File.copy(build_dir + Path.basic("bin") + prg_path, platform_dir + exe_path)
+ 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"),
"""# -*- shell-script -*- :mode=shellscript:
ZIPPERPOSITION_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
""")
/* README */
File.write(component_dir + Path.basic("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/components.scala b/src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala
+++ b/src/Pure/Admin/components.scala
@@ -1,354 +1,354 @@
/* Title: Pure/Admin/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)
{
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
progress.echo("Getting " + remote)
Bytes.write(archive, Url.read_bytes(Url(remote)))
}
for (dir <- copy_dir) {
Isabelle_System.make_directory(dir)
- File.copy(archive, dir)
+ Isabelle_System.copy_file(archive, dir)
}
unpack(target_dir getOrElse base_dir, archive, progress = progress)
}
}
def purge(dir: Path, platform: Platform.Family.Value)
{
def purge_platforms(platforms: String*): Set[String] =
platforms.flatMap(name =>
List("arm64-" + name, "x86-" + name, "x86_64_32-" + name, "x86_64-" + name)).toSet +
"ppc-darwin" + "arm64-linux"
val purge_set =
platform match {
case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows")
case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows")
case Platform.Family.windows => purge_platforms("linux", "darwin")
}
File.find_files(dir.file,
(file: JFile) => file.isDirectory && purge_set(file.getName),
include_dirs = true).foreach(Isabelle_System.rm_tree)
}
/* component directory content */
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(sha1: String, file_name: String)
{
override def toString: String = sha1 + " " + file_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, name))
case _ => error("Bad components.sha1 entry: " + quote(line))
})
def write_components_sha1(entries: List[SHA1_Digest]): Unit =
File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n"))
/** manage user components **/
val components_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 (!(path + Path.explode("etc/settings")).is_file &&
!(path + Path.explode("etc/components")).is_file) 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)
{
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) {
options.string("isabelle_components_server") match {
case SSH.Target(user, host) =>
using(SSH.open_session(options, host = host, user = user))(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 entry.is_file && entry.name.endsWith(Archive.suffix)
}
yield {
progress.echo("Digesting remote " + entry.name)
ssh.execute("cd " + ssh.bash_path(components_dir) +
"; sha1sum " + Bash.string(entry.name)).check.out
}
write_components_sha1(read_components_sha1(lines))
}
})
case s => error("Bad isabelle_components_server: " + quote(s))
}
}
// local SHA1 digests
{
val new_entries =
for (archive <- archives)
yield {
val file_name = archive.file_name
progress.echo("Digesting local " + file_name)
val sha1 = SHA1.digest(archive).rep
SHA1_Digest(sha1, file_name)
}
val new_names = new_entries.map(_.file_name).toSet
write_components_sha1(
new_entries :::
read_components_sha1().filterNot(entry => new_names.contains(entry.file_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.map(name => options.options(name).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.prefix_lines(" ", 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/Admin/other_isabelle.scala b/src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala
+++ b/src/Pure/Admin/other_isabelle.scala
@@ -1,120 +1,120 @@
/* Title: Pure/Admin/other_isabelle.scala
Author: Makarius
Manage other Isabelle distributions.
*/
package isabelle
object Other_Isabelle
{
def apply(isabelle_home: Path,
isabelle_identifier: String = "",
user_home: Path = Path.explode("$USER_HOME"),
progress: Progress = new Progress): Other_Isabelle =
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
}
class Other_Isabelle(
val isabelle_home: Path,
val isabelle_identifier: String,
user_home: Path,
progress: Progress)
{
other_isabelle =>
override def toString: String = isabelle_home.toString
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
/* static system */
def bash(
script: String,
redirect: Boolean = false,
echo: Boolean = false,
strict: Boolean = true): Process_Result =
progress.bash(
"export USER_HOME=" + File.bash_path(user_home) + "\n" +
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
def apply(
cmdline: String,
redirect: Boolean = false,
echo: Boolean = false,
strict: Boolean = true): Process_Result =
bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
def resolve_components(echo: Boolean): Unit =
other_isabelle(
"env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) +
" isabelle components -a", redirect = true, echo = echo).check
def getenv(name: String): String =
other_isabelle("getenv -b " + Bash.string(name)).check.out
val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
val etc: Path = isabelle_home_user + Path.explode("etc")
val etc_settings: Path = etc + Path.explode("settings")
val etc_preferences: Path = etc + Path.explode("preferences")
def copy_fonts(target_dir: Path): Unit =
Isabelle_Fonts.make_entries(getenv = getenv, hidden = true).
- foreach(entry => File.copy(entry.path, target_dir))
+ foreach(entry => Isabelle_System.copy_file(entry.path, target_dir))
/* components */
def init_components(
component_repository: String = Components.default_component_repository,
components_base: Path = Components.default_components_base,
catalogs: List[String] = Nil,
components: List[String] = Nil): List[String] =
{
val dir = Components.admin(isabelle_home)
("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) ::
catalogs.map(name =>
"init_components " + File.bash_path(components_base) + " " +
File.bash_path(dir + Path.basic(name))) :::
components.map(name =>
"init_component " + File.bash_path(components_base + Path.basic(name)))
}
/* settings */
def clean_settings(): Boolean =
if (!etc_settings.is_file) true
else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
etc_settings.file.delete; true
}
else false
def init_settings(settings: List[String])
{
if (!clean_settings())
error("Cannot proceed with existing user settings file: " + etc_settings)
Isabelle_System.make_directory(etc_settings.dir)
File.write(etc_settings,
"# generated by Isabelle " + Date.now() + "\n" +
"#-*- shell-script -*- :mode=shellscript:\n" +
settings.mkString("\n", "\n", "\n"))
}
/* cleanup */
def cleanup()
{
clean_settings()
etc.file.delete
isabelle_home_user.file.delete
}
}
diff --git a/src/Pure/General/file.scala b/src/Pure/General/file.scala
--- a/src/Pure/General/file.scala
+++ b/src/Pure/General/file.scala
@@ -1,381 +1,327 @@
/* Title: Pure/General/file.scala
Author: Makarius
File-system operations.
*/
package isabelle
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
InputStreamReader, File => JFile, IOException}
-import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
- Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException}
+import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
+ FileVisitOption, FileVisitResult}
import java.nio.file.attribute.BasicFileAttributes
import java.net.{URL, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import java.util.regex.Pattern
import java.util.EnumSet
import org.tukaani.xz.{XZInputStream, XZOutputStream}
import scala.collection.mutable
import scala.util.matching.Regex
object File
{
/* standard path (Cygwin or Posix) */
def standard_path(path: Path): String = path.expand.implode
def standard_path(platform_path: String): String =
if (Platform.is_windows) {
val Platform_Root = new Regex("(?i)" +
Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
platform_path.replace('/', '\\') match {
case Platform_Root(rest) => "/" + rest.replace('\\', '/')
case Drive(letter, rest) =>
"/cygdrive/" + Word.lowercase(letter) +
(if (rest == "") "" else "/" + rest.replace('\\', '/'))
case path => path.replace('\\', '/')
}
}
else platform_path
def standard_path(file: JFile): String = standard_path(file.getPath)
def standard_url(name: String): String =
try {
val url = new URL(name)
if (url.getProtocol == "file" && Url.is_wellformed_file(name))
standard_path(Url.parse_file(name))
else name
}
catch { case _: MalformedURLException => standard_path(name) }
/* platform path (Windows or Posix) */
private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
private val Named_Root = new Regex("//+([^/]*)(.*)")
def platform_path(standard_path: String): String =
if (Platform.is_windows) {
val result_path = new StringBuilder
val rest =
standard_path match {
case Cygdrive(drive, rest) =>
result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
rest
case Named_Root(root, rest) =>
result_path ++= JFile.separator
result_path ++= JFile.separator
result_path ++= root
rest
case path if path.startsWith("/") =>
result_path ++= Isabelle_System.cygwin_root()
path
case path => path
}
for (p <- space_explode('/', rest) if p != "") {
val len = result_path.length
if (len > 0 && result_path(len - 1) != JFile.separatorChar)
result_path += JFile.separatorChar
result_path ++= p
}
result_path.toString
}
else standard_path
def platform_path(path: Path): String = platform_path(standard_path(path))
def platform_file(path: Path): JFile = new JFile(platform_path(path))
/* platform files */
def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
def absolute_name(file: JFile): String = absolute(file).getPath
def canonical(file: JFile): JFile = file.getCanonicalFile
def canonical_name(file: JFile): String = canonical(file).getPath
def path(file: JFile): Path = Path.explode(standard_path(file))
def pwd(): Path = path(Path.current.absolute_file)
/* relative paths */
def relative_path(base: Path, other: Path): Option[Path] =
{
val base_path = base.file.toPath
val other_path = other.file.toPath
if (other_path.startsWith(base_path))
Some(path(base_path.relativize(other_path).toFile))
else None
}
/* bash path */
def bash_path(path: Path): String = Bash.string(standard_path(path))
def bash_path(file: JFile): String = Bash.string(standard_path(file))
def bash_platform_path(path: Path): String = Bash.string(platform_path(path))
/* directory entries */
def check_dir(path: Path): Path =
if (path.is_dir) path else error("No such directory: " + path)
def check_file(path: Path): Path =
if (path.is_file) path else error("No such file: " + path)
/* directory content */
def read_dir(dir: Path): List[String] =
{
if (!dir.is_dir) error("No such directory: " + dir.toString)
val files = dir.file.listFiles
if (files == null) Nil
else files.toList.map(_.getName).sorted
}
def get_dir(dir: Path): String =
read_dir(dir).filter(name => (dir + Path.basic(name)).is_dir) match {
case List(entry) => entry
case dirs =>
error("Exactly one directory entry expected: " + commas_quote(dirs.sorted))
}
def find_files(
start: JFile,
pred: JFile => Boolean = _ => true,
include_dirs: Boolean = false,
follow_links: Boolean = false): List[JFile] =
{
val result = new mutable.ListBuffer[JFile]
def check(file: JFile) { if (pred(file)) result += file }
if (start.isFile) check(start)
else if (start.isDirectory) {
val options =
if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS)
else EnumSet.noneOf(classOf[FileVisitOption])
Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE,
new SimpleFileVisitor[JPath] {
override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
{
if (include_dirs) check(path.toFile)
FileVisitResult.CONTINUE
}
override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
{
val file = path.toFile
if (include_dirs || !file.isDirectory) check(file)
FileVisitResult.CONTINUE
}
}
)
}
result.toList
}
/* read */
def read(file: JFile): String = Bytes.read(file).text
def read(path: Path): String = read(path.file)
def read_stream(reader: BufferedReader): String =
{
val output = new StringBuilder(100)
var c = -1
while ({ c = reader.read; c != -1 }) output += c.toChar
reader.close
output.toString
}
def read_stream(stream: InputStream): String =
read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
def read_gzip(file: JFile): String =
read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
def read_gzip(path: Path): String = read_gzip(path.file)
def read_xz(file: JFile): String =
read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
def read_xz(path: Path): String = read_xz(path.file)
/* read lines */
def read_line(reader: BufferedReader): Option[String] =
{
val line =
try { reader.readLine}
catch { case _: IOException => null }
Option(line).map(Library.trim_line)
}
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
{
val result = new mutable.ListBuffer[String]
var line: Option[String] = None
while ({ line = read_line(reader); line.isDefined }) {
progress(line.get)
result += line.get
}
reader.close
result.toList
}
/* write */
def writer(file: JFile): BufferedWriter =
new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset))
def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
{
val stream = make_stream(new FileOutputStream(file))
using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text))
}
def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s)
def write(path: Path, text: CharSequence): Unit = write(path.file, text)
def write_gzip(file: JFile, text: CharSequence): Unit =
write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit =
File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options())
def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit =
write_xz(path.file, text, options)
def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options())
def write_backup(path: Path, text: CharSequence)
{
- if (path.is_file) move(path, path.backup)
+ if (path.is_file) Isabelle_System.move_file(path, path.backup)
write(path, text)
}
def write_backup2(path: Path, text: CharSequence)
{
- if (path.is_file) move(path, path.backup2)
+ if (path.is_file) Isabelle_System.move_file(path, path.backup2)
write(path, text)
}
/* change */
def change(file: JFile, f: String => String): Unit = write(file, f(read(file)))
def change(path: Path, f: String => String): Unit = write(path, f(read(path)))
/* append */
def append(file: JFile, text: CharSequence): Unit =
Files.write(file.toPath, UTF8.bytes(text.toString),
StandardOpenOption.APPEND, StandardOpenOption.CREATE)
def append(path: Path, text: CharSequence): Unit = append(path.file, text)
/* eq */
def eq(file1: JFile, file2: JFile): Boolean =
try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) }
catch { case ERROR(_) => false }
def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)
/* eq_content */
def eq_content(file1: JFile, file2: JFile): Boolean =
if (eq(file1, file2)) true
else if (file1.length != file2.length) false
else Bytes.read(file1) == Bytes.read(file2)
def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file)
- /* copy */
-
- def copy(src: JFile, dst: JFile)
- {
- val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
- if (!eq(src, target))
- Files.copy(src.toPath, target.toPath,
- StandardCopyOption.COPY_ATTRIBUTES,
- StandardCopyOption.REPLACE_EXISTING)
- }
-
- def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
-
- def copy_base(base_dir: Path, src0: Path, target_dir: Path)
- {
- val src = src0.expand
- val src_dir = src.dir
- if (!src.starts_basic) error("Illegal path specification " + src + " beyond base directory")
- copy(base_dir + src, Isabelle_System.make_directory(target_dir + src_dir))
- }
-
-
- /* move */
-
- def move(src: JFile, dst: JFile)
- {
- val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
- if (!eq(src, target))
- Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
- }
-
- def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file)
-
-
- /* symbolic link */
-
- def link(src: Path, dst: Path, force: Boolean = false)
- {
- val src_file = src.file
- val dst_file = dst.file
- val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
-
- if (force) target.delete
-
- try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
- catch {
- case _: UnsupportedOperationException if Platform.is_windows =>
- Cygwin.link(standard_path(src), target)
- case _: FileSystemException if Platform.is_windows =>
- Cygwin.link(standard_path(src), target)
- }
- }
-
-
/* permissions */
def is_executable(path: Path): Boolean =
{
if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok
else path.file.canExecute
}
def set_executable(path: Path, flag: Boolean)
{
if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path)
else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
else path.file.setExecutable(flag, false)
}
}
diff --git a/src/Pure/System/executable.scala b/src/Pure/System/executable.scala
--- a/src/Pure/System/executable.scala
+++ b/src/Pure/System/executable.scala
@@ -1,78 +1,78 @@
/* Title: Pure/System/executable.scala
Author: Makarius
Support for platform-specific executables.
*/
package isabelle
object Executable
{
def libraries_closure(path: Path,
mingw: MinGW = MinGW.none,
filter: String => Boolean = _ => true,
patchelf: Boolean = false): List[String] =
{
val exe_path = path.expand
val exe_dir = exe_path.dir
val exe = exe_path.base
val ldd_lines =
{
val ldd = if (Platform.is_macos) "otool -L" else "ldd"
val script = mingw.bash_script(ldd + " " + File.bash_path(exe))
Library.split_lines(Isabelle_System.bash(script, cwd = exe_dir.file).check.out)
}
def lib_name(lib: String): String =
Library.take_prefix[Char](c => c != '.' && c != '-',
Library.take_suffix[Char](_ != '/', lib.toList)._2)._1.mkString
val libs =
if (Platform.is_macos) {
val Pattern = """^\s*(/.+)\s+\(.*\)$""".r
for {
Pattern(lib) <- ldd_lines
if !lib.startsWith("@executable_path/") && filter(lib_name(lib))
} yield lib
}
else {
val Pattern = """^.*=>\s*(/.+)\s+\(.*\)$""".r
val prefix =
mingw.root match {
case None => ""
case Some(path) => path.absolute.implode
}
for { Pattern(lib) <- ldd_lines if filter(lib_name(lib)) }
yield prefix + lib
}
if (libs.nonEmpty) {
- libs.foreach(lib => File.copy(Path.explode(lib), exe_dir))
+ libs.foreach(lib => Isabelle_System.copy_file(Path.explode(lib), exe_dir))
if (Platform.is_linux) {
if (patchelf) {
// requires e.g. Ubuntu 16.04 LTS
Isabelle_System.require_command("patchelf")
Isabelle_System.bash("patchelf --force-rpath --set-rpath '$ORIGIN' " + File.bash_path(exe_path)).check
}
else {
// requires e.g. LDFLAGS=-Wl,-rpath,_DUMMY_
Isabelle_System.require_command("chrpath")
Isabelle_System.bash("chrpath -r '$ORIGIN' " + File.bash_path(exe_path)).check
}
}
else if (Platform.is_macos) {
val script =
("install_name_tool" ::
libs.map(file => "-change " + Bash.string(file) + " " +
Bash.string("@executable_path/" + Path.explode(file).file_name) + " " +
File.bash_path(exe))).mkString(" ")
Isabelle_System.bash(script, cwd = exe_dir.file).check
}
}
libs
}
}
diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala
+++ b/src/Pure/System/isabelle_system.scala
@@ -1,451 +1,509 @@
/* Title: Pure/System/isabelle_system.scala
Author: Makarius
Fundamental Isabelle system environment: quasi-static module with
optional init operation.
*/
package isabelle
import java.io.{File => JFile, IOException}
-import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
+import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
+ StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
+
import scala.annotation.tailrec
object Isabelle_System
{
/** bootstrap information **/
def jdk_home(): String =
{
val java_home = System.getProperty("java.home", "")
val home = new JFile(java_home)
val parent = home.getParent
if (home.getName == "jre" && parent != null &&
(new JFile(new JFile(parent, "bin"), "javac")).exists) parent
else java_home
}
def bootstrap_directory(
preference: String, envar: String, property: String, description: String): String =
{
val value =
proper_string(preference) orElse // explicit argument
proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool
proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process
error("Unknown " + description + " directory")
if ((new JFile(value)).isDirectory) value
else error("Bad " + description + " directory " + quote(value))
}
/** implicit settings environment **/
abstract class Service
@volatile private var _settings: Option[Map[String, String]] = None
@volatile private var _services: Option[List[Class[Service]]] = None
def settings(): Map[String, String] =
{
if (_settings.isEmpty) init() // unsynchronized check
_settings.get
}
def services(): List[Class[Service]] =
{
if (_services.isEmpty) init() // unsynchronized check
_services.get
}
def make_services[C](c: Class[C]): List[C] =
for { c1 <- services() if Library.is_subclass(c1, c) }
yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
{
if (_settings.isEmpty || _services.isEmpty) {
val isabelle_root1 =
bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
val cygwin_root1 =
if (Platform.is_windows)
bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
else ""
if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
def set_cygwin_root()
{
if (Platform.is_windows)
_settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
}
set_cygwin_root()
def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
if (env.isDefinedAt(entry._1) || entry._2 == "") env
else env + entry
val env =
{
val temp_windows =
{
val temp = if (Platform.is_windows) System.getenv("TEMP") else null
if (temp != null && temp.contains('\\')) temp else ""
}
val user_home = System.getProperty("user.home", "")
val isabelle_app = System.getProperty("isabelle.app", "")
default(
default(
default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
"TEMP_WINDOWS" -> temp_windows),
"HOME" -> user_home),
"ISABELLE_APP" -> "true")
}
val settings =
{
val dump = JFile.createTempFile("settings", null)
dump.deleteOnExit
try {
val cmd1 =
if (Platform.is_windows)
List(cygwin_root1 + "\\bin\\bash", "-l",
File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
else
List(isabelle_root1 + "/bin/isabelle")
val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
val (output, rc) = process_output(process(cmd, env = env, redirect = true))
if (rc != 0) error(output)
val entries =
(for (entry <- File.read(dump).split("\u0000") if entry != "") yield {
val i = entry.indexOf('=')
if (i <= 0) entry -> ""
else entry.substring(0, i) -> entry.substring(i + 1)
}).toMap
entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
}
finally { dump.delete }
}
_settings = Some(settings)
set_cygwin_root()
val variable = "ISABELLE_SCALA_SERVICES"
val services =
for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
yield {
def err(msg: String): Nothing =
error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
try { Class.forName(name).asInstanceOf[Class[Service]] }
catch {
case _: ClassNotFoundException => err("Class not found")
case exn: Throwable => err(Exn.message(exn))
}
}
_services = Some(services)
}
}
/* getenv */
private def getenv_error(name: String): Nothing =
error("Undefined Isabelle environment variable: " + quote(name))
def getenv(name: String, env: Map[String, String] = settings()): String =
env.getOrElse(name, "")
def getenv_strict(name: String, env: Map[String, String] = settings()): String =
proper_string(getenv(name, env)) getOrElse
error("Undefined Isabelle environment variable: " + quote(name))
def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
def isabelle_id(): String =
proper_string(getenv("ISABELLE_ID")) getOrElse
Mercurial.repository(Path.explode("~~")).parent()
/** file-system operations **/
/* permissions */
def chmod(arg: String, path: Path): Unit =
bash("chmod " + arg + " " + File.bash_path(path)).check
def chown(arg: String, path: Path): Unit =
bash("chown " + arg + " " + File.bash_path(path)).check
/* directories */
def make_directory(path: Path): Path =
{
try { Files.createDirectories(path.file.toPath) }
catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
path
}
object Make_Directory extends Scala.Fun("make_directory")
{
val here = Scala_Project.here
def apply(arg: String): String = { make_directory(Path.explode(arg)); "" }
}
def new_directory(path: Path): Path =
if (path.is_dir) error("Directory already exists: " + path.absolute)
else make_directory(path)
+
+
+ /* copy */
+
def copy_dir(dir1: Path, dir2: Path): Unit =
bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
+ def copy_file(src: JFile, dst: JFile): Unit =
+ {
+ val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
+ if (!eq(src, target)) {
+ Files.copy(src.toPath, target.toPath,
+ StandardCopyOption.COPY_ATTRIBUTES,
+ StandardCopyOption.REPLACE_EXISTING)
+ }
+ }
+
+ def copy_file(path1: Path, path2: Path): Unit = copy_file(path1.file, path2.file)
+
+ def copy_file_base(base_dir: Path, src0: Path, target_dir: Path): Unit =
+ {
+ val src = src0.expand
+ val src_dir = src.dir
+ if (!src.starts_basic) error("Illegal path specification " + src + " beyond base directory")
+ copy_file(base_dir + src, Isabelle_System.make_directory(target_dir + src_dir))
+ }
+
+
+ /* move */
+
+ def move_file(src: JFile, dst: JFile)
+ {
+ val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
+ if (!eq(src, target))
+ Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
+ }
+
+ def move_file(path1: Path, path2: Path): Unit = move_file(path1.file, path2.file)
+
+
+ /* symbolic link */
+
+ def symlink(src: Path, dst: Path, force: Boolean = false)
+ {
+ val src_file = src.file
+ val dst_file = dst.file
+ val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
+
+ if (force) target.delete
+
+ try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
+ catch {
+ case _: UnsupportedOperationException if Platform.is_windows =>
+ Cygwin.link(File.standard_path(src), target)
+ case _: FileSystemException if Platform.is_windows =>
+ Cygwin.link(File.standard_path(src), target)
+ }
+ }
+
/* tmp files */
def isabelle_tmp_prefix(): JFile =
{
val path = Path.explode("$ISABELLE_TMP_PREFIX")
path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment
File.platform_file(path)
}
def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile =
{
val suffix = if (ext == "") "" else "." + ext
val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
file.deleteOnExit
file
}
def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
{
val file = tmp_file(name, ext)
try { body(File.path(file)) } finally { file.delete }
}
/* tmp dirs */
def rm_tree(root: Path): Unit = rm_tree(root.file)
def rm_tree(root: JFile)
{
root.delete
if (root.isDirectory) {
Files.walkFileTree(root.toPath,
new SimpleFileVisitor[JPath] {
override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
{
try { Files.deleteIfExists(file) }
catch { case _: IOException => }
FileVisitResult.CONTINUE
}
override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
{
if (e == null) {
try { Files.deleteIfExists(dir) }
catch { case _: IOException => }
FileVisitResult.CONTINUE
}
else throw e
}
}
)
}
}
def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
{
val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
dir.deleteOnExit
dir
}
def with_tmp_dir[A](name: String)(body: Path => A): A =
{
val dir = tmp_dir(name)
try { body(File.path(dir)) } finally { rm_tree(dir) }
}
/* quasi-atomic update of directory */
def update_directory(dir: Path, f: Path => Unit)
{
val new_dir = dir.ext("new")
val old_dir = dir.ext("old")
rm_tree(new_dir)
rm_tree(old_dir)
f(new_dir)
- if (dir.is_dir) File.move(dir, old_dir)
- File.move(new_dir, dir)
+ if (dir.is_dir) move_file(dir, old_dir)
+ move_file(new_dir, dir)
rm_tree(old_dir)
}
/** external processes **/
/* raw process */
def process(command_line: List[String],
cwd: JFile = null,
env: Map[String, String] = settings(),
redirect: Boolean = false): Process =
{
val proc = new ProcessBuilder
proc.command(command_line:_*) // fragile on Windows
if (cwd != null) proc.directory(cwd)
if (env != null) {
proc.environment.clear
for ((x, y) <- env) proc.environment.put(x, y)
}
proc.redirectErrorStream(redirect)
proc.start
}
def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close
val output = File.read_stream(proc.getInputStream)
val rc =
try { proc.waitFor }
finally {
proc.getInputStream.close
proc.getErrorStream.close
proc.destroy
Exn.Interrupt.dispose()
}
(output, rc)
}
def kill(signal: String, group_pid: String): (String, Int) =
{
val bash =
if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
}
/* GNU bash */
def bash(script: String,
cwd: JFile = null,
env: Map[String, String] = settings(),
redirect: Boolean = false,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
watchdog: Option[Bash.Watchdog] = None,
strict: Boolean = true,
cleanup: () => Unit = () => ()): Process_Result =
{
Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
result(progress_stdout = progress_stdout, progress_stderr = progress_stderr,
watchdog = watchdog, strict = strict)
}
private lazy val gnutar_check: Boolean =
try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
catch { case ERROR(_) => false }
def gnutar(
args: String,
dir: Path = Path.current,
original_owner: Boolean = false,
redirect: Boolean = false): Process_Result =
{
val options =
(if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
(if (original_owner) "" else "--owner=root --group=staff ")
if (gnutar_check) bash("tar " + options + args, redirect = redirect)
else error("Expected to find GNU tar executable")
}
def require_command(cmds: String*)
{
for (cmd <- cmds) {
if (!bash(Bash.string(cmd) + " --version").ok) error("Missing command: " + quote(cmd))
}
}
private lazy val curl_check: Unit =
try { require_command("curl") }
catch { case ERROR(msg) => error(msg + " --- cannot download files") }
def download(url: String, file: Path, progress: Progress = new Progress): Unit =
{
curl_check
progress.echo("Getting " + quote(url))
try {
bash("curl --fail --silent --location " + Bash.string(url) +
" > " + File.bash_path(file)).check
}
catch { case ERROR(msg) => cat_error("Failed to download " + quote(url), msg) }
}
def hostname(): String = bash("hostname -s").check.out
def open(arg: String): Unit =
bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
def pdf_viewer(arg: Path): Unit =
bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
def open_external_file(name: String): Boolean =
{
val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
val external =
ext.nonEmpty &&
Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
if (external) {
if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
else open(name)
}
external
}
def export_isabelle_identifier(isabelle_identifier: String): String =
if (isabelle_identifier == "") ""
else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
/** Isabelle resources **/
/* repository clone with Admin */
def admin(): Boolean = Path.explode("~~/Admin").is_dir
/* components */
def components(): List[Path] =
Path.split(getenv_strict("ISABELLE_COMPONENTS"))
/* default logic */
def default_logic(args: String*): String =
{
args.find(_ != "") match {
case Some(logic) => logic
- case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC")
+ case None => getenv_strict("ISABELLE_LOGIC")
}
}
}
diff --git a/src/Pure/Thy/bibtex.scala b/src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala
+++ b/src/Pure/Thy/bibtex.scala
@@ -1,702 +1,702 @@
/* Title: Pure/Thy/bibtex.scala
Author: Makarius
BibTeX support.
*/
package isabelle
import java.io.{File => JFile}
import scala.collection.mutable
import scala.util.parsing.combinator.RegexParsers
import scala.util.parsing.input.Reader
object Bibtex
{
/** file format **/
def is_bibtex(name: String): Boolean = name.endsWith(".bib")
class File_Format extends isabelle.File_Format
{
val format_name: String = "bibtex"
val file_ext: String = "bib"
override def theory_suffix: String = "bibtex_file"
override def theory_content(name: String): String =
"""theory "bib" imports Pure begin bibtex_file """ +
Outer_Syntax.quote_string(name) + """ end"""
override def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
{
val name = snapshot.node_name
if (detect(name.node)) {
val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
val content =
Isabelle_System.with_tmp_file("bib", "bib") { bib =>
File.write(bib, snapshot.node.source)
Bibtex.html_output(List(bib), style = "unsort", title = title)
}
Some(Presentation.HTML_Document(title, content))
}
else None
}
}
/** bibtex errors **/
def bibtex_errors(dir: Path, root_name: String): List[String] =
{
val log_path = dir + Path.explode(root_name).ext("blg")
if (log_path.is_file) {
val Error1 = """^(I couldn't open database file .+)$""".r
val Error2 = """^(.+)---line (\d+) of file (.+)""".r
Line.logical_lines(File.read(log_path)).flatMap(line =>
line match {
case Error1(msg) => Some("Bibtex error: " + msg)
case Error2(msg, Value.Int(l), file) =>
val path = File.standard_path(file)
if (Path.is_wellformed(path)) {
val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode)
Some("Bibtex error" + Position.here(pos) + ":\n " + msg)
}
else None
case _ => None
})
}
else Nil
}
/** check database **/
def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) =
{
val chunks = parse(Line.normalize(database))
var chunk_pos = Map.empty[String, Position.T]
val tokens = new mutable.ListBuffer[(Token, Position.T)]
var line = 1
var offset = 1
def make_pos(length: Int): Position.T =
Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line)
def advance_pos(tok: Token)
{
for (s <- Symbol.iterator(tok.source)) {
if (Symbol.is_newline(s)) line += 1
offset += 1
}
}
def get_line_pos(l: Int): Position.T =
if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none
for (chunk <- chunks) {
val name = chunk.name
if (name != "" && !chunk_pos.isDefinedAt(name)) {
chunk_pos += (name -> make_pos(chunk.heading_length))
}
for (tok <- chunk.tokens) {
tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length))
advance_pos(tok)
}
}
Isabelle_System.with_tmp_dir("bibtex")(tmp_dir =>
{
File.write(tmp_dir + Path.explode("root.bib"),
tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n"))
File.write(tmp_dir + Path.explode("root.aux"),
"\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}")
Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file)
val Error = """^(.*)---line (\d+) of file root.bib$""".r
val Warning = """^Warning--(.+)$""".r
val Warning_Line = """--line (\d+) of file root.bib$""".r
val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r
val log_file = tmp_dir + Path.explode("root.blg")
val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil
val (errors, warnings) =
if (lines.isEmpty) (Nil, Nil)
else {
lines.zip(lines.tail ::: List("")).flatMap(
{
case (Error(msg, Value.Int(l)), _) =>
Some((true, (msg, get_line_pos(l))))
case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name))))
case (Warning(msg), Warning_Line(Value.Int(l))) =>
Some((false, (Word.capitalize(msg), get_line_pos(l))))
case (Warning(msg), _) =>
Some((false, (Word.capitalize(msg), Position.none)))
case _ => None
}
).partition(_._1)
}
(errors.map(_._2), warnings.map(_._2))
})
}
object Check_Database extends Scala.Fun("bibtex_check_database")
{
val here = Scala_Project.here
def apply(database: String): String =
{
import XML.Encode._
YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
check_database(database)))
}
}
/** document model **/
/* entries */
def entries(text: String): List[Text.Info[String]] =
{
val result = new mutable.ListBuffer[Text.Info[String]]
var offset = 0
for (chunk <- Bibtex.parse(text)) {
val end_offset = offset + chunk.source.length
if (chunk.name != "" && !chunk.is_command)
result += Text.Info(Text.Range(offset, end_offset), chunk.name)
offset = end_offset
}
result.toList
}
def entries_iterator[A, B <: Document.Model](models: Map[A, B])
: Iterator[Text.Info[(String, B)]] =
{
for {
(_, model) <- models.iterator
info <- model.bibtex_entries.iterator
} yield info.map((_, model))
}
/* completion */
def completion[A, B <: Document.Model](
history: Completion.History, rendering: Rendering, caret: Text.Offset,
models: Map[A, B]): Option[Completion.Result] =
{
for {
Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
name1 <- Completion.clean_name(name)
original <- rendering.get_text(r)
original1 <- Completion.clean_name(Library.perhaps_unquote(original))
entries =
(for {
Text.Info(_, (entry, _)) <- entries_iterator(models)
if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
} yield entry).toList
if entries.nonEmpty
items =
entries.sorted.map({
case entry =>
val full_name = Long_Name.qualify(Markup.CITATION, entry)
val description = List(entry, "(BibTeX entry)")
val replacement = quote(entry)
Completion.Item(r, original, full_name, description, replacement, 0, false)
}).sorted(history.ordering).take(rendering.options.int("completion_limit"))
} yield Completion.Result(r, original, false, items)
}
/** content **/
private val months = List(
"jan",
"feb",
"mar",
"apr",
"may",
"jun",
"jul",
"aug",
"sep",
"oct",
"nov",
"dec")
def is_month(s: String): Boolean = months.contains(s.toLowerCase)
private val commands = List("preamble", "string")
def is_command(s: String): Boolean = commands.contains(s.toLowerCase)
sealed case class Entry(
kind: String,
required: List[String],
optional_crossref: List[String],
optional_other: List[String])
{
val optional_standard: List[String] = List("url", "doi", "ee")
def is_required(s: String): Boolean = required.contains(s.toLowerCase)
def is_optional(s: String): Boolean =
optional_crossref.contains(s.toLowerCase) ||
optional_other.contains(s.toLowerCase) ||
optional_standard.contains(s.toLowerCase)
def fields: List[String] =
required ::: optional_crossref ::: optional_other ::: optional_standard
def template: String =
"@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n"
}
val known_entries: List[Entry] =
List(
Entry("Article",
List("author", "title"),
List("journal", "year"),
List("volume", "number", "pages", "month", "note")),
Entry("InProceedings",
List("author", "title"),
List("booktitle", "year"),
List("editor", "volume", "number", "series", "pages", "month", "address",
"organization", "publisher", "note")),
Entry("InCollection",
List("author", "title", "booktitle"),
List("publisher", "year"),
List("editor", "volume", "number", "series", "type", "chapter", "pages",
"edition", "month", "address", "note")),
Entry("InBook",
List("author", "editor", "title", "chapter"),
List("publisher", "year"),
List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
Entry("Proceedings",
List("title", "year"),
List(),
List("booktitle", "editor", "volume", "number", "series", "address", "month",
"organization", "publisher", "note")),
Entry("Book",
List("author", "editor", "title"),
List("publisher", "year"),
List("volume", "number", "series", "address", "edition", "month", "note")),
Entry("Booklet",
List("title"),
List(),
List("author", "howpublished", "address", "month", "year", "note")),
Entry("PhdThesis",
List("author", "title", "school", "year"),
List(),
List("type", "address", "month", "note")),
Entry("MastersThesis",
List("author", "title", "school", "year"),
List(),
List("type", "address", "month", "note")),
Entry("TechReport",
List("author", "title", "institution", "year"),
List(),
List("type", "number", "address", "month", "note")),
Entry("Manual",
List("title"),
List(),
List("author", "organization", "address", "edition", "month", "year", "note")),
Entry("Unpublished",
List("author", "title", "note"),
List(),
List("month", "year")),
Entry("Misc",
List(),
List(),
List("author", "title", "howpublished", "month", "year", "note")))
def get_entry(kind: String): Option[Entry] =
known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
def is_entry(kind: String): Boolean = get_entry(kind).isDefined
/** tokens and chunks **/
object Token
{
object Kind extends Enumeration
{
val COMMAND = Value("command")
val ENTRY = Value("entry")
val KEYWORD = Value("keyword")
val NAT = Value("natural number")
val STRING = Value("string")
val NAME = Value("name")
val IDENT = Value("identifier")
val SPACE = Value("white space")
val COMMENT = Value("ignored text")
val ERROR = Value("bad input")
}
}
sealed case class Token(kind: Token.Kind.Value, source: String)
{
def is_kind: Boolean =
kind == Token.Kind.COMMAND ||
kind == Token.Kind.ENTRY ||
kind == Token.Kind.IDENT
def is_name: Boolean =
kind == Token.Kind.NAME ||
kind == Token.Kind.IDENT
def is_ignored: Boolean =
kind == Token.Kind.SPACE ||
kind == Token.Kind.COMMENT
def is_malformed: Boolean =
kind == Token.Kind.ERROR
def is_open: Boolean =
kind == Token.Kind.KEYWORD && (source == "{" || source == "(")
}
case class Chunk(kind: String, tokens: List[Token])
{
val source = tokens.map(_.source).mkString
private val content: Option[List[Token]] =
tokens match {
case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty =>
(body.init.filterNot(_.is_ignored), body.last) match {
case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}"))
if tok.is_kind => Some(toks)
case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")"))
if tok.is_kind => Some(toks)
case _ => None
}
case _ => None
}
def name: String =
content match {
case Some(tok :: _) if tok.is_name => tok.source
case _ => ""
}
def heading_length: Int =
if (name == "") 1
else (0 /: tokens.takeWhile(tok => !tok.is_open)){ case (n, tok) => n + tok.source.length }
def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
}
/** parsing **/
// context of partial line-oriented scans
abstract class Line_Context
case object Ignored extends Line_Context
case object At extends Line_Context
case class Item_Start(kind: String) extends Line_Context
case class Item_Open(kind: String, end: String) extends Line_Context
case class Item(kind: String, end: String, delim: Delimited) extends Line_Context
case class Delimited(quoted: Boolean, depth: Int)
val Closed = Delimited(false, 0)
private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source)
private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
// See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
// module @.
object Parsers extends RegexParsers
{
/* white space and comments */
override val whiteSpace = "".r
private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
private val spaces = rep(space)
/* ignored text */
private val ignored: Parser[Chunk] =
rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
private def ignored_line: Parser[(Chunk, Line_Context)] =
ignored ^^ { case a => (a, Ignored) }
/* delimited string: outermost "..." or {...} and body with balanced {...} */
// see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces
private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] =
new Parser[(String, Delimited)]
{
require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0,
"bad delimiter depth")
def apply(in: Input) =
{
val start = in.offset
val end = in.source.length
var i = start
var q = delim.quoted
var d = delim.depth
var finished = false
while (!finished && i < end) {
val c = in.source.charAt(i)
if (c == '"' && d == 0) { i += 1; d = 1; q = true }
else if (c == '"' && d == 1 && q) {
i += 1; d = 0; q = false; finished = true
}
else if (c == '{') { i += 1; d += 1 }
else if (c == '}') {
if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true }
else {i = start; finished = true }
}
else if (d > 0) i += 1
else finished = true
}
if (i == start) Failure("bad input", in)
else {
val s = in.source.subSequence(start, i).toString
Success((s, Delimited(q, d)), in.drop(i - start))
}
}
}.named("delimited_depth")
private def delimited: Parser[Token] =
delimited_depth(Closed) ^?
{ case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
private def recover_delimited: Parser[Token] =
"""["{][^@]*""".r ^^ token(Token.Kind.ERROR)
def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
(Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
/* other tokens */
private val at = "@" ^^ keyword
private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT)
private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME)
private val identifier =
"""[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r
private val ident = identifier ^^ token(Token.Kind.IDENT)
val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space))
/* body */
private val body =
delimited | (recover_delimited | other_token)
private def body_line(ctxt: Item) =
if (ctxt.delim.depth > 0)
delimited_line(ctxt)
else
delimited_line(ctxt) |
other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } |
ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) }
/* items: command or entry */
private val item_kind =
identifier ^^ { case a =>
val kind =
if (is_command(a)) Token.Kind.COMMAND
else if (is_entry(a)) Token.Kind.ENTRY
else Token.Kind.IDENT
Token(kind, a)
}
private val item_begin =
"{" ^^ { case a => ("}", keyword(a)) } |
"(" ^^ { case a => (")", keyword(a)) }
private def item_name(kind: String) =
kind.toLowerCase match {
case "preamble" => failure("")
case "string" => identifier ^^ token(Token.Kind.NAME)
case _ => name
}
private val item_start =
at ~ spaces ~ item_kind ~ spaces ^^
{ case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) }
private val item: Parser[Chunk] =
(item_start ~ item_begin ~ spaces) into
{ case (kind, a) ~ ((end, b)) ~ c =>
opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
private val recover_item: Parser[Chunk] =
at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
/* chunks */
val chunk: Parser[Chunk] = ignored | (item | recover_item)
def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] =
{
ctxt match {
case Ignored =>
ignored_line |
at ^^ { case a => (Chunk("", List(a)), At) }
case At =>
space ^^ { case a => (Chunk("", List(a)), ctxt) } |
item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } |
recover_item ^^ { case a => (a, Ignored) } |
ignored_line
case Item_Start(kind) =>
space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } |
recover_item ^^ { case a => (a, Ignored) } |
ignored_line
case Item_Open(kind, end) =>
space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } |
body_line(Item(kind, end, Closed)) |
ignored_line
case item_ctxt: Item =>
body_line(item_ctxt) |
ignored_line
case _ => failure("")
}
}
}
/* parse */
def parse(input: CharSequence): List[Chunk] =
Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match {
case Parsers.Success(result, _) => result
case _ => error("Unexpected failure to parse input:\n" + input.toString)
}
def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) =
{
var in: Reader[Char] = Scan.char_reader(input)
val chunks = new mutable.ListBuffer[Chunk]
var ctxt = context
while (!in.atEnd) {
Parsers.parse(Parsers.chunk_line(ctxt), in) match {
case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
case Parsers.NoSuccess(_, rest) =>
error("Unepected failure to parse input:\n" + rest.source.toString)
}
}
(chunks.toList, ctxt)
}
/** HTML output **/
private val output_styles =
List(
"" -> "html-n",
"plain" -> "html-n",
"alpha" -> "html-a",
"named" -> "html-n",
"paragraph" -> "html-n",
"unsort" -> "html-u",
"unsortlist" -> "html-u")
def html_output(bib: List[Path],
title: String = "Bibliography",
body: Boolean = false,
citations: List[String] = List("*"),
style: String = "",
chronological: Boolean = false): String =
{
Isabelle_System.with_tmp_dir("bibtex")(tmp_dir =>
{
/* database files */
val bib_files = bib.map(_.drop_ext)
val bib_names =
{
val names0 = bib_files.map(_.file_name)
if (Library.duplicates(names0).isEmpty) names0
else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
}
for ((a, b) <- bib_files zip bib_names) {
- File.copy(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
+ Isabelle_System.copy_file(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
}
/* style file */
val bst =
output_styles.toMap.get(style) match {
case Some(base) => base + (if (chronological) "c" else "") + ".bst"
case None =>
error("Bad style for bibtex HTML output: " + quote(style) +
"\n(expected: " + commas_quote(output_styles.map(_._1)) + ")")
}
- File.copy(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
+ Isabelle_System.copy_file(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
/* result */
val in_file = Path.explode("bib.aux")
val out_file = Path.explode("bib.html")
File.write(tmp_dir + in_file,
bib_names.mkString("\\bibdata{", ",", "}\n") +
citations.map(cite => "\\citation{" + cite + "}\n").mkString)
Isabelle_System.bash(
"\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
" -u -s " + Bash.string(proper_string(style) getOrElse "empty") +
(if (chronological) " -c" else "") +
(if (title != "") " -h " + Bash.string(title) + " " else "") +
" " + File.bash_path(in_file) + " " + File.bash_path(out_file),
cwd = tmp_dir.file).check
val html = File.read(tmp_dir + out_file)
if (body) {
cat_lines(
split_lines(html).
dropWhile(line => !line.startsWith("