| author | paulson | 
| Thu, 19 Oct 2017 17:16:13 +0100 | |
| changeset 66885 | d3d508b23d1d | 
| parent 66047 | 3e8a897042d9 | 
| child 66896 | 85e6748bf8b2 | 
| 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 root = Path.explode("~/html-data/devel")
 | 
| 13 | ||
| 14 | val RELEASE_SNAPSHOT = "release_snapshot" | |
| 15 | val BUILD_LOG_DB = "build_log.db" | |
| 16 | val BUILD_STATUS = "build_status" | |
| 17 | ||
| 18 | val standard_log_dirs = | |
| 19 |     List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
 | |
| 20 | ||
| 21 | ||
| 22 | /* index */ | |
| 23 | ||
| 24 | def make_index() | |
| 25 |   {
 | |
| 26 | val header = "Isabelle Development Resources" | |
| 65770 | 27 | |
| 65838 | 28 | HTML.write_document(root, "index.html", | 
| 29 | List(HTML.title(header)), | |
| 30 | List(HTML.chapter(header), | |
| 31 | HTML.itemize( | |
| 32 | List( | |
| 33 |             HTML.text("Isabelle nightly ") :::
 | |
| 34 |             List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
 | |
| 35 |             HTML.text(" (for all platforms)"),
 | |
| 65770 | 36 | |
| 65838 | 37 |             HTML.text("Isabelle ") :::
 | 
| 38 |             List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
 | |
| 39 |             HTML.text(" information"),
 | |
| 65771 | 40 | |
| 65838 | 41 |             HTML.text("Database with recent ") :::
 | 
| 42 |             List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
 | |
| 43 |             HTML.text(" information (e.g. for ") :::
 | |
| 44 |             List(HTML.link("http://sqlitebrowser.org",
 | |
| 45 |               List(HTML.code(HTML.text("sqlitebrowser"))))) :::
 | |
| 46 |             HTML.text(")")))))
 | |
| 65771 | 47 | } | 
| 65770 | 48 | |
| 49 | ||
| 50 | /* release snapshot */ | |
| 51 | ||
| 52 | def release_snapshot( | |
| 53 | rev: String = "", | |
| 54 | afp_rev: String = "", | |
| 55 | parallel_jobs: Int = 1, | |
| 56 | remote_mac: String = "") | |
| 57 |   {
 | |
| 58 |     Isabelle_System.with_tmp_dir("isadist")(base_dir =>
 | |
| 59 |       {
 | |
| 65793 | 60 | Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT), | 
| 61 | website_dir => | |
| 62 | Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev, | |
| 63 | parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(website_dir))) | |
| 65770 | 64 | }) | 
| 65 | } | |
| 66 | ||
| 67 | ||
| 68 | /* maintain build_log database */ | |
| 69 | ||
| 65771 | 70 | def build_log_database(options: Options, log_dirs: List[Path] = standard_log_dirs) | 
| 65770 | 71 |   {
 | 
| 72 | val store = Build_Log.store(options) | |
| 73 | using(store.open_database())(db => | |
| 74 |     {
 | |
| 66047 
3e8a897042d9
more robust: store important meta info before potential failure;
 wenzelm parents: 
65854diff
changeset | 75 | store.update_database(db, log_dirs) | 
| 65770 | 76 | store.update_database(db, log_dirs, ml_statistics = true) | 
| 65771 | 77 | store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB)) | 
| 65770 | 78 | }) | 
| 79 | } | |
| 65793 | 80 | |
| 81 | ||
| 82 | /* present build status */ | |
| 83 | ||
| 84 | def build_status(options: Options) | |
| 85 |   {
 | |
| 86 | Isabelle_System.update_directory(root + Path.explode(BUILD_STATUS), | |
| 65854 | 87 | dir => Build_Status.build_status(options, target_dir = dir, ml_statistics = true)) | 
| 65793 | 88 | } | 
| 65770 | 89 | } |