author | wenzelm |
Sat, 14 Oct 2023 15:26:39 +0200 | |
changeset 78774 | 99ff760cf63a |
parent 78772 | b8c0a45e3381 |
child 78775 | e5b2574f6462 |
permissions | -rw-r--r-- |
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
1 |
/* Title: Pure/Admin/component_polyml.scala |
64483 | 2 |
Author: Makarius |
3 |
||
4 |
Build Poly/ML from sources. |
|
78772 | 5 |
|
6 |
Note: macOS 14 Sonoma requires "LDFLAGS=... -ld64". |
|
64483 | 7 |
*/ |
8 |
||
9 |
package isabelle |
|
10 |
||
11 |
||
69704 | 12 |
import scala.util.matching.Regex |
13 |
||
14 |
||
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
15 |
object Component_PolyML { |
65880 | 16 |
/** platform-specific build **/ |
64496 | 17 |
|
64483 | 18 |
sealed case class Platform_Info( |
19 |
options: List[String] = Nil, |
|
64487 | 20 |
setup: String = "", |
72462
7c552a256ca5
misc tuning and clarification: prefer Executable.libraries_closure;
wenzelm
parents:
72455
diff
changeset
|
21 |
libs: Set[String] = Set.empty) |
64483 | 22 |
|
23 |
private val platform_info = Map( |
|
69704 | 24 |
"linux" -> |
67580
eb64467e8bcf
more robust access to shared libraries for poly executable: avoid global change of LD_LIBRARY_PATH (e.g. relevant for subprocesses);
wenzelm
parents:
66998
diff
changeset
|
25 |
Platform_Info( |
69704 | 26 |
options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"), |
72462
7c552a256ca5
misc tuning and clarification: prefer Executable.libraries_closure;
wenzelm
parents:
72455
diff
changeset
|
27 |
libs = Set("libgmp")), |
69704 | 28 |
"darwin" -> |
64483 | 29 |
Platform_Info( |
73666
4d0df84a5b88
clarified options: implicitly support both x86_64 and arm64;
wenzelm
parents:
73340
diff
changeset
|
30 |
options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"), |
69704 | 31 |
setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin", |
72462
7c552a256ca5
misc tuning and clarification: prefer Executable.libraries_closure;
wenzelm
parents:
72455
diff
changeset
|
32 |
libs = Set("libpolyml", "libgmp")), |
69704 | 33 |
"windows" -> |
64483 | 34 |
Platform_Info( |
35 |
options = |
|
67597 | 36 |
List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"), |
72427 | 37 |
setup = MinGW.environment_export, |
72468 | 38 |
libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread"))) |
64483 | 39 |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
40 |
def polyml_platform(arch_64: Boolean): String = { |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
41 |
val platform = Isabelle_Platform.self |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
42 |
(if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
43 |
} |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
44 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
45 |
def make_polyml( |
64489 | 46 |
root: Path, |
64495 | 47 |
sha1_root: Option[Path] = None, |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
48 |
target_dir: Path = Path.current, |
64493 | 49 |
arch_64: Boolean = false, |
64485
e996c0a5eca9
support other bash executable (notably for msys on Windows);
wenzelm
parents:
64484
diff
changeset
|
50 |
options: List[String] = Nil, |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
51 |
mingw: MinGW = MinGW.none, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
52 |
progress: Progress = new Progress, |
75393 | 53 |
): Unit = { |
64489 | 54 |
if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir)) |
55 |
error("Bad Poly/ML root directory: " + root) |
|
64483 | 56 |
|
72352
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72351
diff
changeset
|
57 |
val platform = Isabelle_Platform.self |
69704 | 58 |
|
72352
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72351
diff
changeset
|
59 |
val sha1_platform = platform.arch_64 + "-" + platform.os_name |
64493 | 60 |
|
64483 | 61 |
val info = |
72352
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72351
diff
changeset
|
62 |
platform_info.getOrElse(platform.os_name, |
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72351
diff
changeset
|
63 |
error("Bad OS platform: " + quote(platform.os_name))) |
64483 | 64 |
|
72455 | 65 |
if (platform.is_linux) Isabelle_System.require_command("chrpath") |
70977 | 66 |
|
64491 | 67 |
|
64495 | 68 |
/* bash */ |
69 |
||
64504 | 70 |
def bash( |
73672
70d3c7009a65
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
wenzelm
parents:
73667
diff
changeset
|
71 |
cwd: Path, script: String, |
70d3c7009a65
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
wenzelm
parents:
73667
diff
changeset
|
72 |
redirect: Boolean = false, |
75393 | 73 |
echo: Boolean = false |
74 |
): Process_Result = { |
|
73672
70d3c7009a65
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
wenzelm
parents:
73667
diff
changeset
|
75 |
val script1 = |
70d3c7009a65
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
wenzelm
parents:
73667
diff
changeset
|
76 |
if (platform.is_arm && platform.is_macos) { |
70d3c7009a65
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
wenzelm
parents:
73667
diff
changeset
|
77 |
"arch -arch arm64 bash -c " + Bash.string(script) |
70d3c7009a65
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
wenzelm
parents:
73667
diff
changeset
|
78 |
} |
70d3c7009a65
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
wenzelm
parents:
73667
diff
changeset
|
79 |
else mingw.bash_script(script) |
70d3c7009a65
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
wenzelm
parents:
73667
diff
changeset
|
80 |
progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo) |
64504 | 81 |
} |
64495 | 82 |
|
83 |
||
64491 | 84 |
/* configure and make */ |
85 |
||
64483 | 86 |
val configure_options = |
67783
839de121665c
more robust build: prevent problems seen with Poly/ML eb94e2820013 on Mac OS X;
wenzelm
parents:
67609
diff
changeset
|
87 |
List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") ::: |
69704 | 88 |
info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit")) |
64483 | 89 |
|
64495 | 90 |
bash(root, |
64487 | 91 |
info.setup + "\n" + |
64485
e996c0a5eca9
support other bash executable (notably for msys on Windows);
wenzelm
parents:
64484
diff
changeset
|
92 |
""" |
e996c0a5eca9
support other bash executable (notably for msys on Windows);
wenzelm
parents:
64484
diff
changeset
|
93 |
[ -f Makefile ] && make distclean |
e996c0a5eca9
support other bash executable (notably for msys on Windows);
wenzelm
parents:
64484
diff
changeset
|
94 |
{ |
e996c0a5eca9
support other bash executable (notably for msys on Windows);
wenzelm
parents:
64484
diff
changeset
|
95 |
./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """ |
e996c0a5eca9
support other bash executable (notably for msys on Windows);
wenzelm
parents:
64484
diff
changeset
|
96 |
rm -rf target |
74635 | 97 |
make && make install |
64485
e996c0a5eca9
support other bash executable (notably for msys on Windows);
wenzelm
parents:
64484
diff
changeset
|
98 |
} || { echo "Build failed" >&2; exit 2; } |
64501 | 99 |
""", redirect = true, echo = true).check |
64485
e996c0a5eca9
support other bash executable (notably for msys on Windows);
wenzelm
parents:
64484
diff
changeset
|
100 |
|
64491 | 101 |
|
64495 | 102 |
/* sha1 library */ |
103 |
||
104 |
val sha1_files = |
|
105 |
if (sha1_root.isDefined) { |
|
106 |
val dir1 = sha1_root.get |
|
72352
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72351
diff
changeset
|
107 |
bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check |
64505 | 108 |
|
72352
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72351
diff
changeset
|
109 |
val dir2 = dir1 + Path.explode(sha1_platform) |
72462
7c552a256ca5
misc tuning and clarification: prefer Executable.libraries_closure;
wenzelm
parents:
72455
diff
changeset
|
110 |
File.read_dir(dir2).map(entry => dir2 + Path.basic(entry)) |
64495 | 111 |
} |
112 |
else Nil |
|
113 |
||
114 |
||
72462
7c552a256ca5
misc tuning and clarification: prefer Executable.libraries_closure;
wenzelm
parents:
72455
diff
changeset
|
115 |
/* install */ |
64484 | 116 |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
117 |
val platform_path = Path.explode(polyml_platform(arch_64)) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
118 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
119 |
val platform_dir = target_dir + platform_path |
72462
7c552a256ca5
misc tuning and clarification: prefer Executable.libraries_closure;
wenzelm
parents:
72455
diff
changeset
|
120 |
Isabelle_System.rm_tree(platform_dir) |
7c552a256ca5
misc tuning and clarification: prefer Executable.libraries_closure;
wenzelm
parents:
72455
diff
changeset
|
121 |
Isabelle_System.make_directory(platform_dir) |
64483 | 122 |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
123 |
val root_platform_dir = Isabelle_System.make_directory(root + platform_path) |
64483 | 124 |
for { |
64484 | 125 |
d <- List("target/bin", "target/lib") |
64489 | 126 |
dir = root + Path.explode(d) |
64483 | 127 |
entry <- File.read_dir(dir) |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
128 |
} Isabelle_System.move_file(dir + Path.explode(entry), root_platform_dir) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
129 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
130 |
Isabelle_System.copy_dir(root_platform_dir, platform_dir, direct = true) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
131 |
for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir) |
67584 | 132 |
|
72469 | 133 |
Executable.libraries_closure( |
134 |
platform_dir + Path.basic("poly").platform_exe, mingw = mingw, filter = info.libs) |
|
135 |
||
67584 | 136 |
|
137 |
/* polyc: directory prefix */ |
|
138 |
||
72378 | 139 |
val Header = "#! */bin/sh".r |
75205 | 140 |
File.change_lines(platform_dir + Path.explode("polyc")) { |
141 |
case Header() :: lines => |
|
142 |
val lines1 = |
|
143 |
lines.map(line => |
|
144 |
if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\"" |
|
145 |
else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\"" |
|
146 |
else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\"" |
|
147 |
else line) |
|
148 |
"#!/usr/bin/env bash" :: lines1 |
|
149 |
case lines => |
|
150 |
error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3))) |
|
75202 | 151 |
} |
64483 | 152 |
} |
153 |
||
154 |
||
64496 | 155 |
|
65880 | 156 |
/** skeleton for component **/ |
157 |
||
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
158 |
val default_polyml_url = "https://github.com/polyml/polyml/archive" |
78774 | 159 |
val default_polyml_version = "90c0dbb2514e" |
160 |
val default_polyml_name = "polyml-5.9.1" |
|
71396
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
161 |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
162 |
val default_sha1_url = "https://isabelle.sketis.net/repos/sha1/archive" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
163 |
val default_sha1_version = "e0239faa6f42" |
71396
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
164 |
|
77191 | 165 |
private def init_src_root(src_dir: Path, input: String, output: String): Unit = { |
166 |
val lines = split_lines(File.read(src_dir + Path.explode(input))) |
|
71396
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
167 |
val ml_files = |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
168 |
for { |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
169 |
line <- lines |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
170 |
rest <- Library.try_unprefix("use", line) |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
171 |
} yield "ML_file" + rest |
65880 | 172 |
|
77191 | 173 |
File.write(src_dir + Path.explode(output), |
71396
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
174 |
"""(* Poly/ML Compiler root file. |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
175 |
|
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
176 |
When this file is open in the Prover IDE, the ML files of the Poly/ML |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
177 |
compiler can be explored interactively. This is a separate copy: it does |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
178 |
not affect the running ML session. *) |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
179 |
""" + ml_files.mkString("\n", "\n", "\n")) |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
180 |
} |
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
181 |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
182 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
183 |
def build_polyml( |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
184 |
options: List[String] = Nil, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
185 |
mingw: MinGW = MinGW.none, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
186 |
component_name: String = "", |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
187 |
polyml_url: String = default_polyml_url, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
188 |
polyml_version: String = default_polyml_version, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
189 |
polyml_name: String = default_polyml_name, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
190 |
sha1_url: String = default_sha1_url, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
191 |
sha1_version: String = default_sha1_version, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
192 |
target_dir: Path = Path.current, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
193 |
progress: Progress = new Progress |
75393 | 194 |
): Unit = { |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
195 |
/* component */ |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
196 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
197 |
val component_name1 = if (component_name.isEmpty) "polyml-" + polyml_version else component_name |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
198 |
val component_dir = Components.Directory(target_dir + Path.basic(component_name1)).create() |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
199 |
progress.echo("Component " + component_dir) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
200 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
201 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
202 |
/* download and build */ |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
203 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
204 |
Isabelle_System.with_tmp_dir("download") { download_dir => |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
205 |
val List(polyml_download, sha1_download) = |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
206 |
for { |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
207 |
(url, version, target) <- |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
208 |
List((polyml_url, polyml_version, "src"), (sha1_url, sha1_version, "sha1")) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
209 |
} yield { |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
210 |
val remote = Url.append_path(url, version + ".tar.gz") |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
211 |
val download = download_dir + Path.basic(version) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
212 |
Isabelle_System.download_file(remote, download.tar.gz, progress = progress) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
213 |
Isabelle_System.extract(download.tar.gz, download, strip = true) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
214 |
Isabelle_System.extract( |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
215 |
download.tar.gz, component_dir.path + Path.basic(target), strip = true) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
216 |
download |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
217 |
} |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
218 |
|
77191 | 219 |
init_src_root(component_dir.src, "RootArm64.ML", "ROOT0.ML") |
220 |
init_src_root(component_dir.src, "RootX86.ML", "ROOT.ML") |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
221 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
222 |
for (arch_64 <- List(false, true)) { |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
223 |
progress.echo("Building " + polyml_platform(arch_64)) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
224 |
make_polyml( |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
225 |
root = polyml_download, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
226 |
sha1_root = Some(sha1_download), |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
227 |
target_dir = component_dir.path, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
228 |
arch_64 = arch_64, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
229 |
options = options, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
230 |
mingw = mingw, |
77510
f5d6cd98b16a
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77191
diff
changeset
|
231 |
progress = if (progress.verbose) progress else new Progress) |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
232 |
} |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
233 |
} |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
234 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
235 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
236 |
/* settings */ |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
237 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
238 |
component_dir.write_settings("""# -*- shell-script -*- :mode=shellscript: |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
239 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
240 |
POLYML_HOME="$COMPONENT" |
71396
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
241 |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
242 |
if [ -n "$ISABELLE_APPLE_PLATFORM64" ] |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
243 |
then |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
244 |
if grep "ML_system_apple.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
245 |
then |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
246 |
ML_PLATFORM="$ISABELLE_PLATFORM64" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
247 |
else |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
248 |
ML_PLATFORM="$ISABELLE_APPLE_PLATFORM64" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
249 |
fi |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
250 |
else |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
251 |
ML_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
252 |
fi |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
253 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
254 |
if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
255 |
then |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
256 |
ML_OPTIONS="--minheap 1000" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
257 |
else |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
258 |
ML_PLATFORM="${ML_PLATFORM/64/64_32}" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
259 |
ML_OPTIONS="--minheap 500" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
260 |
fi |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
261 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
262 |
ML_SYSTEM=""" + Bash.string(polyml_name) + """ |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
263 |
ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
264 |
ML_SOURCES="$POLYML_HOME/src" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
265 |
|
77191 | 266 |
case "$ML_PLATFORM" in |
267 |
*arm64*) |
|
268 |
ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT0.ML" |
|
269 |
;; |
|
270 |
*) |
|
271 |
ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT.ML" |
|
272 |
;; |
|
273 |
esac |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
274 |
""") |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
275 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
276 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
277 |
/* README */ |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
278 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
279 |
File.write(component_dir.README, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
280 |
"""Poly/ML for Isabelle |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
281 |
==================== |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
282 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
283 |
This compilation of Poly/ML (https://www.polyml.org) is based on the |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
284 |
source distribution from |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
285 |
https://github.com/polyml/polyml/commit/""" + polyml_version + """ |
64483 | 286 |
|
78774 | 287 |
This coincides with the official release of Poly/ML 5.9.1, see also |
288 |
https://github.com/polyml/polyml/releases/tag/v5.9.1 |
|
289 |
||
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
290 |
The Isabelle repository provides an administrative tool "isabelle |
78482 | 291 |
component_polyml", which can be used in the polyml component directory as |
292 |
follows: |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
293 |
|
78482 | 294 |
* Linux and macOS |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
295 |
|
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
296 |
$ isabelle component_polyml |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
297 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
298 |
* Windows (Cygwin shell) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
299 |
|
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
300 |
$ isabelle component_polyml -M /cygdrive/c/msys64 |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
301 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
302 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
303 |
Building libgmp on macOS |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
304 |
======================== |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
305 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
306 |
The build_polyml invocations above implicitly use the GNU Multiple Precision |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
307 |
Arithmetic Library (libgmp), but that is not available on macOS by default. |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
308 |
Appending "--without-gmp" to the command-line omits this library. Building |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
309 |
libgmp properly from sources works as follows (library headers and binaries |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
310 |
will be placed in /usr/local). |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
311 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
312 |
* Download: |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
313 |
|
78770
8a7c0f8fc9d2
updated to gmp-6.3.0, for the sake of macOS 14 Sonoma;
wenzelm
parents:
78483
diff
changeset
|
314 |
$ curl https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2 | tar xjf - |
8a7c0f8fc9d2
updated to gmp-6.3.0, for the sake of macOS 14 Sonoma;
wenzelm
parents:
78483
diff
changeset
|
315 |
$ cd gmp-6.3.0 |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
316 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
317 |
* build: |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
318 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
319 |
$ make distclean |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
320 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
321 |
#Intel |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
322 |
$ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
323 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
324 |
#ARM |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
325 |
$ ./configure --enable-cxx --build=aarch64-apple-darwin"$(uname -r)" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
326 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
327 |
$ make && make check |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
328 |
$ sudo make install |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
329 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
330 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
331 |
Makarius |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
332 |
""" + Date.Format.date(Date.now()) + "\n") |
65880 | 333 |
} |
334 |
||
335 |
||
336 |
||
337 |
/** Isabelle tool wrappers **/ |
|
338 |
||
339 |
val isabelle_tool1 = |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
340 |
Isabelle_Tool("make_polyml", "make Poly/ML from existing sources", Scala_Project.here, |
75394 | 341 |
{ args => |
342 |
var mingw = MinGW.none |
|
343 |
var arch_64 = false |
|
344 |
var sha1_root: Option[Path] = None |
|
64483 | 345 |
|
75394 | 346 |
val getopts = Getopts(""" |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
347 |
Usage: isabelle make_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS] |
64483 | 348 |
|
349 |
Options are: |
|
72429 | 350 |
-M DIR msys/mingw root specification for Windows |
72352
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72351
diff
changeset
|
351 |
-m ARCH processor architecture (32 or 64, default: """ + |
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72351
diff
changeset
|
352 |
(if (arch_64) "64" else "32") + """) |
69691 | 353 |
-s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 |
64483 | 354 |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
355 |
Make Poly/ML in the ROOT directory of its sources, with additional |
67593 | 356 |
CONFIGURE_OPTIONS (e.g. --without-gmp). |
64483 | 357 |
""", |
75394 | 358 |
"M:" -> (arg => mingw = MinGW(Path.explode(arg))), |
359 |
"m:" -> |
|
360 |
{ |
|
361 |
case "32" => arch_64 = false |
|
362 |
case "64" => arch_64 = true |
|
363 |
case bad => error("Bad processor architecture: " + quote(bad)) |
|
364 |
}, |
|
365 |
"s:" -> (arg => sha1_root = Some(Path.explode(arg)))) |
|
64483 | 366 |
|
75394 | 367 |
val more_args = getopts(args) |
368 |
val (root, options) = |
|
369 |
more_args match { |
|
370 |
case root :: options => (Path.explode(root), options) |
|
371 |
case Nil => getopts.usage() |
|
372 |
} |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
373 |
make_polyml(root, sha1_root = sha1_root, progress = new Console_Progress, |
75394 | 374 |
arch_64 = arch_64, options = options, mingw = mingw) |
375 |
}) |
|
65880 | 376 |
|
377 |
val isabelle_tool2 = |
|
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
378 |
Isabelle_Tool("component_polyml", "build Poly/ML component from official repository", |
75394 | 379 |
Scala_Project.here, |
380 |
{ args => |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
381 |
var target_dir = Path.current |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
382 |
var mingw = MinGW.none |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
383 |
var component_name = "" |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
384 |
var sha1_url = default_sha1_url |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
385 |
var sha1_version = default_sha1_version |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
386 |
var polyml_url = default_polyml_url |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
387 |
var polyml_version = default_polyml_version |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
388 |
var polyml_name = default_polyml_name |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
389 |
var verbose = false |
75394 | 390 |
|
391 |
val getopts = Getopts(""" |
|
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
392 |
Usage: isabelle component_polyml [OPTIONS] [CONFIGURE_OPTIONS] |
65880 | 393 |
|
394 |
Options are: |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
395 |
-D DIR target directory (default ".") |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
396 |
-M DIR msys/mingw root specification for Windows |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
397 |
-N NAME component name (default: derived from Poly/ML version) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
398 |
-S URL SHA1 repository archive area |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
399 |
(default: """ + quote(default_sha1_url) + """) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
400 |
-T VERSION SHA1 version (default: """ + quote(default_sha1_version) + """) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
401 |
-U URL Poly/ML repository archive area |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
402 |
(default: """ + quote(default_polyml_url) + """) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
403 |
-V VERSION Poly/ML version (default: """ + quote(default_polyml_version) + """) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
404 |
-W NAME Poly/ML name (default: """ + quote(default_polyml_name) + """) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
405 |
-v verbose |
65880 | 406 |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
407 |
Download and build Poly/ML component from source repositories, with additional |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
408 |
CONFIGURE_OPTIONS (e.g. --without-gmp). |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
409 |
""", |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
410 |
"D:" -> (arg => target_dir = Path.explode(arg)), |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
411 |
"M:" -> (arg => mingw = MinGW(Path.explode(arg))), |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
412 |
"N:" -> (arg => component_name = arg), |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
413 |
"S:" -> (arg => sha1_url = arg), |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
414 |
"T:" -> (arg => sha1_version = arg), |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
415 |
"U:" -> (arg => polyml_url = arg), |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
416 |
"V:" -> (arg => polyml_version = arg), |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
417 |
"W:" -> (arg => polyml_name = arg), |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
418 |
"v" -> (_ => verbose = true)) |
71396
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
71117
diff
changeset
|
419 |
|
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
420 |
val options = getopts(args) |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
421 |
|
77510
f5d6cd98b16a
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77191
diff
changeset
|
422 |
val progress = new Console_Progress(verbose = verbose) |
77190
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
423 |
|
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
424 |
build_polyml(options = options, mingw = mingw, component_name = component_name, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
425 |
polyml_url = polyml_url, polyml_version = polyml_version, polyml_name = polyml_name, |
f6ba88f23135
clarified "isabelle build_polyml": download and build everything for current platform;
wenzelm
parents:
76547
diff
changeset
|
426 |
sha1_url = sha1_url, sha1_version = sha1_version, target_dir = target_dir, |
77510
f5d6cd98b16a
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77191
diff
changeset
|
427 |
progress = progress) |
75394 | 428 |
}) |
64483 | 429 |
} |