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