author | wenzelm |
Mon, 03 Dec 2018 21:32:08 +0100 | |
changeset 69397 | df7d7477284b |
parent 69396 | 56bea34e0f8e |
child 69400 | c19b7b565998 |
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 |
{ |
|
69174 | 12 |
/** release info **/ |
13 |
||
14 |
sealed case class Bundle_Info( |
|
15 |
platform_family: String, |
|
16 |
platform_description: String, |
|
17 |
main: String, |
|
18 |
fallback: Option[String]) |
|
19 |
{ |
|
20 |
def names: List[String] = main :: fallback.toList |
|
21 |
} |
|
22 |
||
23 |
class Release private[Build_Release]( |
|
24 |
val date: Date, |
|
25 |
val dist_name: String, |
|
26 |
val dist_dir: Path, |
|
27 |
val dist_version: String, |
|
28 |
val ident: String) |
|
29 |
{ |
|
30 |
val isabelle_dir: Path = dist_dir + Path.explode(dist_name) |
|
31 |
val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") |
|
32 |
val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") |
|
33 |
||
34 |
val other_isabelle_identifier: String = dist_name + "-build" |
|
35 |
||
69177 | 36 |
def bundle_info(platform_family: String): Bundle_Info = |
37 |
platform_family match { |
|
38 |
case "linux" => Bundle_Info("linux", "Linux", dist_name + "_app.tar.gz", None) |
|
39 |
case "windows" => Bundle_Info("windows", "Windows", dist_name + ".exe", None) |
|
40 |
case "macos" => |
|
41 |
Bundle_Info("macos", "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz")) |
|
42 |
case _ => error("Unknown platform family " + quote(platform_family)) |
|
43 |
} |
|
69174 | 44 |
} |
45 |
||
46 |
||
47 |
||
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
48 |
/** generated content **/ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
49 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
50 |
/* patch release */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
51 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
52 |
private def change_file(dir: Path, name: String, f: String => String) |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
53 |
{ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
54 |
val file = dir + Path.explode(name) |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
55 |
File.write(file, f(File.read(file))) |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
56 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
57 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
58 |
private val getsettings_file: String = "lib/scripts/getsettings" |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
59 |
|
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
60 |
private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
61 |
|
69174 | 62 |
def patch_release(release: Release, is_official: Boolean) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
63 |
{ |
69174 | 64 |
val dir = release.isabelle_dir |
65 |
||
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
66 |
for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala")) |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
67 |
{ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
68 |
change_file(dir, name, |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
69 |
s => |
69392 | 70 |
s.replaceAllLiterally("val is_identified = false", "val is_identified = true") |
71 |
.replaceAllLiterally("val is_official = false", "val is_official = " + is_official)) |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
72 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
73 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
74 |
change_file(dir, getsettings_file, |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
75 |
s => |
69392 | 76 |
s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident)) |
77 |
.replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"", |
|
78 |
"ISABELLE_IDENTIFIER=" + quote(release.dist_name))) |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
79 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
80 |
change_file(dir, "lib/html/library_index_header.template", |
69392 | 81 |
s => s.replaceAllLiterally("{ISABELLE}", release.dist_name)) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
82 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
83 |
for { |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
84 |
name <- |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
85 |
List( |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
86 |
"src/Pure/System/distribution.ML", |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
87 |
"src/Pure/System/distribution.scala", |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
88 |
"lib/Tools/version") } |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
89 |
{ |
69392 | 90 |
change_file(dir, name, |
91 |
s => s.replaceAllLiterally("repository version", release.dist_version)) |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
92 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
93 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
94 |
change_file(dir, "README", |
69392 | 95 |
s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version)) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
96 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
97 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
98 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
99 |
/* ANNOUNCE */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
100 |
|
69174 | 101 |
def make_announce(release: Release) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
102 |
{ |
69174 | 103 |
File.write(release.isabelle_dir + Path.explode("ANNOUNCE"), |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
104 |
""" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
105 |
IMPORTANT NOTE |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
106 |
============== |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
107 |
|
69174 | 108 |
This is a snapshot of Isabelle/""" + release.ident + """ from the repository. |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
109 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
110 |
""") |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
111 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
112 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
113 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
114 |
/* NEWS */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
115 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
116 |
def make_news(other_isabelle: Other_Isabelle, dist_version: String) |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
117 |
{ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
118 |
val target = other_isabelle.isabelle_home + Path.explode("doc") |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
119 |
val target_fonts = target + Path.explode("fonts") |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
120 |
Isabelle_System.mkdirs(target_fonts) |
69360 | 121 |
other_isabelle.copy_fonts(target_fonts) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
122 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
123 |
HTML.write_document(target, "NEWS.html", |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
124 |
List(HTML.title("NEWS (" + dist_version + ")")), |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
125 |
List( |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
126 |
HTML.chapter("NEWS"), |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
127 |
HTML.source( |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
128 |
Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS")))))) |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
129 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
130 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
131 |
|
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
132 |
/* bundled components */ |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
133 |
|
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
134 |
class Bundled(platform: String = "") |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
135 |
{ |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
136 |
def detect(s: String): Boolean = |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
137 |
s.startsWith("#bundled") && !s.startsWith("#bundled ") |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
138 |
|
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
139 |
def apply(name: String): String = |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
140 |
"#bundled" + (if (platform == "") "" else "-" + platform) + ":" + name |
69391
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
141 |
|
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
142 |
private val Pattern1 = ("""^#bundled:(.*)$""").r |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
143 |
private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
144 |
|
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
145 |
def unapply(s: String): Option[String] = |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
146 |
s match { |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
147 |
case Pattern1(name) => Some(name) |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
148 |
case Pattern2(platform1, name) if platform == platform1 => Some(name) |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
149 |
case _ => None |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
150 |
} |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
151 |
} |
69391
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
152 |
|
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
153 |
def record_bundled_components(dir: Path) |
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
154 |
{ |
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
155 |
val catalogs = |
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
156 |
List("main", "bundled").map((_, new Bundled())) ::: |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
157 |
default_platform_families.flatMap(platform => |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
158 |
List(platform, "bundled-" + platform).map((_, new Bundled(platform = platform)))) |
69391
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
159 |
|
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
160 |
File.append(Components.components(dir), |
69391
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
161 |
terminate_lines("#bundled components" :: |
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
162 |
(for { |
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
163 |
(catalog, bundled) <- catalogs.iterator |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
164 |
val path = Components.admin(dir) + Path.basic(catalog) |
69391
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
165 |
if path.is_file |
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
166 |
line <- split_lines(File.read(path)) |
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
167 |
if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build") |
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
168 |
} yield bundled(line)).toList)) |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
169 |
} |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
170 |
|
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
171 |
def get_bundled_components(dir: Path, platform: String): List[String] = |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
172 |
{ |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
173 |
val Bundled = new Bundled(platform) |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
174 |
for (Bundled(name) <- Components.read_components(dir)) yield name |
69391
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
175 |
} |
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
176 |
|
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
177 |
def activate_bundled_components(dir: Path, platform: String) |
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
178 |
{ |
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
179 |
val Bundled = new Bundled(platform) |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
180 |
Components.write_components(dir, |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
181 |
Components.read_components(dir).flatMap(line => |
69391
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
182 |
line match { |
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
183 |
case Bundled(name) => |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
184 |
if (Components.check_dir(Components.contrib(dir, name))) |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
185 |
Some(Components.contrib(name = name).implode) |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
186 |
else None |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
187 |
case _ => if (Bundled.detect(line)) None else Some(line) |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
188 |
})) |
69391
a3c776b9d3dd
manage components similar to makedist_bundle (still inactive);
wenzelm
parents:
69390
diff
changeset
|
189 |
} |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
190 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
191 |
def make_contrib(dir: Path) |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
192 |
{ |
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
193 |
Isabelle_System.mkdirs(Components.contrib(dir)) |
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
194 |
File.write(Components.contrib(dir, "README"), |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
195 |
"""This directory contains add-on components that contribute to the main |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
196 |
Isabelle distribution. Separate licensing conditions apply, see each |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
197 |
directory individually. |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
198 |
""") |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
199 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
200 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
201 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
202 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
203 |
/** build_release **/ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
204 |
|
69390 | 205 |
def distribution_classpath( |
206 |
components_base: Path, |
|
207 |
isabelle_home: Path, |
|
208 |
isabelle_classpath: String): List[Path] = |
|
209 |
{ |
|
210 |
val base = isabelle_home.absolute |
|
211 |
val contrib_base = components_base.absolute |
|
212 |
||
213 |
Path.split(isabelle_classpath).map(path => |
|
214 |
{ |
|
215 |
val abs_path = path.absolute |
|
216 |
File.relative_path(base, abs_path) match { |
|
217 |
case Some(rel_path) => rel_path |
|
218 |
case None => |
|
219 |
File.relative_path(contrib_base, abs_path) match { |
|
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69392
diff
changeset
|
220 |
case Some(rel_path) => Components.contrib() + rel_path |
69390 | 221 |
case None => error("Bad ISABELLE_CLASSPATH element: " + path) |
222 |
} |
|
223 |
} |
|
224 |
}) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar")) |
|
225 |
} |
|
226 |
||
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
227 |
private def execute(dir: Path, script: String): Unit = |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
228 |
Isabelle_System.bash(script, cwd = dir.file).check |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
229 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
230 |
private def execute_tar(dir: Path, args: String): Unit = |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
231 |
Isabelle_System.gnutar(args, cwd = dir.file).check |
64203 | 232 |
|
69170 | 233 |
private def tar_options: String = |
234 |
if (Platform.is_macos) "--owner=root --group=staff" else "--owner=root --group=root" |
|
235 |
||
66724 | 236 |
private val default_platform_families = List("linux", "windows", "macos") |
64204 | 237 |
|
64202 | 238 |
def build_release(base_dir: Path, |
69397 | 239 |
components_base: Option[Path] = None, |
64909 | 240 |
progress: Progress = No_Progress, |
64202 | 241 |
rev: String = "", |
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
242 |
afp_rev: String = "", |
64202 | 243 |
official_release: Boolean = false, |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
244 |
proper_release_name: Option[String] = None, |
64208 | 245 |
platform_families: List[String] = default_platform_families, |
64211 | 246 |
website: Option[Path] = None, |
64202 | 247 |
build_library: Boolean = false, |
248 |
parallel_jobs: Int = 1, |
|
69167 | 249 |
remote_mac: String = ""): Release = |
64202 | 250 |
{ |
69174 | 251 |
val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) |
252 |
||
69167 | 253 |
val release = |
64203 | 254 |
{ |
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
255 |
val date = Date.now() |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
256 |
val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date)) |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
257 |
val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute |
69174 | 258 |
|
259 |
val version = proper_release_name orElse proper_string(rev) getOrElse "tip" |
|
260 |
val ident = |
|
261 |
try { hg.id(version) } |
|
69176 | 262 |
catch { case ERROR(_) => error("Bad repository version: " + version) } |
69174 | 263 |
|
264 |
val dist_version = |
|
265 |
proper_release_name match { |
|
266 |
case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date) |
|
267 |
case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date) |
|
268 |
} |
|
269 |
||
270 |
new Release(date, dist_name, dist_dir, dist_version, ident) |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
271 |
} |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
272 |
|
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
273 |
|
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
274 |
/* make distribution */ |
64202 | 275 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
276 |
if (release.isabelle_archive.is_file) { |
69178 | 277 |
progress.echo("### Release archive already exists: " + release.isabelle_archive) |
69175 | 278 |
|
279 |
val archive_ident = |
|
280 |
Isabelle_System.with_tmp_dir("build_release")(tmp_dir => |
|
281 |
{ |
|
282 |
val getsettings = Path.explode(release.dist_name + "/" + getsettings_file) |
|
283 |
execute_tar(tmp_dir, "-xzf " + |
|
284 |
File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings)) |
|
285 |
split_lines(File.read(tmp_dir + getsettings)) |
|
286 |
.collectFirst({ case ISABELLE_ID(ident) => ident }) |
|
287 |
.getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive)) |
|
288 |
}) |
|
289 |
||
290 |
if (release.ident != archive_ident) { |
|
291 |
error("Mismatch of release identification " + release.ident + |
|
292 |
" vs. archive " + archive_ident) |
|
293 |
} |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
294 |
} |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
295 |
else { |
69178 | 296 |
progress.echo("### Producing release archive " + release.isabelle_archive + " ...") |
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
297 |
|
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
298 |
Isabelle_System.mkdirs(release.dist_dir) |
64221 | 299 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
300 |
if (release.isabelle_dir.is_dir) |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
301 |
error("Directory " + release.isabelle_dir + " already exists") |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
302 |
|
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
303 |
|
69176 | 304 |
progress.echo("### Retrieving Mercurial repository version " + release.ident) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
305 |
|
69174 | 306 |
hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files") |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
307 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
308 |
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
309 |
(release.isabelle_dir + Path.explode(name)).file.delete |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
310 |
} |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
311 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
312 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
313 |
progress.echo("### Preparing distribution " + quote(release.dist_name)) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
314 |
|
69174 | 315 |
patch_release(release, proper_release_name.isDefined && official_release) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
316 |
|
69174 | 317 |
if (proper_release_name.isEmpty) make_announce(release) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
318 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
319 |
make_contrib(release.isabelle_dir) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
320 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
321 |
execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""") |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
322 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
323 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
324 |
/* build tools and documentation */ |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
325 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
326 |
val other_isabelle = |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
327 |
Other_Isabelle(release.isabelle_dir, |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
328 |
isabelle_identifier = release.other_isabelle_identifier, |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
329 |
progress = progress) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
330 |
|
69388 | 331 |
other_isabelle.init_settings( |
69397 | 332 |
other_isabelle.init_components(base = components_base, catalogs = List("main"))) |
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
333 |
other_isabelle.resolve_components(echo = true) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
334 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
335 |
try { |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
336 |
val export_classpath = |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
337 |
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
338 |
other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
339 |
other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
340 |
} |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
341 |
catch { case ERROR(_) => error("Failed to build tools") } |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
342 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
343 |
try { |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
344 |
other_isabelle.bash( |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
345 |
"./bin/isabelle build_doc -a -s -j " + parallel_jobs, echo = true).check |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
346 |
} |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
347 |
catch { case ERROR(_) => error("Failed to build documentation") } |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
348 |
|
69174 | 349 |
make_news(other_isabelle, release.dist_version) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
350 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
351 |
for (name <- List("Admin", "browser_info", "heaps")) { |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
352 |
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
353 |
} |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
354 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
355 |
other_isabelle.cleanup() |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
356 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
357 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
358 |
progress.echo("### Creating distribution archive " + release.isabelle_archive) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
359 |
|
69174 | 360 |
def execute_dist_name(script: String): Unit = |
361 |
Isabelle_System.bash(script, cwd = release.dist_dir.file, |
|
362 |
env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check |
|
363 |
||
364 |
execute_dist_name(""" |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
365 |
set -e |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
366 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
367 |
chmod -R a+r "$DIST_NAME" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
368 |
chmod -R u+w "$DIST_NAME" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
369 |
chmod -R g=o "$DIST_NAME" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
370 |
find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
371 |
""") |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
372 |
|
69171
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
373 |
execute_tar(release.dist_dir, tar_options + " -czf " + |
710845a85944
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
wenzelm
parents:
69170
diff
changeset
|
374 |
File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name)) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
375 |
|
69174 | 376 |
execute_dist_name(""" |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
377 |
set -e |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
378 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
379 |
mv "$DIST_NAME" "${DIST_NAME}-old" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
380 |
mkdir "$DIST_NAME" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
381 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
382 |
mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
383 |
"${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
384 |
mkdir "$DIST_NAME/doc" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
385 |
mv "${DIST_NAME}-old/doc/"*.pdf \ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
386 |
"${DIST_NAME}-old/doc/"*.html \ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
387 |
"${DIST_NAME}-old/doc/"*.css \ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
388 |
"${DIST_NAME}-old/doc/fonts" \ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
389 |
"${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
390 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
391 |
rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
392 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
393 |
rm -rf "${DIST_NAME}-old" |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
394 |
""") |
64203 | 395 |
} |
64202 | 396 |
|
397 |
||
398 |
/* make application bundles */ |
|
399 |
||
69177 | 400 |
val bundle_infos = platform_families.map(release.bundle_info) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
401 |
|
66730 | 402 |
for (bundle_info <- bundle_infos) { |
64361 | 403 |
val bundle = |
66730 | 404 |
(if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main |
69167 | 405 |
val bundle_archive = release.dist_dir + Path.explode(bundle) |
64203 | 406 |
if (bundle_archive.is_file) |
69178 | 407 |
progress.echo("### Application bundle already exists: " + bundle_archive) |
64203 | 408 |
else { |
64361 | 409 |
progress.echo( |
69178 | 410 |
"\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive) |
64203 | 411 |
progress.bash( |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
412 |
"isabelle makedist_bundle " + File.bash_path(release.isabelle_archive) + |
66730 | 413 |
" " + Bash.string(bundle_info.platform_family) + |
64304 | 414 |
(if (remote_mac == "") "" else " " + Bash.string(remote_mac)), |
64203 | 415 |
echo = true).check |
416 |
} |
|
64202 | 417 |
} |
418 |
||
419 |
||
420 |
/* minimal website */ |
|
421 |
||
64361 | 422 |
for (dir <- website) { |
423 |
val website_platform_bundles = |
|
424 |
for { |
|
66730 | 425 |
bundle_info <- bundle_infos |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
426 |
bundle <- bundle_info.names.find(name => (release.dist_dir + Path.explode(name)).is_file) |
66730 | 427 |
} yield (bundle, bundle_info) |
64206 | 428 |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
429 |
val afp_link = |
66854 | 430 |
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
|
431 |
|
65838 | 432 |
HTML.write_document(dir, "index.html", |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
433 |
List(HTML.title(release.dist_name)), |
65838 | 434 |
List( |
69175 | 435 |
HTML.chapter(release.dist_name + " (" + release.ident + ")"), |
65838 | 436 |
HTML.itemize( |
66730 | 437 |
website_platform_bundles.map({ case (bundle, bundle_info) => |
438 |
List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) ::: |
|
65838 | 439 |
(if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))) |
64202 | 440 |
|
64361 | 441 |
for ((bundle, _) <- website_platform_bundles) |
69167 | 442 |
File.copy(release.dist_dir + Path.explode(bundle), dir) |
64361 | 443 |
} |
64202 | 444 |
|
445 |
||
446 |
/* HTML library */ |
|
447 |
||
64203 | 448 |
if (build_library) { |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
449 |
if (release.isabelle_library_archive.is_file) { |
69178 | 450 |
progress.echo("### Library archive already exists: " + release.isabelle_library_archive) |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
451 |
} |
64203 | 452 |
else { |
64316 | 453 |
Isabelle_System.with_tmp_dir("build_release")(tmp_dir => |
454 |
{ |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
455 |
val name = release.dist_name |
64316 | 456 |
val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY") |
69167 | 457 |
val bundle = release.dist_dir + Path.explode(name + "_" + platform + ".tar.gz") |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
458 |
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) |
64316 | 459 |
|
460 |
val other_isabelle = |
|
67045 | 461 |
Other_Isabelle(tmp_dir + Path.explode(name), |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
462 |
isabelle_identifier = release.other_isabelle_identifier, progress = progress) |
64316 | 463 |
|
68755
67d6f1708ea4
enforce ML_system_64: more robust as cold build, without command_timings;
wenzelm
parents:
67045
diff
changeset
|
464 |
Isabelle_System.mkdirs(other_isabelle.etc) |
67d6f1708ea4
enforce ML_system_64: more robust as cold build, without command_timings;
wenzelm
parents:
67045
diff
changeset
|
465 |
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") |
67d6f1708ea4
enforce ML_system_64: more robust as cold build, without command_timings;
wenzelm
parents:
67045
diff
changeset
|
466 |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
467 |
other_isabelle.bash("bin/isabelle build -j " + parallel_jobs + |
64316 | 468 |
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + |
469 |
" -s -c -a -d '~~/src/Benchmarks'", echo = true).check |
|
470 |
other_isabelle.isabelle_home_user.file.delete |
|
471 |
||
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
472 |
execute(tmp_dir, "chmod -R a+r " + Bash.string(name)) |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
473 |
execute(tmp_dir, "chmod -R g=o " + Bash.string(name)) |
69170 | 474 |
execute_tar(tmp_dir, |
475 |
tar_options + " -czf " + File.bash_path(release.isabelle_library_archive) + |
|
64316 | 476 |
" " + Bash.string(name + "/browser_info")) |
477 |
}) |
|
64203 | 478 |
} |
479 |
} |
|
480 |
||
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
481 |
release |
64202 | 482 |
} |
483 |
||
484 |
||
485 |
||
486 |
/** command line entry point **/ |
|
487 |
||
488 |
def main(args: Array[String]) |
|
489 |
{ |
|
490 |
Command_Line.tool0 { |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
491 |
var afp_rev = "" |
69397 | 492 |
var components_base: Option[Path] = None |
64202 | 493 |
var remote_mac = "" |
494 |
var official_release = false |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
495 |
var proper_release_name: Option[String] = None |
64211 | 496 |
var website: Option[Path] = None |
64202 | 497 |
var parallel_jobs = 1 |
498 |
var build_library = false |
|
64208 | 499 |
var platform_families = default_platform_families |
64202 | 500 |
var rev = "" |
501 |
||
502 |
val getopts = Getopts(""" |
|
503 |
Usage: Admin/build_release [OPTIONS] BASE_DIR |
|
504 |
||
505 |
Options are: |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
506 |
-A REV corresponding AFP changeset id |
69397 | 507 |
-C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib) |
64202 | 508 |
-M USER@HOST remote Mac OS X for dmg build |
509 |
-O official release (not release-candidate) |
|
510 |
-R RELEASE proper release with name |
|
64211 | 511 |
-W WEBSITE produce minimal website in given directory |
64202 | 512 |
-j INT maximum number of parallel jobs (default 1) |
513 |
-l build library |
|
65067 | 514 |
-p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) |
64202 | 515 |
-r REV Mercurial changeset id (default: RELEASE or tip) |
516 |
||
517 |
Build Isabelle release in base directory, using the local repository clone. |
|
518 |
""", |
|
64405
81bac77929d9
just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents:
64371
diff
changeset
|
519 |
"A:" -> (arg => afp_rev = arg), |
69397 | 520 |
"C:" -> (arg => components_base = Some(Path.explode(arg))), |
64202 | 521 |
"M:" -> (arg => remote_mac = arg), |
522 |
"O" -> (_ => official_release = true), |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
523 |
"R:" -> (arg => proper_release_name = Some(arg)), |
64211 | 524 |
"W:" -> (arg => website = Some(Path.explode(arg))), |
64202 | 525 |
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), |
64316 | 526 |
"l" -> (_ => build_library = true), |
66923 | 527 |
"p:" -> (arg => platform_families = space_explode(',', arg)), |
64204 | 528 |
"r:" -> (arg => rev = arg)) |
64202 | 529 |
|
530 |
val more_args = getopts(args) |
|
531 |
val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } |
|
532 |
||
533 |
val progress = new Console_Progress() |
|
534 |
||
69397 | 535 |
build_release(Path.explode(base_dir), components_base = components_base, progress = progress, |
536 |
rev = rev, afp_rev = afp_rev, official_release = official_release, |
|
537 |
proper_release_name = proper_release_name, website = website, |
|
64204 | 538 |
platform_families = |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
539 |
if (platform_families.isEmpty) default_platform_families |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69167
diff
changeset
|
540 |
else platform_families, |
64202 | 541 |
build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac) |
542 |
} |
|
543 |
} |
|
544 |
} |