author | wenzelm |
Thu, 04 May 2017 12:30:19 +0200 | |
changeset 65715 | e57e5935c6b4 |
parent 65713 | b99b48eb46e5 |
child 65836 | 3b4877fbd9cb |
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, |
|
15 |
main_bundle: String, |
|
16 |
fallback_bundle: Option[String]) |
|
17 |
{ |
|
18 |
def all_bundles: List[String] = main_bundle :: fallback_bundle.toList |
|
19 |
} |
|
20 |
||
64203 | 21 |
sealed case class Release_Info( |
64221 | 22 |
date: Date, name: String, dist_dir: Path, dist_archive: Path, dist_library_archive: Path, |
23 |
id: String) |
|
64361 | 24 |
{ |
25 |
val bundle_infos: List[Bundle_Info] = |
|
26 |
List(Bundle_Info("linux", "Linux", name + "_app.tar.gz", None), |
|
27 |
Bundle_Info("windows", "Windows (32bit)", name + "-win32.exe", None), |
|
28 |
Bundle_Info("windows64", "Windows (64bit)", name + "-win64.exe", None), |
|
29 |
Bundle_Info("macos", "Mac OS X", name + ".dmg", Some(name + "_dmg.tar.gz"))) |
|
30 |
||
31 |
def bundle_info(platform_family: String): Bundle_Info = |
|
32 |
bundle_infos.find(info => info.platform_family == platform_family) getOrElse |
|
33 |
error("Unknown platform family " + quote(platform_family)) |
|
34 |
} |
|
35 |
||
64203 | 36 |
|
64208 | 37 |
private val default_platform_families = List("linux", "windows", "windows64", "macos") |
64204 | 38 |
|
64202 | 39 |
def build_release(base_dir: Path, |
64909 | 40 |
progress: Progress = No_Progress, |
64202 | 41 |
rev: String = "", |
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
42 |
afp_rev: String = "", |
64202 | 43 |
official_release: Boolean = false, |
44 |
release_name: String = "", |
|
64208 | 45 |
platform_families: List[String] = default_platform_families, |
64211 | 46 |
website: Option[Path] = None, |
64202 | 47 |
build_library: Boolean = false, |
48 |
parallel_jobs: Int = 1, |
|
64203 | 49 |
remote_mac: String = ""): Release_Info = |
64202 | 50 |
{ |
51 |
/* release info */ |
|
52 |
||
64371 | 53 |
Isabelle_System.mkdirs(base_dir) |
54 |
||
64203 | 55 |
val release_info = |
56 |
{ |
|
57 |
val date = Date.now() |
|
65715 | 58 |
val name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date)) |
64203 | 59 |
val dist_dir = base_dir + Path.explode("dist-" + name) |
60 |
val dist_archive = dist_dir + Path.explode(name + ".tar.gz") |
|
61 |
val dist_library_archive = dist_dir + Path.explode(name + "_library.tar.gz") |
|
64221 | 62 |
Release_Info(date, name, dist_dir, dist_archive, dist_library_archive, "") |
64203 | 63 |
} |
64202 | 64 |
|
64361 | 65 |
val bundle_infos = platform_families.map(release_info.bundle_info(_)) |
64204 | 66 |
|
64202 | 67 |
|
68 |
/* make distribution */ |
|
69 |
||
64203 | 70 |
val jobs_option = " -j" + parallel_jobs.toString |
71 |
||
64221 | 72 |
val release_id = |
73 |
{ |
|
74 |
val isabelle_ident_file = base_dir + Path.explode("ISABELLE_IDENT") |
|
75 |
val isabelle_dist_file = base_dir + Path.explode("ISABELLE_DIST") |
|
76 |
||
77 |
if (release_info.dist_archive.is_file && |
|
78 |
isabelle_ident_file.is_file && isabelle_dist_file.is_file && |
|
79 |
File.eq(Path.explode(Library.trim_line(File.read(isabelle_dist_file))), |
|
80 |
release_info.dist_archive)) { |
|
81 |
progress.echo("### Release archive already exists: " + release_info.dist_archive.implode) |
|
82 |
} |
|
83 |
else { |
|
84 |
progress.echo("Producing release archive " + release_info.dist_archive.implode + " ...") |
|
85 |
progress.bash( |
|
86 |
"isabelle makedist -d " + File.bash_path(base_dir) + jobs_option + |
|
87 |
(if (official_release) " -O" else "") + |
|
64304 | 88 |
(if (release_name != "") " -r " + Bash.string(release_name) else "") + |
89 |
(if (rev != "") " " + Bash.string(rev) else ""), |
|
64221 | 90 |
echo = true).check |
91 |
} |
|
92 |
Library.trim_line(File.read(isabelle_ident_file)) |
|
64203 | 93 |
} |
64202 | 94 |
|
95 |
||
96 |
/* make application bundles */ |
|
97 |
||
64361 | 98 |
for (info <- bundle_infos) { |
99 |
val bundle = |
|
100 |
(if (remote_mac.isEmpty) info.fallback_bundle else None) getOrElse info.main_bundle |
|
101 |
val bundle_archive = release_info.dist_dir + Path.explode(bundle) |
|
64203 | 102 |
if (bundle_archive.is_file) |
64209 | 103 |
progress.echo("### Application bundle already exists: " + bundle_archive.implode) |
64203 | 104 |
else { |
64361 | 105 |
progress.echo( |
106 |
"\nApplication bundle for " + info.platform_family + ": " + bundle_archive.implode) |
|
64203 | 107 |
progress.bash( |
108 |
"isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) + |
|
64361 | 109 |
" " + Bash.string(info.platform_family) + |
64304 | 110 |
(if (remote_mac == "") "" else " " + Bash.string(remote_mac)), |
64203 | 111 |
echo = true).check |
112 |
} |
|
64202 | 113 |
} |
114 |
||
115 |
||
116 |
/* minimal website */ |
|
117 |
||
64361 | 118 |
for (dir <- website) { |
119 |
val website_platform_bundles = |
|
120 |
for { |
|
121 |
info <- bundle_infos |
|
122 |
bundle <- |
|
123 |
info.all_bundles.find(name => (release_info.dist_dir + Path.explode(name)).is_file) |
|
124 |
} yield (bundle, info) |
|
64206 | 125 |
|
64361 | 126 |
Isabelle_System.mkdirs(dir) |
64211 | 127 |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
128 |
val afp_link = |
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
129 |
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
|
130 |
HTML.text("AFP/" + afp_rev)) |
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
131 |
|
64361 | 132 |
File.write(dir + Path.explode("index.html"), |
133 |
HTML.output_document( |
|
134 |
List(HTML.title(release_info.name)), |
|
135 |
List( |
|
136 |
HTML.chapter(release_info.name + " (" + release_id + ")"), |
|
137 |
HTML.itemize( |
|
138 |
website_platform_bundles.map({ case (bundle, info) => |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
139 |
List(HTML.link(bundle, HTML.text(info.platform_description))) }))) ::: |
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
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 |
} |