1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
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()
|
