55 msys_root: Option[Path] = None) |
55 msys_root: Option[Path] = None) |
56 { |
56 { |
57 if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir)) |
57 if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir)) |
58 error("Bad Poly/ML root directory: " + root) |
58 error("Bad Poly/ML root directory: " + root) |
59 |
59 |
60 val platform_arch = if (arch_64) "x86_64" else "x86_64_32" |
60 val platform = Isabelle_Platform.self |
61 val platform_os = Platform.os_name |
61 val platform_arch = |
62 |
62 if (arch_64) platform.arch_64 |
63 val platform = platform_arch + "-" + platform_os |
63 else if (platform.is_intel) "x86_64_32" |
64 val platform_64 = "x86_64-" + platform_os |
64 else platform.arch_32 |
|
65 |
|
66 val polyml_platform = platform_arch + "-" + platform.os_name |
|
67 val sha1_platform = platform.arch_64 + "-" + platform.os_name |
65 |
68 |
66 val info = |
69 val info = |
67 platform_info.getOrElse(platform_os, |
70 platform_info.getOrElse(platform.os_name, |
68 error("Bad OS platform: " + quote(platform_os))) |
71 error("Bad OS platform: " + quote(platform.os_name))) |
69 |
72 |
70 val settings = |
73 val settings = |
71 msys_root match { |
74 msys_root match { |
72 case None if Platform.is_windows => |
75 case None if platform.is_windows => |
73 error("Windows requires specification of msys root directory") |
76 error("Windows requires specification of msys root directory") |
74 case None => Isabelle_System.settings() |
77 case None => Isabelle_System.settings() |
75 case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode) |
78 case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode) |
76 } |
79 } |
77 |
80 |
78 if (Platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) { |
81 if (platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) { |
79 error("""Missing "chrpath" executable on Linux""") |
82 error("""Missing "chrpath" executable on Linux""") |
80 } |
83 } |
81 |
84 |
82 |
85 |
83 /* bash */ |
86 /* bash */ |
126 /* sha1 library */ |
129 /* sha1 library */ |
127 |
130 |
128 val sha1_files = |
131 val sha1_files = |
129 if (sha1_root.isDefined) { |
132 if (sha1_root.isDefined) { |
130 val dir1 = sha1_root.get |
133 val dir1 = sha1_root.get |
131 bash(dir1, "./build " + platform_64, redirect = true, echo = true).check |
134 bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check |
132 |
135 |
133 val dir2 = dir1 + Path.explode(platform_64) |
136 val dir2 = dir1 + Path.explode(sha1_platform) |
134 File.read_dir(dir2).map(entry => dir2.implode + "/" + entry) |
137 File.read_dir(dir2).map(entry => dir2.implode + "/" + entry) |
135 } |
138 } |
136 else Nil |
139 else Nil |
137 |
140 |
138 |
141 |
139 /* target */ |
142 /* target */ |
140 |
143 |
141 val target = Path.explode(platform) |
144 val target = Path.explode(polyml_platform) |
142 Isabelle_System.rm_tree(target) |
145 Isabelle_System.rm_tree(target) |
143 Isabelle_System.mkdirs(target) |
146 Isabelle_System.mkdirs(target) |
144 |
147 |
145 for (file <- info.copy_files ::: ldd_files ::: sha1_files) |
148 for (file <- info.copy_files ::: ldd_files ::: sha1_files) |
146 File.copy(Path.explode(file).expand_env(settings), target) |
149 File.copy(Path.explode(file).expand_env(settings), target) |
152 } File.move(dir + Path.explode(entry), target) |
155 } File.move(dir + Path.explode(entry), target) |
153 |
156 |
154 |
157 |
155 /* poly: library path */ |
158 /* poly: library path */ |
156 |
159 |
157 if (Platform.is_linux) { |
160 if (platform.is_linux) { |
158 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check |
161 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check |
159 } |
162 } |
160 else if (Platform.is_macos) { |
163 else if (platform.is_macos) { |
161 for (file <- ldd_files) { |
164 for (file <- ldd_files) { |
162 bash(target, |
165 bash(target, |
163 """install_name_tool -change """ + Bash.string(file) + " " + |
166 """install_name_tool -change """ + Bash.string(file) + " " + |
164 Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check |
167 Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check |
165 } |
168 } |
255 |
258 |
256 val isabelle_tool1 = |
259 val isabelle_tool1 = |
257 Isabelle_Tool("build_polyml", "build Poly/ML from sources", args => |
260 Isabelle_Tool("build_polyml", "build Poly/ML from sources", args => |
258 { |
261 { |
259 var msys_root: Option[Path] = None |
262 var msys_root: Option[Path] = None |
260 var arch_64 = false |
263 var arch_64 = Isabelle_Platform.self.is_arm |
261 var sha1_root: Option[Path] = None |
264 var sha1_root: Option[Path] = None |
262 |
265 |
263 val getopts = Getopts(""" |
266 val getopts = Getopts(""" |
264 Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS] |
267 Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS] |
265 |
268 |
266 Options are: |
269 Options are: |
267 -M DIR msys root directory (for Windows) |
270 -M DIR msys root directory (for Windows) |
268 -m ARCH processor architecture (32=x86_64_32, 64=x86_64, default: 32) |
271 -m ARCH processor architecture (32 or 64, default: """ + |
|
272 (if (arch_64) "64" else "32") + """) |
269 -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 |
273 -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 |
270 |
274 |
271 Build Poly/ML in the ROOT directory of its sources, with additional |
275 Build Poly/ML in the ROOT directory of its sources, with additional |
272 CONFIGURE_OPTIONS (e.g. --without-gmp). |
276 CONFIGURE_OPTIONS (e.g. --without-gmp). |
273 """, |
277 """, |
274 "M:" -> (arg => msys_root = Some(Path.explode(arg))), |
278 "M:" -> (arg => msys_root = Some(Path.explode(arg))), |
275 "m:" -> |
279 "m:" -> |
276 { |
280 { |
277 case "32" | "x86_64_32" => arch_64 = false |
281 case "32" => arch_64 = false |
278 case "64" | "x86_64" => arch_64 = true |
282 case "64" => arch_64 = true |
279 case bad => error("Bad processor architecture: " + quote(bad)) |
283 case bad => error("Bad processor architecture: " + quote(bad)) |
280 }, |
284 }, |
281 "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) |
285 "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) |
282 |
286 |
283 val more_args = getopts(args) |
287 val more_args = getopts(args) |