48 root: Path, |
48 root: Path, |
49 sha1_root: Option[Path] = None, |
49 sha1_root: Option[Path] = None, |
50 progress: Progress = new Progress, |
50 progress: Progress = new Progress, |
51 arch_64: Boolean = false, |
51 arch_64: Boolean = false, |
52 options: List[String] = Nil, |
52 options: List[String] = Nil, |
53 msys_root: Option[Path] = None) |
53 mingw: MinGW = MinGW.none) |
54 { |
54 { |
55 if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir)) |
55 if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir)) |
56 error("Bad Poly/ML root directory: " + root) |
56 error("Bad Poly/ML root directory: " + root) |
57 |
57 |
58 val platform = Isabelle_Platform.self |
58 val platform = Isabelle_Platform.self |
67 val info = |
67 val info = |
68 platform_info.getOrElse(platform.os_name, |
68 platform_info.getOrElse(platform.os_name, |
69 error("Bad OS platform: " + quote(platform.os_name))) |
69 error("Bad OS platform: " + quote(platform.os_name))) |
70 |
70 |
71 val settings = |
71 val settings = |
72 msys_root match { |
72 if (!Platform.is_windows) Isabelle_System.settings() |
73 case None if platform.is_windows => |
73 else Isabelle_System.settings() + ("MSYS" -> mingw.get_root.expand.implode) |
74 error("Windows requires specification of msys root directory") |
|
75 case None => Isabelle_System.settings() |
|
76 case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode) |
|
77 } |
|
78 |
74 |
79 if (platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) { |
75 if (platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) { |
80 error("""Missing "chrpath" executable on Linux""") |
76 error("""Missing "chrpath" executable on Linux""") |
81 } |
77 } |
82 |
78 |
84 /* bash */ |
80 /* bash */ |
85 |
81 |
86 def bash( |
82 def bash( |
87 cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |
83 cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |
88 { |
84 { |
89 val script1 = |
85 progress.bash(mingw.bash_script(script), cwd = cwd.file, redirect = redirect, echo = echo) |
90 msys_root match { |
|
91 case None => script |
|
92 case Some(msys) => |
|
93 File.bash_path(msys + Path.explode("usr/bin/bash")) + " -c " + Bash.string(script) |
|
94 } |
|
95 progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo) |
|
96 } |
86 } |
97 |
87 |
98 |
88 |
99 /* configure and make */ |
89 /* configure and make */ |
100 |
90 |
247 /** Isabelle tool wrappers **/ |
237 /** Isabelle tool wrappers **/ |
248 |
238 |
249 val isabelle_tool1 = |
239 val isabelle_tool1 = |
250 Isabelle_Tool("build_polyml", "build Poly/ML from sources", args => |
240 Isabelle_Tool("build_polyml", "build Poly/ML from sources", args => |
251 { |
241 { |
252 var msys_root: Option[Path] = None |
242 var mingw = MinGW.none |
253 var arch_64 = Isabelle_Platform.self.is_arm |
243 var arch_64 = Isabelle_Platform.self.is_arm |
254 var sha1_root: Option[Path] = None |
244 var sha1_root: Option[Path] = None |
255 |
245 |
256 val getopts = Getopts(""" |
246 val getopts = Getopts(""" |
257 Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS] |
247 Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS] |
258 |
248 |
259 Options are: |
249 Options are: |
260 -M DIR msys root directory (for Windows) |
250 -M DIR msys/mingw root specification for Windows |
261 -m ARCH processor architecture (32 or 64, default: """ + |
251 -m ARCH processor architecture (32 or 64, default: """ + |
262 (if (arch_64) "64" else "32") + """) |
252 (if (arch_64) "64" else "32") + """) |
263 -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 |
253 -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 |
264 |
254 |
265 Build Poly/ML in the ROOT directory of its sources, with additional |
255 Build Poly/ML in the ROOT directory of its sources, with additional |
266 CONFIGURE_OPTIONS (e.g. --without-gmp). |
256 CONFIGURE_OPTIONS (e.g. --without-gmp). |
267 """, |
257 """, |
268 "M:" -> (arg => msys_root = Some(Path.explode(arg))), |
258 "M:" -> (arg => mingw = MinGW.root(Path.explode(arg))), |
269 "m:" -> |
259 "m:" -> |
270 { |
260 { |
271 case "32" => arch_64 = false |
261 case "32" => arch_64 = false |
272 case "64" => arch_64 = true |
262 case "64" => arch_64 = true |
273 case bad => error("Bad processor architecture: " + quote(bad)) |
263 case bad => error("Bad processor architecture: " + quote(bad)) |
279 more_args match { |
269 more_args match { |
280 case root :: options => (Path.explode(root), options) |
270 case root :: options => (Path.explode(root), options) |
281 case Nil => getopts.usage() |
271 case Nil => getopts.usage() |
282 } |
272 } |
283 build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress, |
273 build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress, |
284 arch_64 = arch_64, options = options, msys_root = msys_root) |
274 arch_64 = arch_64, options = options, mingw = mingw) |
285 }) |
275 }) |
286 |
276 |
287 val isabelle_tool2 = |
277 val isabelle_tool2 = |
288 Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args => |
278 Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args => |
289 { |
279 { |