--- a/etc/build.props Tue Oct 31 17:24:19 2023 +0100
+++ b/etc/build.props Tue Oct 31 17:32:56 2023 +0100
@@ -48,7 +48,6 @@
src/Pure/Admin/component_zipperposition.scala \
src/Pure/Admin/component_zstd.scala \
src/Pure/Admin/isabelle_cronjob.scala \
- src/Pure/Admin/isabelle_devel.scala \
src/Pure/Concurrent/consumer_thread.scala \
src/Pure/Concurrent/counter.scala \
src/Pure/Concurrent/delay.scala \
--- a/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 31 17:24:19 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 31 17:32:56 2023 +0100
@@ -30,6 +30,8 @@
val build_log_dirs =
List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
+ val isabelle_devel: Path = Path.explode("~/html-data/devel")
+
/** logger tasks **/
@@ -45,7 +47,13 @@
val init: Logger_Task =
Logger_Task("init",
{ logger =>
- Isabelle_Devel.make_index()
+ val redirect = "https://isabelle-dev.sketis.net/home/menu/view/20"
+
+ HTML.write_document(isabelle_devel, "index.html",
+ List(
+ XML.Elem(Markup("meta",
+ List("http-equiv" -> "Refresh", "content" -> ("0; url=" + redirect))), Nil)),
+ List(HTML.link(redirect, HTML.text("Isabelle Development Resources"))))
Mercurial.setup_repository(Isabelle_System.afp_repository.root, afp_repos)
@@ -57,7 +65,7 @@
""" -a --include="*/" --include="plain_identify*" --exclude="*" """ +
Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
- val cronjob_log = Isabelle_Devel.isabelle_devel + Path.basic("cronjob-main.log")
+ val cronjob_log = isabelle_devel + Path.basic("cronjob-main.log")
if (!cronjob_log.is_file) {
Files.createSymbolicLink(cronjob_log.java_path, current_log.java_path)
}
@@ -88,8 +96,21 @@
val build_release: Logger_Task =
Logger_Task("build_release", { logger =>
build_release_log.file.delete
- Isabelle_Devel.release_snapshot(logger.options, get_rev(), get_afp_rev(),
- progress = new File_Progress(build_release_log))
+ val rev = get_rev()
+ val afp_rev = get_afp_rev()
+ val progress = new File_Progress(build_release_log)
+
+ Isabelle_System.with_tmp_dir("isadist") { target_dir =>
+ Isabelle_System.update_directory(isabelle_devel + Path.explode("release_snapshot"),
+ { website_dir =>
+ val context = Build_Release.Release_Context(target_dir, progress = progress)
+ Build_Release.build_release_archive(context, rev)
+ Build_Release.build_release(logger.options, context, afp_rev = afp_rev,
+ build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
+ website = Some(website_dir))
+ }
+ )
+ }
})
@@ -618,7 +639,7 @@
logger =>
Build_Log.build_log_database(logger.options, build_log_dirs,
vacuum = true, ml_statistics = true,
- snapshot = Some(Isabelle_Devel.isabelle_devel + Path.explode("build_log.db")))))),
+ snapshot = Some(isabelle_devel + Path.explode("build_log.db")))))),
PAR(
List(remote_builds1, remote_builds2).map(remote_builds =>
SEQUENTIAL(
@@ -631,8 +652,12 @@
.map({ case (rev, afp_rev) => remote_build_history(rev, afp_rev, i, r) })
}
))),
- Logger_Task("build_status",
- logger => Isabelle_Devel.build_status(logger.options))))),
+ Logger_Task("build_status", logger =>
+ Isabelle_System.update_directory(
+ isabelle_devel + Path.explode("build_status"),
+ dir =>
+ Build_Status.build_status(logger.options,
+ target_dir = dir, ml_statistics = true)))))),
exit))))
log_service.shutdown()
--- a/src/Pure/Admin/isabelle_devel.scala Tue Oct 31 17:24:19 2023 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-/* Title: Pure/Admin/isabelle_devel.scala
- Author: Makarius
-
-Website for Isabelle development resources.
-*/
-
-package isabelle
-
-
-object Isabelle_Devel {
- val isabelle_devel: Path = Path.explode("~/html-data/devel")
-
-
- /* index */
-
- def make_index(): Unit = {
- val redirect = "https://isabelle-dev.sketis.net/home/menu/view/20"
-
- HTML.write_document(isabelle_devel, "index.html",
- List(
- XML.Elem(Markup("meta",
- List("http-equiv" -> "Refresh", "content" -> ("0; url=" + redirect))), Nil)),
- List(HTML.link(redirect, HTML.text("Isabelle Development Resources"))))
- }
-
-
- /* release snapshot */
-
- def release_snapshot(options: Options, rev: String, afp_rev: String,
- progress: Progress = new Progress
- ): Unit = {
- Isabelle_System.with_tmp_dir("isadist") { target_dir =>
- Isabelle_System.update_directory(isabelle_devel + Path.explode("release_snapshot"),
- { website_dir =>
- val context = Build_Release.Release_Context(target_dir, progress = progress)
- Build_Release.build_release_archive(context, rev)
- Build_Release.build_release(options, context, afp_rev = afp_rev,
- build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
- website = Some(website_dir))
- }
- )
- }
- }
-
-
- /* present build status */
-
- def build_status(options: Options): Unit = {
- Isabelle_System.update_directory(isabelle_devel + Path.explode("build_status"),
- dir => Build_Status.build_status(options, target_dir = dir, ml_statistics = true))
- }
-}