--- a/Admin/Windows/Cygwin/README Tue Mar 05 16:55:21 2024 +0100
+++ b/Admin/Windows/Cygwin/README Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/Admin/components/PLATFORMS Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/Admin/components/bundled-windows Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/Admin/components/components.sha1 Tue Mar 05 18:42:09 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/NEWS Tue Mar 05 16:55:21 2024 +0100
+++ b/NEWS Tue Mar 05 18:42:09 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:
@@ -174,9 +181,6 @@
* 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.
--- a/src/Pure/Admin/component_cygwin.scala Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Admin/component_cygwin.scala Tue Mar 05 18:42:09 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")
--- a/src/Pure/Build/build_benchmark.scala Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Build/build_process.scala Tue Mar 05 18:42:09 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
@@ -566,10 +565,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 +577,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 +598,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
})
}
@@ -978,7 +974,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)
--- a/src/Pure/Build/build_schedule.scala Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Tue Mar 05 18:42:09 2024 +0100
@@ -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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Build/resources.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Concurrent/delay.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/General/logger.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/General/sql.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/General/time.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/PIDE/headless.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Tools/dump.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Tools/server.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Tools/server_commands.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Tools/VSCode/src/channel.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Tue Mar 05 18:42:09 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 Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Mar 05 18:42:09 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 =>