Write a new packaging script for Dafny

This is intended to superseed the PrepareDafnyZip.bat script. I tried doing this
as an msbuild config, then as a makefile, but the first one was too cumbersome
and the second one required too many dependencies to work properly (and parsing
JSON from a makefile is not fun).

The new script calls the Github API to retrieve the description of the latest z3
release, downloads the zip corresponding to each supported platfom, and
packages one copy of Dafny for each copy of z3 that the latest release
contains.

The next step will be to make Dafny load its binary from the z3 folder.

1 files changed, 198 insertions, 0 deletions

diff --git a/package.py b/package.py
new file mode 100644
index 00000000..22ed232c
--- /dev/null
+++ b/package.py
@@ -0,0 +1,198 @@
+import argparse
+import json
+import os
+from os import path
+import re
+import urllib.request
+import sys
+import zipfile
+import subprocess
+import shutil
+
+# Configuration
+
+RELEASES_URL = "https://api.github.com/repos/Z3Prover/z3/releases/latest"
+RELEASE_REGEXP = r"^(?P<directory>z3-[0-9\.]+-(?P<platform>x86|x64)-(?P<os>[a-z0-9\.\-]+)).zip$"
+
+SOURCE_DIRECTORY = "Source"
+BINARIES_DIRECTORY = "Binaries"
+DESTINATION_DIRECTORY = "Package"
+
+Z3_ARCHIVE_PREFIX = path.join("z3", "bin")
+
+DLLs = ["AbsInt",
+        "Basetypes",
+        "CodeContractsExtender",
+        "Concurrency",
+        "Core",
+        "DafnyPipeline",
+        "Doomed",
+        "ExecutionEngine",
+        "Graph",
+        "Houdini",
+        "Model",
+        "ModelViewer",
+        "ParserHelper",
+        "Provers.SMTLib",
+        "VCExpr",
+        "VCGeneration"]
+EXEs = ["Dafny", "DafnyServer"]
+ETCs = ["dafny", "DafnyPrelude.bpl", "DafnyRuntime.cs"]
+
+# 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")
+
+RELEASE_REGEXP = re.compile(RELEASE_REGEXP, re.IGNORECASE)
+
+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.z3_directory = path.join(CACHE_DIRECTORY, self.directory)
+        self.z3_bin_directory = path.join(self.z3_directory, "bin")
+        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!")
+
+    def unpack(self):
+        shutil.rmtree(self.z3_directory)
+        with zipfile.ZipFile(self.z3_zip) as archive:
+            archive.extractall(CACHE_DIRECTORY)
+            flush("done!")
+
+    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:
+            for root, _, files in os.walk(self.z3_bin_directory):
+                for f in files:
+                    fpath = path.join(root, f)
+                    arcpath = path.join(Z3_ARCHIVE_PREFIX, path.relpath(fpath, self.z3_bin_directory))
+                    archive.write(fpath, arcpath)
+            for fname in ARCHIVE_FNAMES:
+                fpath = path.join(BINARIES_DIRECTORY, fname)
+                if path.exists(fpath):
+                    archive.write(fpath, fname)
+                else:
+                    missing.append(fname)
+        flush("done!")
+        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("https://api.github.com/repos/Z3Prover/z3/releases/latest") 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 unpack(releases):
+    flush("  - Unpacking {} z3 archives".format(len(releases)))
+    for release in releases:
+        flush("    + {}:".format(release.z3_name), end=' ')
+        release.unpack()
+
+def run(cmd):
+    flush("    + {}...".format(" ".join(cmd)), end=' ')
+    retv = subprocess.call(cmd, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL)
+    if retv != 0:
+        flush("failed!")
+        sys.exit(1)
+    else:
+        flush("done!")
+
+def build():
+    os.chdir(ROOT_DIRECTORY)
+    flush("  - Building")
+    builder = "xbuild" if MONO else "xbuild"
+    run([builder, "Source/Dafny.sln", "/t:Clean"])
+    run([builder, "Source/Dafny.sln", "/p:Configuration=Checked", "/t:Rebuild"])
+
+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, downloading, and unpacking Z3 releases")
+    releases = list(discover(args.version))
+    download(releases)
+    unpack(releases)
+
+    flush("* Building and packaging Dafny")
+    build()
+    pack(releases)
+
+if __name__ == '__main__':
+    main()