--- a/.hgtags Wed Mar 06 09:26:40 2024 +0100
+++ b/.hgtags Wed Mar 06 09:43:25 2024 +0100
@@ -42,3 +42,4 @@
68ffcf5cc94bd7be344a49bfff0060114ef92987 build_history_base_arm
1ac2416e843293bc6917ba965f54b42962514b7f Isabelle2022
b5f3d1051b131a80b1e4560cc05e5a3d223bc64f Isabelle2023
+98f009f56400c7317d26d96cf7d904cc984b1d46 Isabelle2024-RC0
--- a/Admin/Release/CHECKLIST Wed Mar 06 09:26:40 2024 +0100
+++ b/Admin/Release/CHECKLIST Wed Mar 06 09:43:25 2024 +0100
@@ -75,23 +75,20 @@
- regular packaging:
- #on fast Linux machine, with access to Linux + Apple ARM + Windows build_host
- Admin/build_release -D ~/tmp/isadist -b HOL -R Isabelle2023 -j2 -l
-
- #with access Linux ARM build_host
- Admin/build_release -D ~/tmp/isadist -b HOL -R Isabelle2023 -p linux_arm
+ #on fast Linux machine, with access to build_host for each platform
+ Admin/build_release -D ~/tmp/isadist -b HOL -R Isabelle2024 -j2 -l
- Docker image:
- isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2023 Isabelle2023_linux.tar.gz
- isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2023_X11_Latex -P X11 -P latex Isabelle2023_linux.tar.gz
+ isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2024 Isabelle2024_linux.tar.gz
+ isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2024_X11_Latex -P X11 -P latex Isabelle2024_linux.tar.gz
- isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2023_ARM Isabelle2023_linux_arm.tar.gz
- isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2023_ARM_X11_Latex -P X11 -P latex Isabelle2023_linux_arm.tar.gz
+ isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2024_ARM Isabelle2024_linux_arm.tar.gz
+ isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2024_ARM_X11_Latex -P X11 -P latex Isabelle2024_linux_arm.tar.gz
docker login
- docker push makarius/isabelle:Isabelle2023
+ docker push makarius/isabelle:Isabelle2024
docker tag ... latest
docker push makarius/isabelle:latest
--- a/Admin/Windows/Cygwin/README Wed Mar 06 09:26:40 2024 +0100
+++ b/Admin/Windows/Cygwin/README Wed Mar 06 09:43:25 2024 +0100
@@ -22,6 +22,7 @@
- https://isabelle.sketis.net/cygwin_2021-1 (Isabelle2021-1)
- https://isabelle.sketis.net/cygwin_2022 (Isabelle2022)
- https://isabelle.sketis.net/cygwin_2023 (Isabelle2023)
+ - https://isabelle.sketis.net/cygwin_2024 (Isabelle2024)
* Apache2 redirects for virtual host isabelle.conf:
```
@@ -57,6 +58,8 @@
Redirect /cygwin_2022/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
Redirect /cygwin_2023/x86_64/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/x86_64/release
Redirect /cygwin_2023/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
+ Redirect /cygwin_2024/x86_64/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/x86_64/release
+ Redirect /cygwin_2024/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
```
* Quasi-component: "isabelle component_cygwin" (as Administrator)
--- a/Admin/components/PLATFORMS Wed Mar 06 09:26:40 2024 +0100
+++ b/Admin/components/PLATFORMS Wed Mar 06 09:43:25 2024 +0100
@@ -47,7 +47,7 @@
macOS 14 Sonoma (studio1 Mac13,2 M1 Ultra, 16+4 cores)
x86_64-windows Windows 10
- x86_64-cygwin Cygwin 3.4.x https://isabelle.sketis.net/cygwin_2023 (x86_64/release)
+ x86_64-cygwin Cygwin 3.5.x https://isabelle.sketis.net/cygwin_2024 (x86_64/release)
64 bit vs. 32 bit platform personality
--- a/Admin/components/bundled-windows Wed Mar 06 09:26:40 2024 +0100
+++ b/Admin/components/bundled-windows Wed Mar 06 09:43:25 2024 +0100
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-cygwin-20230711-1
+cygwin-20240305
windows_app-20240205
--- a/Admin/components/components.sha1 Wed Mar 06 09:26:40 2024 +0100
+++ b/Admin/components/components.sha1 Wed Mar 06 09:43:25 2024 +0100
@@ -80,6 +80,7 @@
6cd34e30e2e650f239d19725c3d15c206fb3a7cf cygwin-20221002.tar.gz
fe8c541722f2fd6940f9e9948928b55fbc32d14b cygwin-20230711-1.tar.gz
bc634cae08dea80238a830955894919af995cf06 cygwin-20230711.tar.gz
+ea23f766909632d8a6c0fefafbde467d1d289383 cygwin-20240305.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
--- a/CONTRIBUTORS Wed Mar 06 09:26:40 2024 +0100
+++ b/CONTRIBUTORS Wed Mar 06 09:43:25 2024 +0100
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* 2023/2024: Makarius Wenzel and Fabian Huch
+ More support for distributed build clusters.
+
* October 2023: Fabian Huch
Support for SMTP mailing.
--- a/NEWS Wed Mar 06 09:26:40 2024 +0100
+++ b/NEWS Wed Mar 06 09:43:25 2024 +0100
@@ -9,6 +9,13 @@
*** General ***
+* Dropped support for very old operating systems. The platform
+base-lines are now as follows:
+
+ - Ubuntu Linux 18.04 LTS
+ - macOS 11 Big Sur
+ - Windows 10 or Windows Server 2012 R2
+
* The arm64-linux platform is now officially supported, although a few
(non-essential) tools are missing:
@@ -17,6 +24,7 @@
- OCaml / OPAM
- Nunchaku + smbc (experimental)
+
*** Document preparation ***
* The bundled LaTeX LNCS style has been updated to version 2.23
@@ -39,12 +47,6 @@
information, see Sledgehammer's documentation relating to
"preplay_timeout". INCOMPATIBILITY.
-* HOL-Analysis: the syntax of Lebesgue integrals (LINT, LBINT, \<integral>, etc.)
-now requires parentheses in most cases. INCOMPATIBILITY.
-
-* HOL-Analysis: corrected the definition of convex function (convex_on)
-to require the underlying set to be convex. INCOMPATIBILITY.
-
* Explicit type class for discrete_linear_ordered_semidom for integral
semidomains with a discrete linear order.
@@ -77,6 +79,12 @@
trans_on_mult
transp_on_multp
+* HOL-Analysis: the syntax of Lebesgue integrals (LINT, LBINT, \<integral>, etc.)
+now requires parentheses in most cases. INCOMPATIBILITY.
+
+* HOL-Analysis: corrected the definition of convex function (convex_on)
+to require the underlying set to be convex. INCOMPATIBILITY.
+
*** Pure ***
@@ -167,19 +175,16 @@
3.3, instead of 3.1. This is the "-old-syntax" variant (Java-like) as
before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY.
-* Update to official Poly/ML 5.9.1.
-
-* Update to OpenJDK 21: the current long-term support version of Java.
+* Isabelle/Scala supports mailing via SMTP, based on new system
+component javamail (previously javax.mail) from jakarta 2.1.2
+using eclipse angus 2.0.2/2.0.1.
* Update to GHC stack 2.15.1 with support for all platforms, including
ARM Linux and Apple Silicon.
-* No longer support for very old versions of macOS and Linux: base-line
-is Ubuntu Linux 18.04 LTS and macOS 11 Big Sur.
-
-* Isabelle/Scala supports mailing via SMTP, based on new system
-component javamail (previously javax.mail) from jakarta 2.1.2
-using eclipse angus 2.0.2/2.0.1.
+* Update to official Poly/ML 5.9.1.
+
+* Update to OpenJDK 21: the current long-term support version of Java.
--- a/src/HOL/Analysis/Set_Integral.thy Wed Mar 06 09:26:40 2024 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Wed Mar 06 09:43:25 2024 +0100
@@ -1746,7 +1746,7 @@
text \<open>We aim to lift results from the real case to arbitrary Banach spaces.
Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \cite{Lang_1993}.
- The theorem allows us to make statements about a function’s value almost everywhere, depending on the value its integral takes on various sets of the measure space.\<close>
+ The theorem allows us to make statements about a function's value almost everywhere, depending on the value its integral takes on various sets of the measure space.\<close>
text \<open>Before we introduce and prove the averaging theorem, we will first show the following lemma which is crucial for our proof.
While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \cite{engelking_1989}.
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Mar 06 09:26:40 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Mar 06 09:43:25 2024 +0100
@@ -599,7 +599,7 @@
val SOME {pre_bnf, absT_info = {abs_inverse, ...},
fp_ctr_sugar = {ctr_defs, ctr_sugar = {ctrs = ctrs0, ...}, ...},
- live_nesting_bnfs = live_nesting_bnfs, ...} =
+ live_nesting_bnfs = live_nesting_bnfs, ...} =
fp_sugar_of ctxt fpT_name;
val ctrs = map (mk_ctr fp_argTs) ctrs0;
@@ -611,7 +611,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
mk_cong_intro_ctr_or_friend_tac ctxt ctr_def
- ([pre_rel_def, abs_inverse] @ live_nesting_rel_eqs) cong_ctor_intro))
+ ([pre_rel_def, abs_inverse] @ live_nesting_rel_eqs) cong_ctor_intro))
|> Thm.close_derivation \<^here>;
val goals = map (mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong) ctrs;
--- a/src/Pure/Admin/component_cygwin.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/Admin/component_cygwin.scala Wed Mar 06 09:43:25 2024 +0100
@@ -8,7 +8,7 @@
object Component_Cygwin {
- val default_mirror: String = "https://isabelle.sketis.net/cygwin_2023"
+ val default_mirror: String = "https://isabelle.sketis.net/cygwin_2024"
val packages: List[String] = List("curl", "libgmp-devel", "nano", "openssh", "perl")
@@ -21,42 +21,42 @@
require(Platform.is_windows, "Windows platform expected")
Isabelle_System.with_tmp_dir("cygwin") { tmp_dir =>
- val cygwin = tmp_dir + Path.explode("cygwin")
- val cygwin_etc = cygwin + Path.explode("etc")
- val cygwin_isabelle = Isabelle_System.make_directory(cygwin + Path.explode("isabelle"))
+ val cygwin = tmp_dir + Path.explode("cygwin")
+ val cygwin_etc = cygwin + Path.explode("etc")
+ val cygwin_isabelle = Isabelle_System.make_directory(cygwin + Path.explode("isabelle"))
- val cygwin_exe_name = mirror + "/setup-x86_64.exe"
- val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe")
- Bytes.write(cygwin_exe,
- try { Bytes.read_url(cygwin_exe_name) }
- catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) })
+ val cygwin_exe_name = mirror + "/setup-x86_64.exe"
+ val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe")
+ Bytes.write(cygwin_exe,
+ try { Bytes.read_url(cygwin_exe_name) }
+ catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) })
- File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror)
+ File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror)
- File.set_executable(cygwin_exe)
- Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check
+ File.set_executable(cygwin_exe)
+ Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check
- val res =
- progress.bash(
- File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" +
- " --local-package-dir 'C:\\temp'" +
- " --root " + File.bash_platform_path(cygwin) +
- " --packages " + quote((packages ::: more_packages).mkString(",")) +
- " --no-shortcuts --no-startmenu --no-desktop --quiet-mode",
- echo = true)
- if (!res.ok || !cygwin_etc.is_dir) error("Failed")
+ val res =
+ progress.bash(
+ File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" +
+ " --local-package-dir 'C:\\temp'" +
+ " --root " + File.bash_platform_path(cygwin) +
+ " --packages " + quote((packages ::: more_packages).mkString(",")) +
+ " --no-shortcuts --no-startmenu --no-desktop --quiet-mode",
+ echo = true)
+ if (!res.ok || !cygwin_etc.is_dir) error("Failed")
- for (name <- List("hosts", "protocols", "services", "networks", "passwd", "group"))
- (cygwin_etc + Path.explode(name)).file.delete
+ for (name <- List("hosts", "protocols", "services", "networks", "passwd", "group"))
+ (cygwin_etc + Path.explode(name)).file.delete
- (cygwin + Path.explode("Cygwin.bat")).file.delete
+ (cygwin + Path.explode("Cygwin.bat")).file.delete
- Isabelle_System.bash("rm -f cygwin/usr/share/man/man1/:.1.gz", cwd = tmp_dir.file).check
+ Isabelle_System.bash("rm -f cygwin/usr/share/man/man1/:.1.gz", cwd = tmp_dir.file).check
- val archive =
- target_dir + Path.explode("cygwin-" + Date.Format.alt_date(Date.now()) + ".tar.gz")
- Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " cygwin", dir = tmp_dir).check
- }
+ val archive =
+ target_dir + Path.explode("cygwin-" + Date.Format.alt_date(Date.now()) + ".tar.gz")
+ Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " cygwin", dir = tmp_dir).check
+ }
}
--- a/src/Pure/Build/build_benchmark.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala Wed Mar 06 09:43:25 2024 +0100
@@ -83,7 +83,7 @@
val local_build_context = build_context.copy(store = Store(local_options))
val build =
- Build_Job.start_session(local_build_context, session, progress, No_Logger, server,
+ Build_Job.start_session(local_build_context, session, progress, new Logger, server,
background, session.sources_shasum, input_shasum, node_info, false)
val timing =
--- a/src/Pure/Build/build_process.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/Build/build_process.scala Wed Mar 06 09:43:25 2024 +0100
@@ -43,7 +43,6 @@
sealed case class Task(
name: String,
deps: List[String],
- info: JSON.Object.T,
build_uuid: String
) {
def is_ready: Boolean = deps.isEmpty
@@ -59,6 +58,8 @@
start_date: Date,
build: Option[Build_Job]
) extends Library.Named {
+ def cancel(): Unit = build.foreach(_.cancel())
+ def is_finished: Boolean = build.isDefined && build.get.is_finished
def join_build: Option[Build_Job.Result] = build.flatMap(_.join)
}
@@ -225,16 +226,8 @@
def is_running(name: String): Boolean = running.isDefinedAt(name)
- def stop_running(): Unit =
- for (job <- running.valuesIterator; build <- job.build) build.cancel()
-
- def build_running: List[Build_Job] =
- List.from(for (job <- running.valuesIterator; build <- job.build) yield build)
-
- def finished_running(): List[Job] =
- List.from(
- for (job <- running.valuesIterator; build <- job.build if build.is_finished)
- yield job)
+ def build_running: List[Job] =
+ List.from(for (job <- running.valuesIterator if job.build.isDefined) yield job)
def add_running(job: Job): State =
copy(running = running + (job.name -> job))
@@ -566,10 +559,9 @@
object Pending {
val name = Generic.name.make_primary_key
val deps = SQL.Column.string("deps")
- val info = SQL.Column.string("info")
val build_uuid = Generic.build_uuid
- val table = make_table(List(name, deps, info, build_uuid), name = "pending")
+ val table = make_table(List(name, deps, build_uuid), name = "pending")
}
def read_pending(db: SQL.Database): List[Task] =
@@ -579,9 +571,8 @@
{ res =>
val name = res.string(Pending.name)
val deps = res.string(Pending.deps)
- val info = res.string(Pending.info)
val build_uuid = res.string(Pending.build_uuid)
- Task(name, split_lines(deps), JSON.Object.parse(info), build_uuid)
+ Task(name, split_lines(deps), build_uuid)
})
def update_pending(
@@ -601,8 +592,7 @@
for (task <- insert) yield { (stmt: SQL.Statement) =>
stmt.string(1) = task.name
stmt.string(2) = cat_lines(task.deps)
- stmt.string(3) = JSON.Format(task.info)
- stmt.string(4) = task.build_uuid
+ stmt.string(3) = task.build_uuid
})
}
@@ -776,7 +766,7 @@
/* collective operations */
- override val tables =
+ override val tables: SQL.Tables =
SQL.Tables(
Base.table,
Workers.table,
@@ -978,7 +968,7 @@
val new_pending =
List.from(
for (session <- sessions1.iterator if !old_pending(session.name))
- yield Build_Process.Task(session.name, session.deps, JSON.Object.empty, build_uuid))
+ yield Build_Process.Task(session.name, session.deps, build_uuid))
val pending1 = new_pending ::: state.pending
state.copy(sessions = sessions1, pending = pending1)
@@ -1135,19 +1125,16 @@
Isabelle_Thread.interrupt_handler(_ => progress.stop()) { build_delay.sleep() }
protected def main_unsynchronized(): Unit = {
- for (job <- _state.finished_running()) {
- job.join_build match {
- case None =>
- _state = _state.remove_running(job.name)
- case Some(result) =>
- val result_name = (job.name, worker_uuid, build_uuid)
- _state = _state.
- remove_pending(job.name).
- remove_running(job.name).
- make_result(result_name,
- result.process_result,
- result.output_shasum,
- node_info = job.node_info)
+ for (job <- _state.build_running.filter(_.is_finished)) {
+ _state = _state.remove_running(job.name)
+ for (result <- job.join_build) {
+ val result_name = (job.name, worker_uuid, build_uuid)
+ _state = _state.
+ remove_pending(job.name).
+ make_result(result_name,
+ result.process_result,
+ result.output_shasum,
+ node_info = job.node_info)
}
}
@@ -1187,7 +1174,7 @@
try {
while (!finished()) {
synchronized_database("Build_Process.main") {
- if (progress.stopped) _state.stop_running()
+ if (progress.stopped) _state.build_running.foreach(_.cancel())
main_unsynchronized()
}
sleep()
--- a/src/Pure/Build/build_schedule.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Wed Mar 06 09:43:25 2024 +0100
@@ -1213,7 +1213,7 @@
remove_schedules(db, remove)
}
- override val tables = SQL.Tables(Schedules.table, Nodes.table)
+ override val tables: SQL.Tables = SQL.Tables(Schedules.table, Nodes.table)
val all_tables: SQL.Tables =
SQL.Tables.list(Build_Process.private_data.tables.list ::: tables.list)
@@ -1328,7 +1328,7 @@
val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
def task(session: Build_Job.Session_Context): Build_Process.Task =
- Build_Process.Task(session.name, session.deps, JSON.Object.empty, build_context.build_uuid)
+ Build_Process.Task(session.name, session.deps, build_context.build_uuid)
val build_state =
Build_Process.State(sessions = sessions, pending = sessions.iterator.map(task).toList)
--- a/src/Pure/Build/resources.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/Build/resources.scala Wed Mar 06 09:43:25 2024 +0100
@@ -24,7 +24,7 @@
class Resources(
val session_background: Sessions.Background,
- val log: Logger = No_Logger,
+ val log: Logger = new Logger,
command_timings: List[Properties.T] = Nil
) {
resources =>
--- a/src/Pure/Concurrent/delay.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/Concurrent/delay.scala Wed Mar 06 09:43:25 2024 +0100
@@ -9,11 +9,11 @@
object Delay {
// delayed event after first invocation
- def first(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+ def first(delay: => Time, log: Logger = new Logger, gui: Boolean = false)(event: => Unit): Delay =
new Delay(true, delay, log, if (gui) GUI_Thread.later { event } else event )
// delayed event after last invocation
- def last(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+ def last(delay: => Time, log: Logger = new Logger, gui: Boolean = false)(event: => Unit): Delay =
new Delay(false, delay, log, if (gui) GUI_Thread.later { event } else event )
}
--- a/src/Pure/General/logger.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/General/logger.scala Wed Mar 06 09:43:25 2024 +0100
@@ -8,42 +8,59 @@
object Logger {
- def make(log_file: Option[Path]): Logger =
- log_file match { case Some(file) => new File_Logger(file) case None => No_Logger }
-
- def make(progress: Progress): Logger =
- new Logger { def apply(msg: => String): Unit = if (progress != null) progress.echo(msg) }
+ def make_file(log_file: Option[Path], guard_time: Time = Time.min): Logger =
+ log_file match {
+ case Some(file) => new File_Logger(file, guard_time)
+ case None => new Logger
+ }
- def make_system_log(progress: Progress, options: Options): Logger =
+ def make_progress(progress: => Progress, guard_time: Time = Time.min): Logger = {
+ val t = guard_time
+ new Logger {
+ override val guard_time: Time = t
+ override def output(msg: => String): Unit =
+ if (progress != null) progress.echo(msg)
+ }
+ }
+
+ def make_system_log(progress: => Progress, options: Options, guard_time: Time = Time.min): Logger =
options.string("system_log") match {
- case "" => No_Logger
- case "-" => make(progress)
- case log_file => make(Some(Path.explode(log_file)))
+ case "" => new Logger
+ case "-" => make_progress(progress, guard_time = guard_time)
+ case log_file => make_file(Some(Path.explode(log_file)), guard_time = guard_time)
}
}
-trait Logger {
- def apply(msg: => String): Unit
+class Logger {
+ val guard_time: Time = Time.min
+ def guard(t: Time): Boolean = t >= guard_time
+ def output(msg: => String): Unit = {}
- def timeit[A](body: => A,
+ final def apply(msg: => String, time: Option[Time] = None): Unit =
+ if (time.isEmpty || guard(time.get)) output(msg)
+
+ final def timeit[A](body: => A,
message: Exn.Result[A] => String = null,
enabled: Boolean = true
): A = Timing.timeit(body, message = message, enabled = enabled, output = apply(_))
}
-object No_Logger extends Logger {
- def apply(msg: => String): Unit = {}
-}
-
-class File_Logger(path: Path) extends Logger {
- def apply(msg: => String): Unit = synchronized { File.append(path, msg + "\n") }
-
+class File_Logger(path: Path, override val guard_time: Time = Time.min)
+extends Logger {
+ override def output(msg: => String): Unit = synchronized { File.append(path, msg + "\n") }
override def toString: String = path.toString
}
-class System_Logger extends Logger {
- def apply(msg: => String): Unit = synchronized {
- if (Platform.is_windows) System.out.println(msg)
- else System.console.writer.println(msg)
+class System_Logger(override val guard_time: Time = Time.min)
+extends Logger {
+ override def output(msg: => String): Unit = synchronized {
+ if (System.console != null && System.console.writer != null) {
+ System.console.writer.println(msg)
+ System.console.writer.flush()
+ }
+ else if (System.out != null) {
+ System.out.println(msg)
+ System.out.flush()
+ }
}
}
--- a/src/Pure/General/sql.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/General/sql.scala Wed Mar 06 09:43:25 2024 +0100
@@ -243,6 +243,12 @@
}
}
+
+ /* access data */
+
+ def transaction_logger(): Logger =
+ new System_Logger(guard_time = Time.guard_property("isabelle.transaction_trace"))
+
abstract class Data(table_prefix: String = "") {
def tables: Tables
@@ -250,7 +256,7 @@
db: Database,
create: Boolean = false,
label: String = "",
- log: Logger = new System_Logger
+ log: Logger = transaction_logger()
)(body: => A): A = {
db.transaction_lock(tables, create = create, label = label, log = log)(body)
}
@@ -468,24 +474,15 @@
tables: Tables,
create: Boolean = false,
label: String = "",
- log: Logger = new System_Logger
+ log: Logger = transaction_logger()
)(body: => A): A = {
- val prop = "isabelle.transaction_trace"
- val trace_min =
- System.getProperty(prop, "") match {
- case Value.Seconds(t) => t
- case "true" => Time.min
- case "false" | "" => Time.max
- case s => error("Bad system property " + prop + ": " + quote(s))
- }
-
val trace_count = - SQL.transaction_count()
val trace_start = Time.now()
var trace_nl = false
def trace(msg: String): Unit = {
val trace_time = Time.now() - trace_start
- if (trace_time >= trace_min) {
+ if (log.guard(trace_time)) {
time_start
val nl =
if (trace_nl) ""
--- a/src/Pure/General/time.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/General/time.scala Wed Mar 06 09:43:25 2024 +0100
@@ -27,6 +27,16 @@
String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L)
+
+ def guard_property(prop: String): Time =
+ System.getProperty(prop, "") match {
+ case Value.Seconds(t) => t
+ case "true" => Time.min
+ case "false" | "" => Time.max
+ case s =>
+ error("Bad system property " + prop + ": " + quote(s) +
+ "\n expected true, false, or time in seconds")
+ }
}
final class Time private(val ms: Long) extends AnyVal {
--- a/src/Pure/PIDE/headless.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/PIDE/headless.scala Wed Mar 06 09:43:25 2024 +0100
@@ -448,7 +448,7 @@
def apply(
options: Options,
session_background: Sessions.Background,
- log: Logger = No_Logger
+ log: Logger = new Logger
): Resources = new Resources(options, session_background, log = log)
def make(
@@ -457,7 +457,7 @@
session_dirs: List[Path] = Nil,
include_sessions: List[String] = Nil,
progress: Progress = new Progress,
- log: Logger = No_Logger
+ log: Logger = new Logger
): Resources = {
val session_background =
Sessions.background(options, session_name, dirs = session_dirs,
@@ -605,7 +605,7 @@
class Resources private[Headless](
val options: Options,
session_background: Sessions.Background,
- log: Logger = No_Logger)
+ log: Logger = new Logger)
extends isabelle.Resources(session_background.check_errors, log = log) {
resources =>
--- a/src/Pure/Tools/dump.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/Tools/dump.scala Wed Mar 06 09:43:25 2024 +0100
@@ -142,7 +142,7 @@
def sessions(
logic: String = default_logic,
- log: Logger = No_Logger
+ log: Logger = new Logger
): List[Session] = {
/* partitions */
@@ -359,7 +359,7 @@
logic: String,
aspects: List[Aspect] = Nil,
progress: Progress = new Progress,
- log: Logger = No_Logger,
+ log: Logger = new Logger,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
output_dir: Path = default_output_dir,
--- a/src/Pure/Tools/server.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/Tools/server.scala Wed Mar 06 09:43:25 2024 +0100
@@ -397,7 +397,7 @@
name: String = default_name,
port: Int = 0,
existing_server: Boolean = false,
- log: Logger = No_Logger
+ log: Logger = new Logger
): (Info, Option[Server]) = {
using(SQLite.open_database(private_data.database, restrict = true)) { db =>
private_data.transaction_lock(db, create = true) {
@@ -495,7 +495,7 @@
sys.exit(if (ok) Process_Result.RC.ok else Process_Result.RC.failure)
}
else {
- val log = Logger.make(log_file)
+ val log = Logger.make_file(log_file)
val (server_info, server) =
init(name, port = port, existing_server = existing_server, log = log)
Output.writeln(server_info.toString, stdout = true)
--- a/src/Pure/Tools/server_commands.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Pure/Tools/server_commands.scala Wed Mar 06 09:43:25 2024 +0100
@@ -123,7 +123,7 @@
def command(
args: Args,
progress: Progress = new Progress,
- log: Logger = No_Logger
+ log: Logger = new Logger
) : (JSON.Object.T, (UUID.T, Headless.Session)) = {
val (_, _, options, session_background) =
try { Session_Build.command(args.build, progress = progress) }
--- a/src/Tools/VSCode/src/channel.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Tools/VSCode/src/channel.scala Wed Mar 06 09:43:25 2024 +0100
@@ -17,7 +17,7 @@
class Channel(
in: InputStream,
out: OutputStream,
- log: Logger = No_Logger,
+ log: Logger = new Logger,
verbose: Boolean = false
) {
/* read message */
--- a/src/Tools/VSCode/src/language_server.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Wed Mar 06 09:43:25 2024 +0100
@@ -73,7 +73,7 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val log = Logger.make(log_file)
+ val log = Logger.make_file(log_file)
val channel = new Channel(System.in, System.out, log, verbose)
val server =
new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
@@ -91,7 +91,7 @@
}
catch {
case exn: Throwable =>
- val channel = new Channel(System.in, System.out, No_Logger)
+ val channel = new Channel(System.in, System.out, new Logger)
channel.error_message(Exn.message(exn))
throw(exn)
}
@@ -108,7 +108,7 @@
session_requirements: Boolean = false,
session_no_build: Boolean = false,
modes: List[String] = Nil,
- log: Logger = No_Logger
+ log: Logger = new Logger
) {
server =>
--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Mar 06 09:26:40 2024 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Mar 06 09:43:25 2024 +0100
@@ -70,7 +70,7 @@
class VSCode_Resources(
val options: Options,
session_background: Sessions.Background,
- log: Logger = No_Logger)
+ log: Logger = new Logger)
extends Resources(session_background, log = log) {
resources =>