15 /** platform-specific build **/ |
15 /** platform-specific build **/ |
16 |
16 |
17 sealed case class Platform_Info( |
17 sealed case class Platform_Info( |
18 options: List[String] = Nil, |
18 options: List[String] = Nil, |
19 setup: String = "", |
19 setup: String = "", |
20 copy_files: List[String] = Nil, |
20 libs: Set[String] = Set.empty) |
21 ldd_pattern: Option[(String, Regex)] = None) |
|
22 |
21 |
23 private val platform_info = Map( |
22 private val platform_info = Map( |
24 "linux" -> |
23 "linux" -> |
25 Platform_Info( |
24 Platform_Info( |
26 options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"), |
25 options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"), |
27 ldd_pattern = Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r))), |
26 libs = Set("libgmp")), |
28 "darwin" -> |
27 "darwin" -> |
29 Platform_Info( |
28 Platform_Info( |
30 options = |
29 options = |
31 List("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include", |
30 List("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include", |
32 "CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64", |
31 "CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64", |
33 "LDFLAGS=-segprot POLY rwx rwx"), |
32 "LDFLAGS=-segprot POLY rwx rwx"), |
34 setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin", |
33 setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin", |
35 ldd_pattern = Some(("otool -L", """\s*(\S+lib(?:polyml|gmp).*dylib).*""".r))), |
34 libs = Set("libpolyml", "libgmp")), |
36 "windows" -> |
35 "windows" -> |
37 Platform_Info( |
36 Platform_Info( |
38 options = |
37 options = |
39 List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"), |
38 List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"), |
40 setup = MinGW.environment_export, |
39 setup = MinGW.environment_export, |
41 copy_files = |
40 libs = Set("libgcc_s_seh-1", "libgmp-10", "libstdc++-6", "libwinpthread-1"))) |
42 List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll", |
|
43 "$MSYS/mingw64/bin/libgmp-10.dll", |
|
44 "$MSYS/mingw64/bin/libstdc++-6.dll", |
|
45 "$MSYS/mingw64/bin/libwinpthread-1.dll"))) |
|
46 |
41 |
47 def build_polyml( |
42 def build_polyml( |
48 root: Path, |
43 root: Path, |
49 sha1_root: Option[Path] = None, |
44 sha1_root: Option[Path] = None, |
50 progress: Progress = new Progress, |
45 progress: Progress = new Progress, |
99 rm -rf target |
90 rm -rf target |
100 make compiler && make compiler && make install |
91 make compiler && make compiler && make install |
101 } || { echo "Build failed" >&2; exit 2; } |
92 } || { echo "Build failed" >&2; exit 2; } |
102 """, redirect = true, echo = true).check |
93 """, redirect = true, echo = true).check |
103 |
94 |
104 val ldd_files = |
95 Executable.libraries_closure( |
105 { |
96 root + Path.explode("target/bin/poly"), mingw = mingw, filter = info.libs) |
106 info.ldd_pattern match { |
|
107 case Some((ldd, pattern)) => |
|
108 val lines = bash(root, ldd + " target/bin/poly").check.out_lines |
|
109 for { line <- lines; List(lib) <- pattern.unapplySeq(line) } yield lib |
|
110 case None => Nil |
|
111 } |
|
112 } |
|
113 |
97 |
114 |
98 |
115 /* sha1 library */ |
99 /* sha1 library */ |
116 |
100 |
117 val sha1_files = |
101 val sha1_files = |
118 if (sha1_root.isDefined) { |
102 if (sha1_root.isDefined) { |
119 val dir1 = sha1_root.get |
103 val dir1 = sha1_root.get |
120 bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check |
104 bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check |
121 |
105 |
122 val dir2 = dir1 + Path.explode(sha1_platform) |
106 val dir2 = dir1 + Path.explode(sha1_platform) |
123 File.read_dir(dir2).map(entry => dir2.implode + "/" + entry) |
107 File.read_dir(dir2).map(entry => dir2 + Path.basic(entry)) |
124 } |
108 } |
125 else Nil |
109 else Nil |
126 |
110 |
127 |
111 |
128 /* target */ |
112 /* install */ |
129 |
113 |
130 val target = Path.explode(polyml_platform) |
114 val platform_dir = Path.explode(polyml_platform) |
131 Isabelle_System.rm_tree(target) |
115 Isabelle_System.rm_tree(platform_dir) |
132 Isabelle_System.make_directory(target) |
116 Isabelle_System.make_directory(platform_dir) |
133 |
117 |
134 for (file <- info.copy_files ::: ldd_files ::: sha1_files) |
118 for (file <- sha1_files) File.copy(file, platform_dir) |
135 File.copy(Path.explode(file).expand_env(settings), target) |
|
136 |
119 |
137 for { |
120 for { |
138 d <- List("target/bin", "target/lib") |
121 d <- List("target/bin", "target/lib") |
139 dir = root + Path.explode(d) |
122 dir = root + Path.explode(d) |
140 entry <- File.read_dir(dir) |
123 entry <- File.read_dir(dir) |
141 } File.move(dir + Path.explode(entry), target) |
124 } File.move(dir + Path.explode(entry), platform_dir) |
142 |
|
143 |
|
144 /* poly: library path */ |
|
145 |
|
146 if (platform.is_linux) { |
|
147 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check |
|
148 } |
|
149 else if (platform.is_macos) { |
|
150 for (file <- ldd_files) { |
|
151 bash(target, |
|
152 """install_name_tool -change """ + Bash.string(file) + " " + |
|
153 Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check |
|
154 } |
|
155 } |
|
156 |
125 |
157 |
126 |
158 /* polyc: directory prefix */ |
127 /* polyc: directory prefix */ |
159 |
128 |
160 val Header = "#! */bin/sh".r |
129 val Header = "#! */bin/sh".r |
161 File.change(target + Path.explode("polyc"), txt => |
130 File.change(platform_dir + Path.explode("polyc"), txt => |
162 split_lines(txt) match { |
131 split_lines(txt) match { |
163 case Header() :: lines => |
132 case Header() :: lines => |
164 val lines1 = |
133 val lines1 = |
165 lines.map(line => |
134 lines.map(line => |
166 if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\"" |
135 if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\"" |