--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Sat Mar 04 23:25:30 2023 +0100
@@ -43,7 +43,6 @@
select_dirs: List[Path] = Nil,
numa_shuffling: Boolean = false,
max_jobs: Int = 1,
- verbose: Boolean = false
): Build.Results = {
require(!selection.requirements)
Isabelle_System.make_directory(output_dir)
@@ -53,7 +52,7 @@
Build.build(options, build_heap = true,
selection = selection.copy(requirements = true), progress = progress, dirs = dirs,
select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
- verbose = verbose)
+ verbose = progress.verbose)
if (build_results0.ok) {
val build_options =
@@ -71,10 +70,9 @@
case msg: Prover.Protocol_Output =>
msg.properties match {
case Protocol.Export(args) if args.name.startsWith("mirabelle/") =>
- if (verbose) {
- progress.echo(
- "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")")
- }
+ progress.echo(
+ "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")",
+ verbose = true)
val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = build_results0.cache)
val lines = Pretty.string_of(yxml).trim()
val prefix =
@@ -97,7 +95,7 @@
Build.build(build_options, clean_build = true,
selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs,
- numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose,
+ numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = progress.verbose,
session_setup = session_setup)
}
else build_results0
@@ -197,9 +195,7 @@
val start_date = Date.now()
- if (verbose) {
- progress.echo("Started at " + Build_Log.print_date(start_date))
- }
+ progress.echo("Started at " + Build_Log.print_date(start_date), verbose = true)
val results =
progress.interrupt_handler {
@@ -216,16 +212,13 @@
dirs = dirs,
select_dirs = select_dirs,
numa_shuffling = Host.numa_check(progress, numa_shuffling),
- max_jobs = max_jobs,
- verbose = verbose)
+ max_jobs = max_jobs)
}
val end_date = Date.now()
val elapsed_time = end_date.time - start_date.time
- if (verbose) {
- progress.echo("\nFinished at " + Build_Log.print_date(end_date))
- }
+ progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
val total_timing =
results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
--- a/src/Pure/Admin/build_csdp.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_csdp.scala Sat Mar 04 23:25:30 2023 +0100
@@ -49,7 +49,6 @@
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
@@ -112,7 +111,9 @@
foreach(file => flags.change(File.path(file)))
}
- progress.bash(mingw.bash_script("make"), cwd = source_dir.file, echo = verbose).check
+ progress.bash(mingw.bash_script("make"),
+ cwd = source_dir.file,
+ echo = progress.verbose).check
/* install */
@@ -188,9 +189,9 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress(verbose = verbose)
- build_csdp(download_url = download_url, verbose = verbose, progress = progress,
+ build_csdp(download_url = download_url, progress = progress,
target_dir = target_dir, mingw = mingw)
})
}
--- a/src/Pure/Admin/build_e.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_e.scala Sat Mar 04 23:25:30 2023 +0100
@@ -16,7 +16,6 @@
def build_e(
version: String = default_version,
download_url: String = default_download_url,
- verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
@@ -58,8 +57,8 @@
val build_script = "./configure" + build_options + " && make"
Isabelle_System.bash(build_script, cwd = source_dir.file,
- progress_stdout = progress.echo_if(verbose, _),
- progress_stderr = progress.echo_if(verbose, _)).check
+ progress_stdout = progress.echo(_, verbose = true),
+ progress_stderr = progress.echo(_, verbose = true)).check
/* install */
@@ -131,9 +130,9 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress(verbose = verbose)
build_e(version = version, download_url = download_url,
- verbose = verbose, progress = progress, target_dir = target_dir)
+ progress = progress, target_dir = target_dir)
})
}
--- a/src/Pure/Admin/build_minisat.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_minisat.scala Sat Mar 04 23:25:30 2023 +0100
@@ -18,7 +18,6 @@
def build_minisat(
download_url: String = default_download_url,
component_name: String = "",
- verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
@@ -77,7 +76,7 @@
_.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "")
}
}
- progress.bash("make r", source_dir.file, echo = verbose).check
+ progress.bash("make r", source_dir.file, echo = progress.verbose).check
Isabelle_System.copy_file(
source_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
@@ -142,9 +141,9 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress(verbose = verbose)
build_minisat(download_url = download_url, component_name = component_name,
- verbose = verbose, progress = progress, target_dir = target_dir)
+ progress = progress, target_dir = target_dir)
})
}
--- a/src/Pure/Admin/build_polyml.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_polyml.scala Sat Mar 04 23:25:30 2023 +0100
@@ -188,7 +188,6 @@
sha1_url: String = default_sha1_url,
sha1_version: String = default_sha1_version,
target_dir: Path = Path.current,
- verbose: Boolean = false,
progress: Progress = new Progress
): Unit = {
/* component */
@@ -227,7 +226,7 @@
arch_64 = arch_64,
options = options,
mingw = mingw,
- progress = if (verbose) progress else new Progress)
+ progress = if (progress.verbose) progress else new Progress)
}
}
@@ -415,11 +414,11 @@
val options = getopts(args)
- val progress = new Console_Progress
+ val progress = new Console_Progress(verbose = verbose)
build_polyml(options = options, mingw = mingw, component_name = component_name,
polyml_url = polyml_url, polyml_version = polyml_version, polyml_name = polyml_name,
sha1_url = sha1_url, sha1_version = sha1_version, target_dir = target_dir,
- verbose = verbose, progress = progress)
+ progress = progress)
})
}
--- a/src/Pure/Admin/build_spass.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_spass.scala Sat Mar 04 23:25:30 2023 +0100
@@ -15,9 +15,9 @@
def build_spass(
download_url: String = default_download_url,
- verbose: Boolean = false,
progress: Progress = new Progress,
- target_dir: Path = Path.current): Unit = {
+ target_dir: Path = Path.current
+ ): Unit = {
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
Isabelle_System.require_command("bison")
Isabelle_System.require_command("flex")
@@ -85,8 +85,8 @@
}
Isabelle_System.bash("make", cwd = source_dir.file,
- progress_stdout = progress.echo_if(verbose, _),
- progress_stderr = progress.echo_if(verbose, _)).check
+ progress_stdout = progress.echo(_, verbose = true),
+ progress_stderr = progress.echo(_, verbose = true)).check
/* install */
@@ -166,9 +166,8 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress(verbose = verbose)
- build_spass(download_url = download_url, verbose = verbose, progress = progress,
- target_dir = target_dir)
+ build_spass(download_url = download_url, progress = progress, target_dir = target_dir)
})
}
--- a/src/Pure/Admin/build_status.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_status.scala Sat Mar 04 23:25:30 2023 +0100
@@ -56,7 +56,6 @@
progress: Progress = new Progress,
profiles: List[Profile] = default_profiles,
only_sessions: Set[String] = Set.empty,
- verbose: Boolean = false,
target_dir: Path = default_target_dir,
ml_statistics: Boolean = false,
image_size: (Int, Int) = default_image_size
@@ -66,8 +65,7 @@
ML_Statistics.workers_fields).flatMap(_._2).toSet
val data =
- read_data(options, progress = progress, profiles = profiles,
- only_sessions = only_sessions, verbose = verbose,
+ read_data(options, progress = progress, profiles = profiles, only_sessions = only_sessions,
ml_statistics = ml_statistics, ml_statistics_domain = ml_statistics_domain)
present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)
@@ -213,8 +211,7 @@
profiles: List[Profile] = default_profiles,
only_sessions: Set[String] = Set.empty,
ml_statistics: Boolean = false,
- ml_statistics_domain: String => Boolean = _ => true,
- verbose: Boolean = false
+ ml_statistics_domain: String => Boolean = _ => true
): Data = {
val date = Date.now()
var data_hosts = Map.empty[String, Set[String]]
@@ -258,7 +255,7 @@
val Threads_Option = """threads\s*=\s*(\d+)""".r
val sql = profile.select(options, columns, only_sessions)
- progress.echo_if(verbose, sql)
+ progress.echo(sql, verbose = true)
db.using_statement(sql) { stmt =>
val res = stmt.execute_query()
@@ -620,9 +617,9 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress
+ val progress = new Console_Progress(verbose = verbose)
- build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
+ build_status(options, progress = progress, only_sessions = only_sessions,
target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size)
})
}
--- a/src/Pure/Admin/build_vampire.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_vampire.scala Sat Mar 04 23:25:30 2023 +0100
@@ -21,7 +21,6 @@
download_url: String = default_download_url,
jobs: Int = default_jobs,
component_name: String = "",
- verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
@@ -80,14 +79,14 @@
val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
val cmake_out =
progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""",
- cwd = source_dir.file, echo = verbose).check.out
+ cwd = source_dir.file, echo = progress.verbose).check.out
val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
val binary =
split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
.getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
- progress.bash("make -j" + jobs, cwd = source_dir.file, echo = verbose).check
+ progress.bash("make -j" + jobs, cwd = source_dir.file, echo = progress.verbose).check
Isabelle_System.copy_file(source_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
platform_dir + Path.basic("vampire").platform_exe)
@@ -151,9 +150,9 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress(verbose = verbose)
build_vampire(download_url = download_url, component_name = component_name,
- jobs = jobs, verbose = verbose, progress = progress, target_dir = target_dir)
+ jobs = jobs, progress = progress, target_dir = target_dir)
})
}
--- a/src/Pure/Admin/build_verit.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_verit.scala Sat Mar 04 23:25:30 2023 +0100
@@ -15,7 +15,6 @@
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
@@ -75,7 +74,7 @@
if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else ""
progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"),
- cwd = source_dir.file, echo = verbose).check
+ cwd = source_dir.file, echo = progress.verbose).check
/* install */
@@ -144,9 +143,9 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress(verbose = verbose)
- build_verit(download_url = download_url, verbose = verbose, progress = progress,
+ build_verit(download_url = download_url, progress = progress,
target_dir = target_dir, mingw = mingw)
})
}
--- a/src/Pure/Admin/build_zipperposition.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_zipperposition.scala Sat Mar 04 23:25:30 2023 +0100
@@ -15,7 +15,6 @@
def build_zipperposition(
version: String = default_version,
- verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
@@ -43,10 +42,10 @@
/* build */
progress.echo("OCaml/OPAM setup ...")
- progress.bash("isabelle ocaml_setup", echo = verbose).check
+ progress.bash("isabelle ocaml_setup", echo = progress.verbose).check
progress.echo("Building Zipperposition for " + platform_name + " ...")
- progress.bash(cwd = build_dir.file, echo = verbose,
+ progress.bash(cwd = build_dir.file, echo = progress.verbose,
script = "isabelle_opam install -y --destdir=" + File.bash_path(build_dir) +
" zipperposition=" + Bash.string(version)).check
@@ -112,9 +111,8 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress(verbose = verbose)
- build_zipperposition(version = version, verbose = verbose, progress = progress,
- target_dir = target_dir)
+ build_zipperposition(version = version, progress = progress, target_dir = target_dir)
})
}
--- a/src/Pure/Admin/ci_build.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/ci_build.scala Sat Mar 04 23:25:30 2023 +0100
@@ -178,7 +178,7 @@
selection = config.selection,
progress = progress,
clean_build = config.clean,
- verbose = true,
+ verbose = progress.verbose,
numa_shuffling = profile.numa,
max_jobs = profile.jobs,
dirs = config.include,
--- a/src/Pure/Thy/document_build.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Thy/document_build.scala Sat Mar 04 23:25:30 2023 +0100
@@ -588,7 +588,7 @@
progress.interrupt_handler {
val build_results =
Build.build(options, selection = Sessions.Selection.session(session),
- dirs = dirs, progress = progress, verbose = verbose_build)
+ dirs = dirs, progress = progress, verbose = progress.verbose)
if (!build_results.ok) error("Failed to build session " + quote(session))
if (output_sources.isEmpty && output_pdf.isEmpty) {
--- a/src/Pure/Tools/build_docker.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Tools/build_docker.scala Sat Mar 04 23:25:30 2023 +0100
@@ -39,8 +39,7 @@
entrypoint: Boolean = false,
output: Option[Path] = None,
more_packages: List[String] = Nil,
- tag: String = "",
- verbose: Boolean = false
+ tag: String = ""
): Unit = {
val isabelle_name =
app_archive match {
@@ -103,7 +102,7 @@
tmp_dir + Path.explode("Isabelle.tar.gz"))
}
- val quiet_option = if (verbose) "" else " -q"
+ val quiet_option = if (progress.verbose) "" else " -q"
val tag_option = if_proper(tag, " -t " + Bash.string(tag))
progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
echo = true).check
@@ -170,8 +169,10 @@
case _ => getopts.usage()
}
- build_docker(new Console_Progress(), app_archive, base = base, work_dir = work_dir,
+ val progress = new Console_Progress(verbose = verbose)
+
+ build_docker(progress, app_archive, base = base, work_dir = work_dir,
logic = logic, no_build = no_build, entrypoint = entrypoint, output = output,
- more_packages = more_packages, tag = tag, verbose = verbose)
+ more_packages = more_packages, tag = tag)
})
}
--- a/src/Pure/Tools/dotnet_setup.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala Sat Mar 04 23:25:30 2023 +0100
@@ -61,7 +61,6 @@
version: String = default_version,
force: Boolean = false,
dry_run: Boolean = false,
- verbose: Boolean = false,
progress: Progress = new Progress
): Unit = {
check_platform_spec(platform_spec)
@@ -134,7 +133,7 @@
" -InstallDir " + Bash.string(platform.name) +
(if (dry_run) " -DryRun" else "") +
" -NoPath"
- progress.bash(script, echo = verbose,
+ progress.bash(script, echo = progress.verbose,
cwd = if (dry_run) null else component_dir.path.file).check
for (exe <- File.find_files(platform_dir.file, pred = _.getName.endsWith(".exe"))) {
File.set_executable(File.path(exe), true)
@@ -192,11 +191,11 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress(verbose = verbose)
for (platform <- platforms) {
dotnet_setup(platform_spec = platform, target_dir = target_dir, install_url = install_url,
- version = version, force = force, dry_run = dry_run, verbose = verbose, progress = progress)
+ version = version, force = force, dry_run = dry_run, progress = progress)
}
})
}
--- a/src/Pure/Tools/dump.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Tools/dump.scala Sat Mar 04 23:25:30 2023 +0100
@@ -464,7 +464,7 @@
val start_date = Date.now()
- progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date))
+ progress.echo("Started at " + Build_Log.print_date(start_date), verbose = true)
progress.interrupt_handler {
dump(options, logic,
@@ -486,7 +486,7 @@
val end_date = Date.now()
val timing = end_date.time - start_date.time
- progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date))
+ progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
progress.echo(timing.message_hms + " elapsed time")
})
}
--- a/src/Tools/VSCode/src/build_vscodium.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala Sat Mar 04 23:25:30 2023 +0100
@@ -275,7 +275,7 @@
/* original repository clones and patches */
- def vscodium_patch(verbose: Boolean = false, progress: Progress = new Progress): String = {
+ def vscodium_patch(progress: Progress = new Progress): String = {
val platform_info = linux_platform_info
check_system(List(platform_info.platform))
@@ -291,7 +291,7 @@
"./prepare_vscode.sh",
// enforce binary diff of code.xpm
"cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm"
- ).mkString("\n"), cwd = build_dir.file, echo = verbose).check
+ ).mkString("\n"), cwd = build_dir.file, echo = progress.verbose).check
Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base,
diff_options = "--exclude=.git --exclude=node_modules")
}
@@ -306,7 +306,6 @@
def build_vscodium(
target_dir: Path = Path.current,
platforms: List[Platform.Family.Value] = default_platforms,
- verbose: Boolean = false,
progress: Progress = new Progress
): Unit = {
check_system(platforms)
@@ -328,7 +327,7 @@
def write_patch(name: String, patch: String): Unit =
File.write(patches_dir + Path.explode(name).patch, patch)
- write_patch("01-vscodium", vscodium_patch(verbose = verbose, progress = progress))
+ write_patch("01-vscodium", vscodium_patch(progress = progress))
/* build */
@@ -346,7 +345,7 @@
progress.echo("Build ...")
progress.bash(platform_info.environment + "\n" + "./build.sh",
- cwd = build_dir.file, echo = verbose).check
+ cwd = build_dir.file, echo = progress.verbose).check
if (platform_info.primary) {
Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
@@ -432,10 +431,9 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress(verbose = verbose)
- build_vscodium(target_dir = target_dir, platforms = platforms,
- verbose = verbose, progress = progress)
+ build_vscodium(target_dir = target_dir, platforms = platforms, progress = progress)
})
val isabelle_tool2 =