diff options
| -rw-r--r-- | package.py | 198 |
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() |