author | wenzelm |
Sat, 30 Sep 2017 18:53:38 +0200 | |
changeset 66730 | e76850a09a12 |
parent 66724 | 1e1f9f603385 |
child 66854 | e23d73f43fb6 |
permissions | -rw-r--r-- |
64202 | 1 |
/* Title: Pure/Admin/build_release.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Build full Isabelle distribution from repository. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Build_Release |
|
11 |
{ |
|
64361 | 12 |
sealed case class Bundle_Info( |
13 |
platform_family: String, |
|
14 |
platform_description: String, |
|
66730 | 15 |
main: String, |
16 |
fallback: Option[String]) |
|
64361 | 17 |
{ |
66730 | 18 |
def names: List[String] = main :: fallback.toList |
64361 | 19 |
} |
20 |
||
64203 | 21 |
sealed case class Release_Info( |
66730 | 22 |
date: Date, |
23 |
name: String, |
|
24 |
dist_dir: Path, |
|
25 |
dist_archive: Path, |
|
26 |
dist_library_archive: Path, |
|
27 |
id: String) |
|
64361 | 28 |
{ |
29 |
val bundle_infos: List[Bundle_Info] = |
|
30 |
List(Bundle_Info("linux", "Linux", name + "_app.tar.gz", None), |
|
66724 | 31 |
Bundle_Info("windows", "Windows (64bit)", name + ".exe", None), |
64361 | 32 |
Bundle_Info("macos", "Mac OS X", name + ".dmg", Some(name + "_dmg.tar.gz"))) |
33 |
||
34 |
def bundle_info(platform_family: String): Bundle_Info = |
|
66730 | 35 |
bundle_infos.find(bundle_info => bundle_info.platform_family == platform_family) getOrElse |
64361 | 36 |
error("Unknown platform family " + quote(platform_family)) |
37 |
} |
|
38 |
||
64203 | 39 |
|
66724 | 40 |
private val default_platform_families = List("linux", "windows", "macos") |
64204 | 41 |
|
64202 | 42 |
def build_release(base_dir: Path, |
64909 | 43 |
progress: Progress = No_Progress, |
64202 | 44 |
rev: String = "", |
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
45 |
afp_rev: String = "", |
64202 | 46 |
official_release: Boolean = false, |
47 |
release_name: String = "", |
|
64208 | 48 |
platform_families: List[String] = default_platform_families, |
64211 | 49 |
website: Option[Path] = None, |
64202 | 50 |
build_library: Boolean = false, |
51 |
parallel_jobs: Int = 1, |
|
64203 | 52 |
remote_mac: String = ""): Release_Info = |
64202 | 53 |
{ |
54 |
/* release info */ |
|
55 |
||
64371 | 56 |
Isabelle_System.mkdirs(base_dir) |
57 |
||
64203 | 58 |
val release_info = |
59 |
{ |
|
60 |
val date = Date.now() |
|
65715 | 61 |
val name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date)) |
64203 | 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") |
|
64221 | 65 |
Release_Info(date, name, dist_dir, dist_archive, dist_library_archive, "") |
64203 | 66 |
} |
64202 | 67 |
|
64361 | 68 |
val bundle_infos = platform_families.map(release_info.bundle_info(_)) |
64204 | 69 |
|
64202 | 70 |
|
71 |
/* make distribution */ |
|
72 |
||
64203 | 73 |
val jobs_option = " -j" + parallel_jobs.toString |
74 |
||
64221 | 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 "") + |
|
64304 | 91 |
(if (release_name != "") " -r " + Bash.string(release_name) else "") + |
92 |
(if (rev != "") " " + Bash.string(rev) else ""), |
|
64221 | 93 |
echo = true).check |
94 |
} |
|
95 |
Library.trim_line(File.read(isabelle_ident_file)) |
|
64203 | 96 |
} |
64202 | 97 |
|
98 |
||
99 |
/* make application bundles */ |
|
100 |
||
66730 | 101 |
for (bundle_info <- bundle_infos) { |
64361 | 102 |
val bundle = |
66730 | 103 |
(if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main |
64361 | 104 |
val bundle_archive = release_info.dist_dir + Path.explode(bundle) |
64203 | 105 |
if (bundle_archive.is_file) |
64209 | 106 |
progress.echo("### Application bundle already exists: " + bundle_archive.implode) |
64203 | 107 |
else { |
64361 | 108 |
progress.echo( |
66730 | 109 |
"\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive.implode) |
64203 | 110 |
progress.bash( |
111 |
"isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) + |
|
66730 | 112 |
" " + Bash.string(bundle_info.platform_family) + |
64304 | 113 |
(if (remote_mac == "") "" else " " + Bash.string(remote_mac)), |
64203 | 114 |
echo = true).check |
115 |
} |
|
64202 | 116 |
} |
117 |
||
118 |
||
119 |
/* minimal website */ |
|
120 |
||
64361 | 121 |
for (dir <- website) { |
122 |
val website_platform_bundles = |
|
123 |
for { |
|
66730 | 124 |
bundle_info <- bundle_infos |
64361 | 125 |
bundle <- |
66730 | 126 |
bundle_info.names.find(name => (release_info.dist_dir + Path.explode(name)).is_file) |
127 |
} yield (bundle, bundle_info) |
|
64206 | 128 |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
129 |
val afp_link = |
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
130 |
HTML.link("https://bitbucket.org/isa-afp/afp-devel/commits/" + afp_rev, |
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
131 |
HTML.text("AFP/" + afp_rev)) |
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
132 |
|
65838 | 133 |
HTML.write_document(dir, "index.html", |
134 |
List(HTML.title(release_info.name)), |
|
135 |
List( |
|
136 |
HTML.chapter(release_info.name + " (" + release_id + ")"), |
|
137 |
HTML.itemize( |
|
66730 | 138 |
website_platform_bundles.map({ case (bundle, bundle_info) => |
139 |
List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) ::: |
|
65838 | 140 |
(if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))) |
64202 | 141 |
|
64361 | 142 |
for ((bundle, _) <- website_platform_bundles) |
143 |
File.copy(release_info.dist_dir + Path.explode(bundle), dir) |
|
144 |
} |
|
64202 | 145 |
|
146 |
||
147 |
/* HTML library */ |
|
148 |
||
64203 | 149 |
if (build_library) { |
150 |
if (release_info.dist_library_archive.is_file) |
|
64209 | 151 |
progress.echo("### Library archive already exists: " + |
152 |
release_info.dist_library_archive.implode) |
|
64203 | 153 |
else { |
64316 | 154 |
Isabelle_System.with_tmp_dir("build_release")(tmp_dir => |
155 |
{ |
|
156 |
def execute(script: String): Unit = |
|
157 |
Isabelle_System.bash(script, cwd = tmp_dir.file).check |
|
64935
9437a117408b
insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents:
64909
diff
changeset
|
158 |
def execute_tar(args: String): Unit = |
9437a117408b
insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents:
64909
diff
changeset
|
159 |
Isabelle_System.gnutar(args, cwd = tmp_dir.file).check |
64316 | 160 |
|
161 |
val name = release_info.name |
|
162 |
val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY") |
|
163 |
val bundle = release_info.dist_dir + Path.explode(name + "_" + platform + ".tar.gz") |
|
64935
9437a117408b
insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents:
64909
diff
changeset
|
164 |
execute_tar("xzf " + File.bash_path(bundle)) |
64316 | 165 |
|
166 |
val other_isabelle = |
|
167 |
new Other_Isabelle(progress, tmp_dir + Path.explode(name), name + "-build") |
|
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)) |
|
64936 | 176 |
execute_tar("--owner=root --group=root -czf " + |
177 |
File.bash_path(release_info.dist_library_archive) + |
|
64316 | 178 |
" " + Bash.string(name + "/browser_info")) |
179 |
}) |
|
64203 | 180 |
} |
181 |
} |
|
182 |
||
183 |
||
64221 | 184 |
release_info.copy(id = release_id) |
64202 | 185 |
} |
186 |
||
187 |
||
188 |
||
189 |
/** command line entry point **/ |
|
190 |
||
191 |
def main(args: Array[String]) |
|
192 |
{ |
|
193 |
Command_Line.tool0 { |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
194 |
var afp_rev = "" |
64202 | 195 |
var remote_mac = "" |
196 |
var official_release = false |
|
197 |
var release_name = "" |
|
64211 | 198 |
var website: Option[Path] = None |
64202 | 199 |
var parallel_jobs = 1 |
200 |
var build_library = false |
|
64208 | 201 |
var platform_families = default_platform_families |
64202 | 202 |
var rev = "" |
203 |
||
204 |
val getopts = Getopts(""" |
|
205 |
Usage: Admin/build_release [OPTIONS] BASE_DIR |
|
206 |
||
207 |
Options are: |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
208 |
-A REV corresponding AFP changeset id |
64202 | 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 |
|
64211 | 212 |
-W WEBSITE produce minimal website in given directory |
64202 | 213 |
-j INT maximum number of parallel jobs (default 1) |
214 |
-l build library |
|
65067 | 215 |
-p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) |
64202 | 216 |
-r REV Mercurial changeset id (default: RELEASE or tip) |
217 |
||
218 |
Build Isabelle release in base directory, using the local repository clone. |
|
219 |
""", |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
220 |
"A:" -> (arg => afp_rev = arg), |
64202 | 221 |
"M:" -> (arg => remote_mac = arg), |
222 |
"O" -> (_ => official_release = true), |
|
223 |
"R:" -> (arg => release_name = arg), |
|
64211 | 224 |
"W:" -> (arg => website = Some(Path.explode(arg))), |
64202 | 225 |
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), |
64316 | 226 |
"l" -> (_ => build_library = true), |
64204 | 227 |
"p:" -> (arg => platform_families = Library.space_explode(',', arg)), |
228 |
"r:" -> (arg => rev = arg)) |
|
64202 | 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 |
||
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
235 |
build_release(Path.explode(base_dir), progress = progress, rev = rev, afp_rev = afp_rev, |
64211 | 236 |
official_release = official_release, release_name = release_name, website = website, |
64204 | 237 |
platform_families = |
64208 | 238 |
if (platform_families.isEmpty) default_platform_families else platform_families, |
64202 | 239 |
build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac) |
240 |
} |
|
241 |
} |
|
242 |
} |