| author | wenzelm | 
| Wed, 25 Sep 2019 19:40:00 +0200 | |
| changeset 70757 | 6a835635fa93 | 
| parent 70105 | eadd87383e30 | 
| child 71272 | 1e7319957408 | 
| permissions | -rw-r--r-- | 
| 65770 | 1 | /* Title: Pure/Admin/isabelle_devel.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 4 | Website for Isabelle development resources. | |
| 5 | */ | |
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 10 | object Isabelle_Devel | |
| 11 | {
 | |
| 65771 | 12 | val RELEASE_SNAPSHOT = "release_snapshot" | 
| 13 | val BUILD_LOG_DB = "build_log.db" | |
| 14 | val BUILD_STATUS = "build_status" | |
| 67854 
8374c80165e1
publish current log file, e.g. for easy error detection;
 wenzelm parents: 
66896diff
changeset | 15 | val CRONJOB_LOG = "cronjob-main.log" | 
| 
8374c80165e1
publish current log file, e.g. for easy error detection;
 wenzelm parents: 
66896diff
changeset | 16 | |
| 
8374c80165e1
publish current log file, e.g. for easy error detection;
 wenzelm parents: 
66896diff
changeset | 17 |   val root = Path.explode("~/html-data/devel")
 | 
| 
8374c80165e1
publish current log file, e.g. for easy error detection;
 wenzelm parents: 
66896diff
changeset | 18 | val cronjob_log = root + Path.basic(CRONJOB_LOG) | 
| 65771 | 19 | |
| 20 | ||
| 21 | /* index */ | |
| 22 | ||
| 23 | def make_index() | |
| 24 |   {
 | |
| 25 | val header = "Isabelle Development Resources" | |
| 65770 | 26 | |
| 65838 | 27 | HTML.write_document(root, "index.html", | 
| 28 | List(HTML.title(header)), | |
| 29 | List(HTML.chapter(header), | |
| 30 | HTML.itemize( | |
| 31 | List( | |
| 32 |             HTML.text("Isabelle nightly ") :::
 | |
| 33 |             List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
 | |
| 34 |             HTML.text(" (for all platforms)"),
 | |
| 65770 | 35 | |
| 68229 | 36 |             HTML.text("Cronjob ") ::: List(HTML.link(CRONJOB_LOG, HTML.text("log file"))),
 | 
| 37 | ||
| 65838 | 38 |             HTML.text("Isabelle ") :::
 | 
| 39 |             List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
 | |
| 40 |             HTML.text(" information"),
 | |
| 65771 | 41 | |
| 65838 | 42 |             HTML.text("Database with recent ") :::
 | 
| 43 |             List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
 | |
| 44 |             HTML.text(" information (e.g. for ") :::
 | |
| 68224 | 45 |             List(HTML.link("https://sqlitebrowser.org",
 | 
| 65838 | 46 |               List(HTML.code(HTML.text("sqlitebrowser"))))) :::
 | 
| 68229 | 47 |             HTML.text(")")))))
 | 
| 65771 | 48 | } | 
| 65770 | 49 | |
| 50 | ||
| 51 | /* release snapshot */ | |
| 52 | ||
| 53 | def release_snapshot( | |
| 69401 
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
 wenzelm parents: 
68229diff
changeset | 54 | options: Options, | 
| 65770 | 55 | rev: String = "", | 
| 56 | afp_rev: String = "", | |
| 69432 
d072f3287ffa
discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
 wenzelm parents: 
69401diff
changeset | 57 | parallel_jobs: Int = 1) | 
| 65770 | 58 |   {
 | 
| 59 |     Isabelle_System.with_tmp_dir("isadist")(base_dir =>
 | |
| 60 |       {
 | |
| 65793 | 61 | Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT), | 
| 62 | website_dir => | |
| 69401 
7a1b7b737c02
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
 wenzelm parents: 
68229diff
changeset | 63 | Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev, | 
| 70105 | 64 | parallel_jobs = parallel_jobs, | 
| 65 |               build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
 | |
| 66 | website = Some(website_dir))) | |
| 65770 | 67 | }) | 
| 68 | } | |
| 69 | ||
| 70 | ||
| 71 | /* maintain build_log database */ | |
| 72 | ||
| 66896 | 73 | def build_log_database(options: Options, log_dirs: List[Path]) | 
| 65770 | 74 |   {
 | 
| 75 | val store = Build_Log.store(options) | |
| 76 | using(store.open_database())(db => | |
| 77 |     {
 | |
| 66047 
3e8a897042d9
more robust: store important meta info before potential failure;
 wenzelm parents: 
65854diff
changeset | 78 | store.update_database(db, log_dirs) | 
| 65770 | 79 | store.update_database(db, log_dirs, ml_statistics = true) | 
| 65771 | 80 | store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB)) | 
| 65770 | 81 | }) | 
| 82 | } | |
| 65793 | 83 | |
| 84 | ||
| 85 | /* present build status */ | |
| 86 | ||
| 87 | def build_status(options: Options) | |
| 88 |   {
 | |
| 89 | Isabelle_System.update_directory(root + Path.explode(BUILD_STATUS), | |
| 65854 | 90 | dir => Build_Status.build_status(options, target_dir = dir, ml_statistics = true)) | 
| 65793 | 91 | } | 
| 65770 | 92 | } |