From 94e1770b5aa240a807955e2855253c0f3ef895a7 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 04:29:59 -0700 Subject: 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. --- package.py | 198 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 198 insertions(+) create mode 100644 package.py (limited to 'package.py') 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"^(?Pz3-[0-9\.]+-(?Px86|x64)-(?P[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() -- cgit v1.2.3 From a8f980afe85d26774806ba9c987423185f1c11ac Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 17:55:08 -0700 Subject: Make the packaging script Windows-compatible --- package.py | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'package.py') diff --git a/package.py b/package.py index 22ed232c..7fc624cf 100644 --- a/package.py +++ b/package.py @@ -101,7 +101,10 @@ class Release: flush("done!") def unpack(self): - shutil.rmtree(self.z3_directory) + try: + shutil.rmtree(self.z3_directory) + except FileNotFoundError: + pass with zipfile.ZipFile(self.z3_zip) as archive: archive.extractall(CACHE_DIRECTORY) flush("done!") @@ -165,9 +168,13 @@ def run(cmd): 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"]) + 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))) -- cgit v1.2.3 From 8b49355bcbe76170504b8f23b4f54a7793b1ae5c Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 18:41:12 -0700 Subject: More fixes to the packaging script --- package.py | 40 ++++++++++++++++++++++++++-------------- 1 file changed, 26 insertions(+), 14 deletions(-) (limited to 'package.py') diff --git a/package.py b/package.py index 7fc624cf..94c7f70e 100644 --- a/package.py +++ b/package.py @@ -1,25 +1,36 @@ +from fnmatch import fnmatch +from os import path import argparse import json import os -from os import path import re -import urllib.request +import shutil +import subprocess import sys +import urllib.request import zipfile -import subprocess -import shutil # Configuration +## Where do we fetch the list of releases from? RELEASES_URL = "https://api.github.com/repos/Z3Prover/z3/releases/latest" -RELEASE_REGEXP = r"^(?Pz3-[0-9\.]+-(?Px86|x64)-(?P[a-z0-9\.\-]+)).zip$" +## How do we extract info from the name of a release file? +RELEASE_REGEXP = re.compile(r"^(?Pz3-[0-9\.]+-(?Px86|x64)-(?P[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" -Z3_ARCHIVE_PREFIX = path.join("z3", "bin") +## 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/*"] +## What do we take from Dafny's Binaries folder? DLLs = ["AbsInt", "Basetypes", "CodeContractsExtender", @@ -48,8 +59,6 @@ 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" @@ -78,7 +87,6 @@ class Release: 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) @@ -116,24 +124,28 @@ class Release: pass missing = [] with zipfile.ZipFile(self.dafny_zip, 'w', zipfile.ZIP_DEFLATED) as archive: - for root, _, files in os.walk(self.z3_bin_directory): + z3_files_count = 0 + for root, _, files in os.walk(self.z3_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) + relpath = path.relpath(fpath, self.z3_directory) + if any(fnmatch(relpath, pattern) for pattern in Z3_INTERESTING_FILES): + arcpath = path.join(Z3_PACKAGE_PREFIX, relpath) + archive.write(fpath, arcpath) + z3_files_count += 1 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!") + 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("https://api.github.com/repos/Z3Prover/z3/releases/latest") as reader: + with urllib.request.urlopen(RELEASES_URL) as reader: js = json.loads(reader.read().decode("utf-8")) for release_js in js["assets"]: -- cgit v1.2.3 From 4c71672823dfac1cd352f0da6a61b83680d7eb31 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 19:38:12 -0700 Subject: package.py: Keep z3's exec bits, and set the exec bit on the dafny/ script --- package.py | 42 ++++++++++++++++-------------------------- 1 file changed, 16 insertions(+), 26 deletions(-) (limited to 'package.py') diff --git a/package.py b/package.py index 94c7f70e..62f8dbdf 100644 --- a/package.py +++ b/package.py @@ -30,6 +30,9 @@ Z3_PACKAGE_PREFIX = path.join("z3") ## What do we take from the z3 archive? (Glob syntax) Z3_INTERESTING_FILES = ["LICENSE.txt", "bin/*"] +## On unix system, which Dafny files should be marked as executable? (Glob syntax; Z3's permissions are preserved) +UNIX_EXECUTABLES = ["dafny"] + ## What do we take from Dafny's Binaries folder? DLLs = ["AbsInt", "Basetypes", @@ -86,7 +89,6 @@ class Release: 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.dafny_name = "dafny-{}-{}-{}.zip".format(version, self.platform, self.os) self.dafny_zip = path.join(DESTINATION_DIRECTORY, self.dafny_name) @@ -108,15 +110,6 @@ class Release: writer.write(reader.read()) flush("done!") - def unpack(self): - try: - shutil.rmtree(self.z3_directory) - except FileNotFoundError: - pass - with zipfile.ZipFile(self.z3_zip) as archive: - archive.extractall(CACHE_DIRECTORY) - flush("done!") - def pack(self): try: os.remove(self.dafny_zip) @@ -124,18 +117,22 @@ class Release: pass missing = [] with zipfile.ZipFile(self.dafny_zip, 'w', zipfile.ZIP_DEFLATED) as archive: - z3_files_count = 0 - for root, _, files in os.walk(self.z3_directory): - for f in files: - fpath = path.join(root, f) - relpath = path.relpath(fpath, self.z3_directory) - if any(fnmatch(relpath, pattern) for pattern in Z3_INTERESTING_FILES): - arcpath = path.join(Z3_PACKAGE_PREFIX, relpath) - archive.write(fpath, arcpath) + 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 = path.join(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) + if any(fnmatch(fname, pattern) for pattern in UNIX_EXECUTABLES): + # http://stackoverflow.com/questions/434641/ + fileinfo.external_attr = 0o777 << 16 archive.write(fpath, fname) else: missing.append(fname) @@ -162,12 +159,6 @@ def download(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) @@ -204,10 +195,9 @@ def main(): os.makedirs(CACHE_DIRECTORY, exist_ok=True) # Z3 - flush("* Finding, downloading, and unpacking Z3 releases") + flush("* Finding and downloading Z3 releases") releases = list(discover(args.version)) download(releases) - unpack(releases) flush("* Building and packaging Dafny") build() -- cgit v1.2.3 From 354c53de79366c09f8550b8cd23ebddb0b7d2c2f Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 20:25:37 -0700 Subject: Add a tip to the packaging script --- package.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'package.py') diff --git a/package.py b/package.py index 62f8dbdf..fa111ec5 100644 --- a/package.py +++ b/package.py @@ -163,7 +163,7 @@ def run(cmd): flush(" + {}...".format(" ".join(cmd)), end=' ') retv = subprocess.call(cmd, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL) if retv != 0: - flush("failed!") + flush("failed! (Is Dafny or the Dafny server running?)") sys.exit(1) else: flush("done!") -- cgit v1.2.3 From 3b1c3923a403efbd28b8f5ae6fc4429ccee8c2e8 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 28 Aug 2015 20:08:14 -0700 Subject: Put contents od release packages into a dafny/ directory --- package.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'package.py') diff --git a/package.py b/package.py index fa111ec5..33e83d73 100644 --- a/package.py +++ b/package.py @@ -24,6 +24,8 @@ 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") @@ -124,7 +126,7 @@ class Release: if any(fnmatch(fname, pattern) for pattern in Z3_INTERESTING_FILES): z3_files_count += 1 contents = Z3_archive.read(fileinfo) - fileinfo.filename = path.join(Z3_PACKAGE_PREFIX, fname) + fileinfo.filename = path.join(DAFNY_PACKAGE_PREFIX, Z3_PACKAGE_PREFIX, fname) archive.writestr(fileinfo, contents) for fname in ARCHIVE_FNAMES: fpath = path.join(BINARIES_DIRECTORY, fname) @@ -133,7 +135,7 @@ class Release: if any(fnmatch(fname, pattern) for pattern in UNIX_EXECUTABLES): # http://stackoverflow.com/questions/434641/ fileinfo.external_attr = 0o777 << 16 - archive.write(fpath, fname) + archive.write(fpath, path.join(DAFNY_PACKAGE_PREFIX, fname)) else: missing.append(fname) flush("done! (imported {} files from z3's sources)".format(z3_files_count)) -- cgit v1.2.3 From d4095cfc0d255422ff732b9ab1666a830776cdf8 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 8 Oct 2015 00:56:33 -0400 Subject: Add vsix to releases and fix invalid path separators in packaging script --- package.py | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) mode change 100644 => 100755 package.py (limited to 'package.py') diff --git a/package.py b/package.py old mode 100644 new mode 100755 index 33e83d73..32192822 --- a/package.py +++ b/package.py @@ -1,12 +1,14 @@ +#!/usr/bin/env python3 + from fnmatch import fnmatch from os import path import argparse import json import os import re -import shutil import subprocess import sys +import time import urllib.request import zipfile @@ -53,7 +55,7 @@ DLLs = ["AbsInt", "VCExpr", "VCGeneration"] EXEs = ["Dafny", "DafnyServer"] -ETCs = ["dafny", "DafnyPrelude.bpl", "DafnyRuntime.cs"] +ETCs = ["dafny", "DafnyPrelude.bpl", "DafnyRuntime.cs", "DafnyLanguageService.vsix"] # Constants @@ -112,6 +114,11 @@ class Release: 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) @@ -126,16 +133,19 @@ class Release: if any(fnmatch(fname, pattern) for pattern in Z3_INTERESTING_FILES): z3_files_count += 1 contents = Z3_archive.read(fileinfo) - fileinfo.filename = path.join(DAFNY_PACKAGE_PREFIX, Z3_PACKAGE_PREFIX, fname) + 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) + 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 - archive.write(fpath, path.join(DAFNY_PACKAGE_PREFIX, fname)) + 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)) -- cgit v1.2.3 From 87047cd015c07f5d98def6681a0187639ccc62b5 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 30 Mar 2016 11:38:13 +0200 Subject: Add a wrapper for DafnyServer.exe --- Binaries/dafny-server | 16 ++++++++++++++++ package.py | 6 +++--- 2 files changed, 19 insertions(+), 3 deletions(-) create mode 100755 Binaries/dafny-server (limited to 'package.py') diff --git a/Binaries/dafny-server b/Binaries/dafny-server new file mode 100755 index 00000000..2fd0d202 --- /dev/null +++ b/Binaries/dafny-server @@ -0,0 +1,16 @@ +#!/usr/bin/env bash + +MONO=$(which mono) +DAFNYSERVER=$(dirname "${BASH_SOURCE[0]}")/DafnyServer.exe + +if [[ ! -x "$MONO" ]]; then + echo "Error: Dafny requires Mono to run on non-Windows systems." + exit 1 +fi + +if [[ ! -x "$DAFNYSERVER" ]]; then + echo "Error: DafnyServer.exe not found at $DAFNYSERVER." + exit 1 +fi + +"$MONO" "$DAFNYSERVER" "$@" diff --git a/package.py b/package.py index 32192822..721bb0eb 100755 --- a/package.py +++ b/package.py @@ -34,8 +34,8 @@ Z3_PACKAGE_PREFIX = path.join("z3") ## What do we take from the z3 archive? (Glob syntax) Z3_INTERESTING_FILES = ["LICENSE.txt", "bin/*"] -## On unix system, which Dafny files should be marked as executable? (Glob syntax; Z3's permissions are preserved) -UNIX_EXECUTABLES = ["dafny"] +## 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", @@ -55,7 +55,7 @@ DLLs = ["AbsInt", "VCExpr", "VCGeneration"] EXEs = ["Dafny", "DafnyServer"] -ETCs = ["dafny", "DafnyPrelude.bpl", "DafnyRuntime.cs", "DafnyLanguageService.vsix"] +ETCs = UNIX_EXECUTABLES + ["DafnyPrelude.bpl", "DafnyRuntime.cs", "DafnyLanguageService.vsix"] # Constants -- cgit v1.2.3