--- a/Admin/PLATFORMS Fri Oct 02 17:03:46 2020 +0100
+++ b/Admin/PLATFORMS Fri Oct 02 23:24:20 2020 +0200
@@ -41,12 +41,16 @@
macOS 10.15 Catalina (laramac01 Macmini8,1)
x86_64-windows Windows 7
- x86_64-cygwin Cygwin 2.10 https://isabelle.sketis.net/cygwin_2018 (x86_64/release)
+ x86_64-cygwin Cygwin 2.10 https://isabelle.sketis.net/cygwin_2021 (x86_64/release)
All of the above platforms are 100% supported by Isabelle -- end-users
should not have to care about the differences (at least in theory).
-Exotic platforms like BSD, Solaris, NixOS are not supported.
+Partial support for ARM (e.g. Raspberry Pi) is available:
+
+ arm64-linux Ubuntu 20.04 LTS
+
+Exotic operating systems like BSD, Solaris, NixOS are unsupported.
64 bit vs. 32 bit platform personality
--- a/Admin/components/bundled-windows Fri Oct 02 17:03:46 2020 +0100
+++ b/Admin/components/bundled-windows Fri Oct 02 23:24:20 2020 +0200
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-cygwin-20200323
+cygwin-20201002
windows_app-20181006
--- a/Admin/components/components.sha1 Fri Oct 02 17:03:46 2020 +0100
+++ b/Admin/components/components.sha1 Fri Oct 02 23:24:20 2020 +0200
@@ -58,6 +58,7 @@
cd01fac0ab4fdb50a2bbb6416da3f15a4d540da1 cygwin-20190524.tar.gz
caa616fbab14c1fce790a87db5c4758c1322cf28 cygwin-20200116.tar.gz
f053a9ab01f0be9cb456560f7eff66a8e7ba2fd2 cygwin-20200323.tar.gz
+0107343cd2562618629f73b2581168f0045c3234 cygwin-20201002.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
@@ -200,6 +201,7 @@
eb499a18e7040ca0fe1ca824c9dcb2087c47c9ba opam-2.0.3-1.tar.gz
002f74c9e65e650de2638bf54d7b012b8de76c28 opam-2.0.3.tar.gz
ddb3b438430d9565adbf5e3d913bd52af8337511 opam-2.0.6.tar.gz
+fc66802c169f44511d3be30435eb89a11e635742 opam-2.0.7.tar.gz
1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
--- a/Admin/components/main Fri Oct 02 17:03:46 2020 +0100
+++ b/Admin/components/main Fri Oct 02 23:24:20 2020 +0200
@@ -11,7 +11,7 @@
jortho-1.0-2
kodkodi-1.5.6
nunchaku-0.5
-opam-2.0.6
+opam-2.0.7
polyml-test-a3cfdf648da-1
postgresql-42.2.9
scala-2.12.12
--- a/src/Pure/Admin/build_cygwin.scala Fri Oct 02 17:03:46 2020 +0100
+++ b/src/Pure/Admin/build_cygwin.scala Fri Oct 02 23:24:20 2020 +0200
@@ -9,7 +9,7 @@
object Build_Cygwin
{
- val default_mirror: String = "https://isabelle.sketis.net/cygwin_2020"
+ val default_mirror: String = "https://isabelle.sketis.net/cygwin_2021"
val packages: List[String] =
List("curl", "libgmp-devel", "nano", "perl", "perl-libwww-perl", "rlwrap", "unzip")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_e.scala Fri Oct 02 23:24:20 2020 +0200
@@ -0,0 +1,184 @@
+/* Title: Pure/Admin/build_e.scala
+ Author: Makarius
+
+Build Isabelle E prover component from official downloads.
+*/
+
+package isabelle
+
+
+object Build_E
+{
+ /* build E prover */
+
+ val default_version = "2.5"
+
+ val default_download_url =
+ "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD"
+
+ val default_runepar_url =
+ "https://raw.githubusercontent.com/JUrban/MPTP2/66f03e5b6df8/MaLARea/bin/runepar.pl"
+
+ def build_e(
+ version: String = default_version,
+ download_url: String = default_download_url,
+ runepar_url: String = default_runepar_url,
+ verbose: Boolean = false,
+ progress: Progress = new Progress,
+ target_dir: Path = Path.current)
+ {
+ Isabelle_System.with_tmp_dir("e")(tmp_dir =>
+ {
+ /* component */
+
+ val component_name = "e-" + version
+ val component_dir = target_dir + Path.basic(component_name)
+ if (component_dir.is_dir) error("Component directory already exists: " + component_dir)
+ else {
+ progress.echo("Component " + component_dir)
+ Isabelle_System.mkdirs(component_dir)
+ }
+
+ val platform_name =
+ proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
+ .getOrElse(error("No 64bit platform"))
+
+ val platform_dir = component_dir + Path.basic(platform_name)
+ Isabelle_System.mkdirs(platform_dir)
+
+
+ /* runepar.pl */
+
+ val runepar_path = platform_dir + Path.basic("runepar.pl")
+ Isabelle_System.download(runepar_url, runepar_path, progress = progress)
+
+ File.write(runepar_path,
+ File.read(runepar_path)
+ .replace("#!/usr/bin/perl", "#!/usr/bin/env perl")
+ .replace("bin/eprover", "$ENV{E_HOME}/eprover")
+ .replace("bin/eproof", "$ENV{E_HOME}/eproof"))
+
+ File.set_executable(runepar_path, true)
+
+
+ /* download source */
+
+ val e_url = download_url + "/V_" + version + "/E.tgz"
+ val e_path = tmp_dir + Path.explode("E.tgz")
+ Isabelle_System.download(e_url, e_path, progress = progress)
+
+ Isabelle_System.bash("tar xzf " + e_path, cwd = tmp_dir.file).check
+ Isabelle_System.bash("tar xzf " + e_path + " && mv E src", cwd = component_dir.file).check
+
+
+ /* build */
+
+ progress.echo("Building E prover ...")
+
+ val build_dir = tmp_dir + Path.basic("E")
+ val build_options =
+ {
+ val result = Isabelle_System.bash("./configure --help", cwd = build_dir.file)
+ if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else ""
+ }
+
+ val build_script = "./configure" + build_options + " && make"
+ Isabelle_System.bash(build_script,
+ cwd = build_dir.file,
+ progress_stdout = progress.echo_if(verbose, _),
+ progress_stderr = progress.echo_if(verbose, _)).check
+
+
+ /* install */
+
+ File.copy(build_dir + Path.basic("COPYING"), component_dir + Path.basic("LICENSE"))
+
+ val install_files = List("epclextract", "eproof_ram", "eprover", "eprover-ho")
+ for (name <- install_files ::: install_files.map(_ + ".exe")) {
+ val path = build_dir + Path.basic("PROVER") + Path.basic(name)
+ if (path.is_file) File.copy(path, platform_dir)
+ }
+ Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi",
+ cwd = platform_dir.file).check
+
+ val eproof_ram = platform_dir + Path.basic("eproof_ram")
+ if (eproof_ram.is_file) {
+ File.write(eproof_ram,
+ File.read(eproof_ram)
+ .replace("EXECPATH=.", "EXECPATH=`dirname \"$0\"`"))
+ }
+
+
+ /* settings */
+
+ val etc_dir = component_dir + Path.basic("etc")
+ Isabelle_System.mkdirs(etc_dir)
+ File.write(etc_dir + Path.basic("settings"),
+ """# -*- shell-script -*- :mode=shellscript:
+
+E_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
+E_VERSION=""" + quote(version) + """
+""")
+
+ /* README */
+
+ File.write(component_dir + Path.basic("README"),
+ "This is E prover " + version + " from\n" + e_url + """
+
+The distribution has been built like this:
+
+ cd src && """ + build_script + """
+
+Only a few executables from PROVERS/ have been moved to the platform-specific
+Isabelle component directory: x86_64-linux etc.
+
+This includes a copy of Josef Urban's "runepar.pl" script, modified to use
+the correct path.
+
+
+ Makarius
+ """ + Date.Format.date(Date.now()) + "\n")
+ })
+}
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("build_e", "build Isabelle E prover component from official download",
+ args =>
+ {
+ var download_url = default_download_url
+ var target_dir = Path.current
+ var runepar_url = default_runepar_url
+ var version = default_version
+ var verbose = false
+
+ val getopts = Getopts("""
+Usage: isabelle build_e [OPTIONS] DOWNLOAD
+
+ Options are:
+ -E URL E prover download URL
+ (default: """ + default_download_url + """)
+ -D DIR target directory (default ".")
+ -R URL URL for runepar.pl by Josef Urban
+ (default: """ + default_runepar_url + """)
+ -V VERSION E prover version (default: """ + default_version + """)
+ -v verbose
+
+ Build E prover component from the specified download URLs and version.
+""",
+ "E:" -> (arg => download_url = arg),
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "R:" -> (arg => runepar_url = arg),
+ "V:" -> (arg => version = arg),
+ "v" -> (_ => verbose = true))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress()
+
+ build_e(version = version, download_url = download_url, runepar_url = runepar_url,
+ verbose = verbose, progress = progress, target_dir = target_dir)
+ })
+}
--- a/src/Pure/Admin/build_sqlite.scala Fri Oct 02 17:03:46 2020 +0100
+++ b/src/Pure/Admin/build_sqlite.scala Fri Oct 02 23:24:20 2020 +0200
@@ -58,14 +58,7 @@
/* jar */
val jar = component_dir + Path.basic(download_name).ext("jar")
- progress.echo("Getting " + quote(download_url))
- try {
- Isabelle_System.bash("curl --fail --silent --location " + Bash.string(download_url) +
- " > " + File.bash_path(jar)).check
- }
- catch {
- case ERROR(msg) => cat_error("Failed to download " + quote(download_url), msg)
- }
+ Isabelle_System.download(download_url, jar, progress = progress)
Isabelle_System.with_tmp_dir("sqlite")(jar_dir =>
{
--- a/src/Pure/System/isabelle_system.scala Fri Oct 02 17:03:46 2020 +0100
+++ b/src/Pure/System/isabelle_system.scala Fri Oct 02 23:24:20 2020 +0200
@@ -368,6 +368,21 @@
else error("Expected to find GNU tar executable")
}
+ private lazy val curl_check: Unit =
+ try { bash("curl --version").check }
+ catch { case ERROR(_) => error("Cannot download files: missing curl") }
+
+ def download(url: String, file: Path, progress: Progress = new Progress): Unit =
+ {
+ curl_check
+ progress.echo("Getting " + quote(url))
+ try {
+ bash("curl --fail --silent --location " + Bash.string(url) +
+ " > " + File.bash_path(file)).check
+ }
+ catch { case ERROR(msg) => cat_error("Failed to download " + quote(url), msg) }
+ }
+
def hostname(): String = bash("hostname -s").check.out
def open(arg: String): Unit =
--- a/src/Pure/System/isabelle_tool.scala Fri Oct 02 17:03:46 2020 +0100
+++ b/src/Pure/System/isabelle_tool.scala Fri Oct 02 23:24:20 2020 +0200
@@ -172,6 +172,7 @@
class Admin_Tools extends Isabelle_Scala_Tools(
Build_Cygwin.isabelle_tool,
Build_Doc.isabelle_tool,
+ Build_E.isabelle_tool,
Build_Fonts.isabelle_tool,
Build_JDK.isabelle_tool,
Build_PolyML.isabelle_tool1,
--- a/src/Pure/build-jars Fri Oct 02 17:03:46 2020 +0100
+++ b/src/Pure/build-jars Fri Oct 02 23:24:20 2020 +0200
@@ -13,6 +13,7 @@
src/Pure/Admin/afp.scala
src/Pure/Admin/build_cygwin.scala
src/Pure/Admin/build_doc.scala
+ src/Pure/Admin/build_e.scala
src/Pure/Admin/build_fonts.scala
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_jdk.scala