1 files changed, 219 insertions, 0 deletions
diff --git a/package.py b/package.py
new file mode 100755
index 00000000..721bb0eb
--- /dev/null
+++ b/package.py
@@ -0,0 +1,219 @@
+#!/usr/bin/env python3
+
+from fnmatch import fnmatch
+from os import path
+import argparse
+import json
+import os
+import re
+import subprocess
+import sys
+import time
+import urllib.request
+import zipfile
+
+# Configuration
+
+## Where do we fetch the list of releases from?
+RELEASES_URL = "https://api.github.com/repos/Z3Prover/z3/releases/latest"
+## How do we extract info from the name of a release file?
+RELEASE_REGEXP = re.compile(r"^(?P<directory>z3-[0-9\.]+-(?P<platform>x86|x64)-(?P<os>[a-z0-9\.\-]+)).zip$", re.IGNORECASE)
+
+## Where are the sources?
+SOURCE_DIRECTORY = "Source"
+## Where do the binaries get put?
+BINARIES_DIRECTORY = "Binaries"
+## Where do we store the built packages and cache files?
+DESTINATION_DIRECTORY = "Package"
+
+## What's the root folder of the archive?
+DAFNY_PACKAGE_PREFIX = path.join("dafny")
+## What sub-folder of the packages does z3 go into?
+Z3_PACKAGE_PREFIX = path.join("z3")
+
+## What do we take from the z3 archive? (Glob syntax)
+Z3_INTERESTING_FILES = ["LICENSE.txt", "bin/*"]
+
+## On unix systems, which Dafny files should be marked as executable? (Glob syntax; Z3's permissions are preserved)
+UNIX_EXECUTABLES = ["dafny", "dafny-server"]
+
+## What do we take from Dafny's Binaries folder?
+DLLs = ["AbsInt",
+        "Basetypes",
+        "CodeContractsExtender",
+        "Concurrency",
+        "Core",
+        "DafnyPipeline",
+        "Doomed",
+        "ExecutionEngine",
+        "Graph",
+        "Houdini",
+        "Model",
+        "ModelViewer",
+        "ParserHelper",
+        "Provers.SMTLib",
+        "VCExpr",
+        "VCGeneration"]
+EXEs = ["Dafny", "DafnyServer"]
+ETCs = UNIX_EXECUTABLES + ["DafnyPrelude.bpl", "DafnyRuntime.cs", "DafnyLanguageService.vsix"]
+
+# Constants
+
+THIS_FILE = path.realpath(__file__)
+ROOT_DIRECTORY = path.dirname(THIS_FILE)
+SOURCE_DIRECTORY = path.join(ROOT_DIRECTORY, SOURCE_DIRECTORY)
+BINARIES_DIRECTORY = path.join(ROOT_DIRECTORY, BINARIES_DIRECTORY)
+DESTINATION_DIRECTORY = path.join(ROOT_DIRECTORY, DESTINATION_DIRECTORY)
+CACHE_DIRECTORY = path.join(DESTINATION_DIRECTORY, "cache")
+
+MONO = sys.platform not in ("win32", "cygwin")
+DLL_PDB_EXT = ".dll.mdb" if MONO else ".pdb"
+EXE_PDB_EXT = ".exe.mdb" if MONO else ".pdb"
+ARCHIVE_FNAMES = ([dll + ".dll" for dll in DLLs] + [dll + DLL_PDB_EXT for dll in DLLs] +
+                  [exe + ".exe" for exe in EXEs] + [exe + EXE_PDB_EXT for exe in EXEs] +
+                  ETCs)
+
+# Code
+
+def flush(*args, **kwargs):
+    print(*args, **kwargs)
+    sys.stdout.flush()
+
+class Release:
+    @staticmethod
+    def parse_zip_name(name):
+        m = RELEASE_REGEXP.match(name)
+        if not m:
+            raise Exception("{} does not match RELEASE_REGEXP".format(name))
+        return m.group('platform'), m.group('os'), m.group("directory")
+
+    def __init__(self, js, version):
+        self.z3_name = js["name"]
+        self.size = js["size"]
+        self.url = js["browser_download_url"]
+        self.platform, self.os, self.directory = Release.parse_zip_name(js["name"])
+        self.z3_zip = path.join(CACHE_DIRECTORY, self.z3_name)
+        self.dafny_name = "dafny-{}-{}-{}.zip".format(version, self.platform, self.os)
+        self.dafny_zip = path.join(DESTINATION_DIRECTORY, self.dafny_name)
+
+    @property
+    def cached(self):
+        return path.exists(self.z3_zip) and path.getsize(self.z3_zip) == self.size
+
+    @property
+    def MB(self):
+        return self.size / 1e6
+
+    def download(self):
+        if self.cached:
+            print("cached!")
+        else:
+            flush("downloading {:.2f}MB...".format(self.MB), end=' ')
+            with urllib.request.urlopen(self.url) as reader:
+                with open(self.z3_zip, mode="wb") as writer:
+                    writer.write(reader.read())
+            flush("done!")
+
+    @staticmethod
+    def zipify_path(fpath):
+        """Zip entries always use '/' as the path separator."""
+        return fpath.replace(os.path.sep, '/')
+
+    def pack(self):
+        try:
+            os.remove(self.dafny_zip)
+        except FileNotFoundError:
+            pass
+        missing = []
+        with zipfile.ZipFile(self.dafny_zip, 'w',  zipfile.ZIP_DEFLATED) as archive:
+            with zipfile.ZipFile(self.z3_zip) as Z3_archive:
+                z3_files_count = 0
+                for fileinfo in Z3_archive.infolist():
+                    fname = path.relpath(fileinfo.filename, self.directory)
+                    if any(fnmatch(fname, pattern) for pattern in Z3_INTERESTING_FILES):
+                        z3_files_count += 1
+                        contents = Z3_archive.read(fileinfo)
+                        fileinfo.filename = Release.zipify_path(path.join(DAFNY_PACKAGE_PREFIX, Z3_PACKAGE_PREFIX, fname))
+                        archive.writestr(fileinfo, contents)
+            for fname in ARCHIVE_FNAMES:
+                fpath = path.join(BINARIES_DIRECTORY, fname)
+                if path.exists(fpath):
+                    fileinfo = zipfile.ZipInfo(fname, time.localtime(os.stat(fpath).st_mtime)[:6])
+                    if any(fnmatch(fname, pattern) for pattern in UNIX_EXECUTABLES):
+                        # http://stackoverflow.com/questions/434641/
+                        fileinfo.external_attr = 0o777 << 16
+                    contents = open(fpath, mode='rb').read()
+                    fileinfo.compress_type = zipfile.ZIP_DEFLATED
+                    fileinfo.filename = Release.zipify_path(path.join(DAFNY_PACKAGE_PREFIX, fname))
+                    archive.writestr(fileinfo, contents)
+                else:
+                    missing.append(fname)
+        flush("done! (imported {} files from z3's sources)".format(z3_files_count))
+        if missing:
+            flush("      WARNING: Not all files were found: {} were missing".format(", ".join(missing)))
+
+def discover(version):
+    flush("  - Getting information about latest release")
+    with urllib.request.urlopen(RELEASES_URL) as reader:
+        js = json.loads(reader.read().decode("utf-8"))
+
+        for release_js in js["assets"]:
+            release = Release(release_js, version)
+            if release.platform == "x64":
+                flush("    + Selecting {} ({:.2f}MB, {})".format(release.z3_name, release.MB, release.size))
+                yield release
+            else:
+                flush("    + Rejecting {}".format(release.z3_name))
+
+def download(releases):
+    flush("  - Downloading {} z3 archives".format(len(releases)))
+    for release in releases:
+        flush("    + {}:".format(release.z3_name), end=' ')
+        release.download()
+
+def run(cmd):
+    flush("    + {}...".format(" ".join(cmd)), end=' ')
+    retv = subprocess.call(cmd, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL)
+    if retv != 0:
+        flush("failed! (Is Dafny or the Dafny server running?)")
+        sys.exit(1)
+    else:
+        flush("done!")
+
+def build():
+    os.chdir(ROOT_DIRECTORY)
+    flush("  - Building")
+    builder = "xbuild" if MONO else "msbuild"
+    try:
+        run([builder, "Source/Dafny.sln", "/p:Configuration=Checked", "/p:Platform=Any CPU", "/t:Clean"])
+        run([builder, "Source/Dafny.sln", "/p:Configuration=Checked", "/p:Platform=Any CPU", "/t:Rebuild"])
+    except FileNotFoundError:
+        flush("Could not find '{}'! On Windows, you need to run this from the VS native tools command prompt.".format(builder))
+        sys.exit(1)
+
+def pack(releases):
+    flush("  - Packaging {} Dafny archives".format(len(releases)))
+    for release in releases:
+        flush("    + {}:".format(release.dafny_name), end=' ')
+        release.pack()
+
+def parse_arguments():
+    parser = argparse.ArgumentParser(description="Prepare a Dafny release. Configuration is hardcoded; edit the `# Configuration' section of this script to change it.")
+    parser.add_argument("version", help="Version number for this release")
+    return parser.parse_args()
+
+def main():
+    args = parse_arguments()
+    os.makedirs(CACHE_DIRECTORY, exist_ok=True)
+
+    # Z3
+    flush("* Finding and downloading Z3 releases")
+    releases = list(discover(args.version))
+    download(releases)
+
+    flush("* Building and packaging Dafny")
+    build()
+    pack(releases)
+
+if __name__ == '__main__':
+    main()