1/* Title: Pure/Admin/build_polyml.scala 2 Author: Makarius 3 4Build Poly/ML from sources. 5*/ 6 7package isabelle 8 9 10object Build_PolyML 11{ 12 /** platform-specific build **/ 13 14 sealed case class Platform_Info( 15 options: List[String] = Nil, 16 options_multilib: List[String] = Nil, 17 setup: String = "", 18 copy_files: List[String] = Nil) 19 { 20 def platform_options(arch_64: Boolean): List[String] = 21 if (!arch_64 && Isabelle_System.getenv("ISABELLE_PLATFORM64") == "x86_64-linux") 22 options_multilib 23 else options 24 } 25 26 private val platform_info = Map( 27 "x86-linux" -> 28 Platform_Info( 29 options_multilib = 30 List("--build=i386", "CFLAGS=-m32 -O3", "CXXFLAGS=-m32 -O3", "CCASFLAGS=-m32", 31 "LDFLAGS=-Wl,-rpath,_DUMMY_", "--without-gmp"), 32 options = List("LDFLAGS=-Wl,-rpath,_DUMMY_")), 33 "x86_64-linux" -> 34 Platform_Info( 35 options = List("LDFLAGS=-Wl,-rpath,_DUMMY_")), 36 "x86-darwin" -> 37 Platform_Info( 38 options = 39 List("--build=i686-darwin", "CFLAGS=-arch i686 -O3 -I../libffi/include", 40 "CXXFLAGS=-arch i686 -O3 -I../libffi/include", "CCASFLAGS=-arch i686 -O3", 41 "LDFLAGS=-segprot POLY rwx rwx -L/usr/local/lib32"), 42 setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin"), 43 "x86_64-darwin" -> 44 Platform_Info( 45 options = 46 List("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include", 47 "CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64", 48 "LDFLAGS=-segprot POLY rwx rwx"), 49 setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin"), 50 "x86-windows" -> 51 Platform_Info( 52 options = 53 List("--host=i686-w32-mingw32", "CPPFLAGS=-I/mingw32/include", "--disable-windows-gui"), 54 setup = 55 """PATH=/usr/bin:/bin:/mingw32/bin 56 export CONFIG_SITE=/etc/config.site""", 57 copy_files = 58 List("$MSYS/mingw32/bin/libgcc_s_dw2-1.dll", 59 "$MSYS/mingw32/bin/libgmp-10.dll", 60 "$MSYS/mingw32/bin/libstdc++-6.dll")), 61 "x86_64-windows" -> 62 Platform_Info( 63 options = 64 List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"), 65 setup = 66 """PATH=/usr/bin:/bin:/mingw64/bin 67 export CONFIG_SITE=/etc/config.site""", 68 copy_files = 69 List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll", 70 "$MSYS/mingw64/bin/libgmp-10.dll", 71 "$MSYS/mingw64/bin/libstdc++-6.dll"))) 72 73 def build_polyml( 74 root: Path, 75 sha1_root: Option[Path] = None, 76 progress: Progress = No_Progress, 77 arch_64: Boolean = false, 78 options: List[String] = Nil, 79 msys_root: Option[Path] = None) 80 { 81 if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir)) 82 error("Bad Poly/ML root directory: " + root) 83 84 val platform = 85 (if (arch_64) "x86_64" else "x86") + 86 (if (Platform.is_windows) "-windows" else if (Platform.is_macos) "-darwin" else "-linux") 87 88 val info = 89 platform_info.get(platform) getOrElse 90 error("Bad platform identifier: " + quote(platform)) 91 92 val settings = 93 msys_root match { 94 case None if Platform.is_windows => 95 error("Windows requires specification of msys root directory") 96 case None => Isabelle_System.settings() 97 case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode) 98 } 99 100 101 /* bash */ 102 103 def bash( 104 cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = 105 { 106 val script1 = 107 msys_root match { 108 case None => script 109 case Some(msys) => 110 File.bash_path(msys + Path.explode("usr/bin/bash")) + " -c " + Bash.string(script) 111 } 112 progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo) 113 } 114 115 116 /* configure and make */ 117 118 val configure_options = 119 List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") ::: 120 info.platform_options(arch_64) ::: options 121 122 bash(root, 123 info.setup + "\n" + 124 """ 125 [ -f Makefile ] && make distclean 126 { 127 ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """ 128 rm -rf target 129 make compiler && make compiler && make install 130 } || { echo "Build failed" >&2; exit 2; } 131 """, redirect = true, echo = true).check 132 133 val ldd_files = 134 { 135 val ldd_pattern = 136 if (Platform.is_linux) Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r)) 137 else if (Platform.is_macos) Some(("otool -L", """\s*(\S+lib(?:polyml|gmp).*dylib).*""".r)) 138 else None 139 ldd_pattern match { 140 case Some((ldd, pattern)) => 141 val lines = bash(root, ldd + " target/bin/poly").check.out_lines 142 for { line <- lines; List(lib) <- pattern.unapplySeq(line) } yield lib 143 case None => Nil 144 } 145 } 146 147 148 /* sha1 library */ 149 150 val sha1_files = 151 if (sha1_root.isDefined) { 152 val dir1 = sha1_root.get 153 bash(dir1, "./build " + platform, redirect = true, echo = true).check 154 155 val dir2 = dir1 + Path.explode(platform) 156 File.read_dir(dir2).map(entry => dir2.implode + "/" + entry) 157 } 158 else Nil 159 160 161 /* target */ 162 163 val target = Path.explode(platform) 164 Isabelle_System.rm_tree(target) 165 Isabelle_System.mkdirs(target) 166 167 for (file <- info.copy_files ::: ldd_files ::: sha1_files) 168 File.copy(Path.explode(file).expand_env(settings), target) 169 170 for { 171 d <- List("target/bin", "target/lib") 172 dir = root + Path.explode(d) 173 entry <- File.read_dir(dir) 174 } File.move(dir + Path.explode(entry), target) 175 176 177 /* poly: library path */ 178 179 if (Platform.is_linux) { 180 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check 181 } 182 else if (Platform.is_macos) { 183 for (file <- ldd_files) { 184 bash(target, 185 """install_name_tool -change """ + Bash.string(file) + " " + 186 Bash.string("@executable_path/" + Path.explode(file).base_name) + " poly").check 187 } 188 } 189 190 191 /* polyc: directory prefix */ 192 193 { 194 val polyc_path = target + Path.explode("polyc") 195 196 val Header = "#! */bin/sh".r 197 val polyc_patched = 198 split_lines(File.read(polyc_path)) match { 199 case Header() :: lines => 200 val lines1 = 201 lines.map(line => 202 if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\"" 203 else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\"" 204 else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\"" 205 else line) 206 cat_lines("#!/usr/bin/env bash" ::lines1) 207 case lines => 208 error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3))) 209 } 210 File.write(polyc_path, polyc_patched) 211 } 212 } 213 214 215 216 /** skeleton for component **/ 217 218 def build_polyml_component(component: Path, sha1_root: Option[Path] = None) 219 { 220 if (component.is_dir) error("Directory already exists: " + component) 221 222 val etc = component + Path.explode("etc") 223 Isabelle_System.mkdirs(etc) 224 File.copy(Path.explode("~~/Admin/polyml/settings"), etc) 225 File.copy(Path.explode("~~/Admin/polyml/README"), component) 226 227 sha1_root match { 228 case Some(dir) => 229 Mercurial.repository(dir).archive(File.standard_path(component + Path.explode("sha1"))) 230 case None => 231 } 232 } 233 234 235 236 /** Isabelle tool wrappers **/ 237 238 val isabelle_tool1 = 239 Isabelle_Tool("build_polyml", "build Poly/ML from sources", args => 240 { 241 Command_Line.tool0 { 242 var msys_root: Option[Path] = None 243 var arch_64 = false 244 var sha1_root: Option[Path] = None 245 246 val getopts = Getopts(""" 247Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS] 248 249 Options are: 250 -M DIR msys root directory (for Windows) 251 -m ARCH processor architecture (32=x86, 64=x86_64, default: x86) 252 -s DIR sha1 sources, see https://bitbucket.org/isabelle_project/sha1 253 254 Build Poly/ML in the ROOT directory of its sources, with additional 255 CONFIGURE_OPTIONS (e.g. --without-gmp). 256""", 257 "M:" -> (arg => msys_root = Some(Path.explode(arg))), 258 "m:" -> 259 { 260 case "32" | "x86" => arch_64 = false 261 case "64" | "x86_64" => arch_64 = true 262 case bad => error("Bad processor architecture: " + quote(bad)) 263 }, 264 "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) 265 266 val more_args = getopts(args) 267 val (root, options) = 268 more_args match { 269 case root :: options => (Path.explode(root), options) 270 case Nil => getopts.usage() 271 } 272 build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress, 273 arch_64 = arch_64, options = options, msys_root = msys_root) 274 } 275 }, admin = true) 276 277 val isabelle_tool2 = 278 Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args => 279 { 280 Command_Line.tool0 { 281 var sha1_root: Option[Path] = None 282 283 val getopts = Getopts(""" 284Usage: isabelle build_polyml_component [OPTIONS] TARGET 285 286 Options are: 287 -s DIR sha1 sources, see https://bitbucket.org/isabelle_project/sha1 288 289 Make skeleton for Poly/ML component in directory TARGET. 290""", 291 "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) 292 293 val more_args = getopts(args) 294 val component = 295 more_args match { 296 case List(arg) => Path.explode(arg) 297 case _ => getopts.usage() 298 } 299 build_polyml_component(component, sha1_root = sha1_root) 300 } 301 }, admin = true) 302} 303