1/*  Title:      Pure/Admin/build_release.scala
2    Author:     Makarius
3
4Build full Isabelle distribution from repository.
5*/
6
7package isabelle
8
9
10object Build_Release
11{
12  sealed case class Bundle_Info(
13    platform_family: String,
14    platform_description: String,
15    main: String,
16    fallback: Option[String])
17  {
18    def names: List[String] = main :: fallback.toList
19  }
20
21  sealed case class Release_Info(
22    date: Date,
23    name: String,
24    dist_dir: Path,
25    dist_archive: Path,
26    dist_library_archive: Path,
27    id: String)
28  {
29    val bundle_infos: List[Bundle_Info] =
30      List(Bundle_Info("linux", "Linux", name + "_app.tar.gz", None),
31        Bundle_Info("windows", "Windows", name + ".exe", None),
32        Bundle_Info("macos", "Mac OS X", name + ".dmg", Some(name + "_dmg.tar.gz")))
33
34    def bundle_info(platform_family: String): Bundle_Info =
35      bundle_infos.find(bundle_info => bundle_info.platform_family == platform_family) getOrElse
36        error("Unknown platform family " + quote(platform_family))
37  }
38
39
40  private val default_platform_families = List("linux", "windows", "macos")
41
42  def build_release(base_dir: Path,
43    progress: Progress = No_Progress,
44    rev: String = "",
45    afp_rev: String = "",
46    official_release: Boolean = false,
47    release_name: String = "",
48    platform_families: List[String] = default_platform_families,
49    website: Option[Path] = None,
50    build_library: Boolean = false,
51    parallel_jobs: Int = 1,
52    remote_mac: String = ""): Release_Info =
53  {
54    /* release info */
55
56    Isabelle_System.mkdirs(base_dir)
57
58    val release_info =
59    {
60      val date = Date.now()
61      val name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
62      val dist_dir = base_dir + Path.explode("dist-" + name)
63      val dist_archive = dist_dir + Path.explode(name + ".tar.gz")
64      val dist_library_archive = dist_dir + Path.explode(name + "_library.tar.gz")
65      Release_Info(date, name, dist_dir, dist_archive, dist_library_archive, "")
66    }
67
68    val bundle_infos = platform_families.map(release_info.bundle_info(_))
69
70
71    /* make distribution */
72
73    val jobs_option = " -j" + parallel_jobs.toString
74
75    val release_id =
76    {
77      val isabelle_ident_file = base_dir + Path.explode("ISABELLE_IDENT")
78      val isabelle_dist_file = base_dir + Path.explode("ISABELLE_DIST")
79
80      if (release_info.dist_archive.is_file &&
81          isabelle_ident_file.is_file && isabelle_dist_file.is_file &&
82          File.eq(Path.explode(Library.trim_line(File.read(isabelle_dist_file))),
83            release_info.dist_archive)) {
84        progress.echo("### Release archive already exists: " + release_info.dist_archive.implode)
85      }
86      else {
87        progress.echo("Producing release archive " + release_info.dist_archive.implode + " ...")
88        progress.bash(
89          "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option +
90            (if (official_release) " -O" else "") +
91            (if (release_name != "") " -r " + Bash.string(release_name) else "") +
92            (if (rev != "") " " + Bash.string(rev) else ""),
93          echo = true).check
94      }
95      Library.trim_line(File.read(isabelle_ident_file))
96    }
97
98
99    /* make application bundles */
100
101    for (bundle_info <- bundle_infos) {
102      val bundle =
103        (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main
104      val bundle_archive = release_info.dist_dir + Path.explode(bundle)
105      if (bundle_archive.is_file)
106        progress.echo("### Application bundle already exists: " + bundle_archive.implode)
107      else {
108        progress.echo(
109          "\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive.implode)
110        progress.bash(
111          "isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) +
112            " " + Bash.string(bundle_info.platform_family) +
113            (if (remote_mac == "") "" else " " + Bash.string(remote_mac)),
114          echo = true).check
115      }
116    }
117
118
119    /* minimal website */
120
121    for (dir <- website) {
122      val website_platform_bundles =
123        for {
124          bundle_info <- bundle_infos
125          bundle <-
126            bundle_info.names.find(name => (release_info.dist_dir + Path.explode(name)).is_file)
127        } yield (bundle, bundle_info)
128
129      val afp_link =
130        HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev))
131
132      HTML.write_document(dir, "index.html",
133        List(HTML.title(release_info.name)),
134        List(
135          HTML.chapter(release_info.name + " (" + release_id + ")"),
136          HTML.itemize(
137            website_platform_bundles.map({ case (bundle, bundle_info) =>
138              List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) :::
139        (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link)))))
140
141      for ((bundle, _) <- website_platform_bundles)
142        File.copy(release_info.dist_dir + Path.explode(bundle), dir)
143    }
144
145
146    /* HTML library */
147
148    if (build_library) {
149      if (release_info.dist_library_archive.is_file)
150        progress.echo("### Library archive already exists: " +
151          release_info.dist_library_archive.implode)
152      else {
153        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
154          {
155            def execute(script: String): Unit =
156              Isabelle_System.bash(script, cwd = tmp_dir.file).check
157            def execute_tar(args: String): Unit =
158              Isabelle_System.gnutar(args, cwd = tmp_dir.file).check
159
160            val name = release_info.name
161            val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY")
162            val bundle = release_info.dist_dir + Path.explode(name + "_" + platform + ".tar.gz")
163            execute_tar("xzf " + File.bash_path(bundle))
164
165            val other_isabelle =
166              Other_Isabelle(tmp_dir + Path.explode(name),
167                isabelle_identifier = name + "-build", progress = progress)
168
169            other_isabelle.bash("bin/isabelle build" + jobs_option +
170                " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
171                " -s -c -a -d '~~/src/Benchmarks'", echo = true).check
172            other_isabelle.isabelle_home_user.file.delete
173
174            execute("chmod -R a+r " + Bash.string(name))
175            execute("chmod -R g=o " + Bash.string(name))
176            execute_tar("--owner=root --group=root -czf " +
177              File.bash_path(release_info.dist_library_archive) +
178              " " + Bash.string(name + "/browser_info"))
179          })
180      }
181    }
182
183
184    release_info.copy(id = release_id)
185  }
186
187
188
189  /** command line entry point **/
190
191  def main(args: Array[String])
192  {
193    Command_Line.tool0 {
194      var afp_rev = ""
195      var remote_mac = ""
196      var official_release = false
197      var release_name = ""
198      var website: Option[Path] = None
199      var parallel_jobs = 1
200      var build_library = false
201      var platform_families = default_platform_families
202      var rev = ""
203
204      val getopts = Getopts("""
205Usage: Admin/build_release [OPTIONS] BASE_DIR
206
207  Options are:
208    -A REV       corresponding AFP changeset id
209    -M USER@HOST remote Mac OS X for dmg build
210    -O           official release (not release-candidate)
211    -R RELEASE   proper release with name
212    -W WEBSITE   produce minimal website in given directory
213    -j INT       maximum number of parallel jobs (default 1)
214    -l           build library
215    -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
216    -r REV       Mercurial changeset id (default: RELEASE or tip)
217
218  Build Isabelle release in base directory, using the local repository clone.
219""",
220        "A:" -> (arg => afp_rev = arg),
221        "M:" -> (arg => remote_mac = arg),
222        "O" -> (_ => official_release = true),
223        "R:" -> (arg => release_name = arg),
224        "W:" -> (arg => website = Some(Path.explode(arg))),
225        "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
226        "l" -> (_ => build_library = true),
227        "p:" -> (arg => platform_families = space_explode(',', arg)),
228        "r:" -> (arg => rev = arg))
229
230      val more_args = getopts(args)
231      val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() }
232
233      val progress = new Console_Progress()
234
235      build_release(Path.explode(base_dir), progress = progress, rev = rev, afp_rev = afp_rev,
236        official_release = official_release, release_name = release_name, website = website,
237        platform_families =
238          if (platform_families.isEmpty) default_platform_families else platform_families,
239        build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac)
240    }
241  }
242}
243