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
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
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()
|
