author | wenzelm |
Fri, 27 Oct 2017 11:46:03 +0200 | |
changeset 66923 | 914935f8a462 |
parent 66910 | 20d61ffa9867 |
child 67045 | 6c94f749410a |
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), |
|
66910 | 31 |
Bundle_Info("windows", "Windows", 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 = |
66854 | 130 |
HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev)) |
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
131 |
|
65838 | 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( |
|
66730 | 137 |
website_platform_bundles.map({ case (bundle, bundle_info) => |
138 |
List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) ::: |
|
65838 | 139 |
(if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))) |
64202 | 140 |
|
64361 | 141 |
for ((bundle, _) <- website_platform_bundles) |
142 |
File.copy(release_info.dist_dir + Path.explode(bundle), dir) |
|
143 |
} |
|
64202 | 144 |
|
145 |
||
146 |
/* HTML library */ |
|
147 |
||
64203 | 148 |
if (build_library) { |
149 |
if (release_info.dist_library_archive.is_file) |
|
64209 | 150 |
progress.echo("### Library archive already exists: " + |
151 |
release_info.dist_library_archive.implode) |
|
64203 | 152 |
else { |
64316 | 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 |
|
64935
9437a117408b
insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents:
64909
diff
changeset
|
157 |
def execute_tar(args: String): Unit = |
9437a117408b
insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents:
64909
diff
changeset
|
158 |
Isabelle_System.gnutar(args, cwd = tmp_dir.file).check |
64316 | 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") |
|
64935
9437a117408b
insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents:
64909
diff
changeset
|
163 |
execute_tar("xzf " + File.bash_path(bundle)) |
64316 | 164 |
|
165 |
val other_isabelle = |
|
166 |
new Other_Isabelle(progress, tmp_dir + Path.explode(name), name + "-build") |
|
167 |
||
168 |
other_isabelle.bash("bin/isabelle build" + jobs_option + |
|
169 |
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + |
|
170 |
" -s -c -a -d '~~/src/Benchmarks'", echo = true).check |
|
171 |
other_isabelle.isabelle_home_user.file.delete |
|
172 |
||
173 |
execute("chmod -R a+r " + Bash.string(name)) |
|
174 |
execute("chmod -R g=o " + Bash.string(name)) |
|
64936 | 175 |
execute_tar("--owner=root --group=root -czf " + |
176 |
File.bash_path(release_info.dist_library_archive) + |
|
64316 | 177 |
" " + Bash.string(name + "/browser_info")) |
178 |
}) |
|
64203 | 179 |
} |
180 |
} |
|
181 |
||
182 |
||
64221 | 183 |
release_info.copy(id = release_id) |
64202 | 184 |
} |
185 |
||
186 |
||
187 |
||
188 |
/** command line entry point **/ |
|
189 |
||
190 |
def main(args: Array[String]) |
|
191 |
{ |
|
192 |
Command_Line.tool0 { |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
193 |
var afp_rev = "" |
64202 | 194 |
var remote_mac = "" |
195 |
var official_release = false |
|
196 |
var release_name = "" |
|
64211 | 197 |
var website: Option[Path] = None |
64202 | 198 |
var parallel_jobs = 1 |
199 |
var build_library = false |
|
64208 | 200 |
var platform_families = default_platform_families |
64202 | 201 |
var rev = "" |
202 |
||
203 |
val getopts = Getopts(""" |
|
204 |
Usage: Admin/build_release [OPTIONS] BASE_DIR |
|
205 |
||
206 |
Options are: |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
207 |
-A REV corresponding AFP changeset id |
64202 | 208 |
-M USER@HOST remote Mac OS X for dmg build |
209 |
-O official release (not release-candidate) |
|
210 |
-R RELEASE proper release with name |
|
64211 | 211 |
-W WEBSITE produce minimal website in given directory |
64202 | 212 |
-j INT maximum number of parallel jobs (default 1) |
213 |
-l build library |
|
65067 | 214 |
-p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) |
64202 | 215 |
-r REV Mercurial changeset id (default: RELEASE or tip) |
216 |
||
217 |
Build Isabelle release in base directory, using the local repository clone. |
|
218 |
""", |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
219 |
"A:" -> (arg => afp_rev = arg), |
64202 | 220 |
"M:" -> (arg => remote_mac = arg), |
221 |
"O" -> (_ => official_release = true), |
|
222 |
"R:" -> (arg => release_name = arg), |
|
64211 | 223 |
"W:" -> (arg => website = Some(Path.explode(arg))), |
64202 | 224 |
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), |
64316 | 225 |
"l" -> (_ => build_library = true), |
66923 | 226 |
"p:" -> (arg => platform_families = space_explode(',', arg)), |
64204 | 227 |
"r:" -> (arg => rev = arg)) |
64202 | 228 |
|
229 |
val more_args = getopts(args) |
|
230 |
val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } |
|
231 |
||
232 |
val progress = new Console_Progress() |
|
233 |
||
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
234 |
build_release(Path.explode(base_dir), progress = progress, rev = rev, afp_rev = afp_rev, |
64211 | 235 |
official_release = official_release, release_name = release_name, website = website, |
64204 | 236 |
platform_families = |
64208 | 237 |
if (platform_families.isEmpty) default_platform_families else platform_families, |
64202 | 238 |
build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac) |
239 |
} |
|
240 |
} |
|
241 |
} |