Merge

4 files changed, 200 insertions, 234 deletions

diff --git a/Util/Emacs/README b/Util/Emacs/README
new file mode 100644
index 00000000..9140f20a
--- /dev/null
+++ b/Util/Emacs/README
@@ -0,0 +1,2 @@
+Emacs support for dafny is provided by the boogie-friends package, available from MELPA.
+See https://github.com/boogie-org/boogie-friends for setup instructions and tips.
\ No newline at end of file
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
deleted file mode 100644
index fd1bf369..00000000
--- a/Util/Emacs/dafny-mode.el
+++ /dev/null
@@ -1,121 +0,0 @@
-;; dafny-mode.el - GNU Emacs mode for Dafny

-;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why

-

-(defvar dafny-mode-hook nil)

-

-(defvar dafny-mode-map nil

-  "Keymap for Dafny major mode")

-

-(if dafny-mode-map nil

-  (setq dafny-mode-map (make-keymap))

-  (define-key dafny-mode-map "\C-c\C-c" 'dafny-run-verifier)

-  (define-key dafny-mode-map [(control return)] 'font-lock-fontify-buffer))

-

-(setq auto-mode-alist

-      (append

-       '(("\\.dfy" . dafny-mode))

-       auto-mode-alist))

-

-;; font-lock

-

-(defun dafny-regexp-opt (l)

-  (concat "\\_<" (concat (regexp-opt l t) "\\_>")))

-

-(defconst dafny-font-lock-keywords-1

-  (list

-   ; comments have the form /* ... */

-   '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)

-   ; or // ...

-   '("//\\([^

-]\\)*" . font-lock-comment-face)

-

-   `(,(dafny-regexp-opt '(

-        "class" "trait" "datatype" "codatatype" "newtype" "type" "iterator"

-        "function" "predicate" "copredicate" "inductive"

-        "var" "method" "constructor" "lemma" "colemma"

-        "ghost" "static" "protected" "abstract"

-	"module" "import" "default" "as" "opened"

-	"include"

-        "extends" "refines" "returns" "yields"

-	"requires" "ensures" "modifies" "reads" "free" "invariant" "decreases"

-        )) . font-lock-builtin-face)

-   `(,(dafny-regexp-opt '(

-        "assert" "assume" "break" "then" "else" "if" "label" "return" "yield"

-        "while" "print" "where"

-        "old" "forall" "exists" "new" "calc" "modify" "in" "this" "fresh"

-        "match" "case" "false" "true" "null")) . font-lock-keyword-face)

-   `(,(dafny-regexp-opt '(

-        "bool" "char" "int" "nat" "real"

-        "set" "iset" "multiset" "seq" "string" "map" "imap"

-	"object" "array" "array2" "array3")) . font-lock-type-face)

-   )

-  "Minimal highlighting for Dafny mode")

-

-(defvar dafny-font-lock-keywords dafny-font-lock-keywords-1

-  "Default highlighting for Dafny mode")

-

-;; syntax

-

-(defvar dafny-mode-syntax-table nil

-  "Syntax table for dafny-mode")

-

-(defun dafny-create-syntax-table ()

-  (if dafny-mode-syntax-table

-      ()

-    (setq dafny-mode-syntax-table (make-syntax-table))

-    (set-syntax-table dafny-mode-syntax-table)

-    (modify-syntax-entry ?' "w" dafny-mode-syntax-table)

-    (modify-syntax-entry ?_ "w" dafny-mode-syntax-table)))

-

-;; menu

-

-(require 'easymenu)

-

-(defun dafny-menu ()

-  (easy-menu-define

-   dafny-mode-menu (list dafny-mode-map)

-   "Dafny Mode Menu." 

-   '("Dafny"

-     ["Run Dafny" dafny-run-verifier t]

-     "---"

-     ["Recolor buffer" font-lock-fontify-buffer t]

-     "---"

-     ))

-  (easy-menu-add dafny-mode-menu))

-

-;; commands

-

-(defun dafny-command-line (file)

-  (concat "dafny " file))

-

-(defun dafny-run-verifier ()

-  "run Dafny verifier"

-  (interactive)

-  (let ((f (buffer-name)))

-    (compile (dafny-command-line f))))

-

-;; setting the mode

-

-(defun dafny-mode ()

-  "Major mode for editing Dafny programs.

-

-\\{dafny-mode-map}"

-  (interactive)

-  (kill-all-local-variables)

-  (dafny-create-syntax-table)

-  ; hilight

-  (make-local-variable 'font-lock-defaults)

-  (setq font-lock-defaults '(dafny-font-lock-keywords))

-  ; indentation

-  ; (make-local-variable 'indent-line-function)

-  ; (setq indent-line-function 'dafny-indent-line)

-  ; menu

-  ; providing the mode

-  (setq major-mode 'dafny-mode)

-  (setq mode-name "Dafny")

-  (use-local-map dafny-mode-map)

-  (font-lock-mode 1)

-  (dafny-menu)

-  (run-hooks 'dafny-mode-hook))

-

-(provide 'dafny-mode)

diff --git a/Util/Emacs/jennisys-mode.el b/Util/Emacs/jennisys-mode.el
deleted file mode 100644
index d8f20a31..00000000
--- a/Util/Emacs/jennisys-mode.el
+++ /dev/null
@@ -1,113 +0,0 @@
-;; jennisys-mode.el - GNU Emacs mode for Jennisys

-;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why

-

-(defvar jennisys-mode-hook nil)

-

-(defvar jennisys-mode-map nil

-  "Keymap for Jennisys major mode")

-

-(if jennisys-mode-map nil

-  (setq jennisys-mode-map (make-keymap))

-  (define-key jennisys-mode-map "\C-c\C-c" 'jennisys-run-boogie)

-  (define-key jennisys-mode-map [(control return)] 'font-lock-fontify-buffer))

-

-(setq auto-mode-alist

-      (append

-       '(("\\.jen" . jennisys-mode))

-       auto-mode-alist))

-

-;; font-lock

-

-(defun jennisys-regexp-opt (l)

-  (concat "\\<" (concat (regexp-opt l t) "\\>")))

-

-(defconst jennisys-font-lock-keywords-1

-  (list

-   ; comments have the form /* ... */

-   '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)

-   ; or // ...

-   '("//\\([^

-]\\)*" . font-lock-comment-face)

-

-   `(,(jennisys-regexp-opt '(

-        "interface" "datamodel" "code"

-        "var" "constructor" "method"

-        "frame" "invariant" "returns" "requires" "ensures"

-        )) . font-lock-builtin-face)

-   `(,(jennisys-regexp-opt '(

-        "if" "then" "else"

-        "forall" "exists"

-        "this" "in"

-        "false" "true" "null")) . font-lock-keyword-face)

-   `(,(jennisys-regexp-opt '("array" "bool" "int" "set" "seq")) . font-lock-type-face)

-   )

-  "Minimal highlighting for Jennisys mode")

-

-(defvar jennisys-font-lock-keywords jennisys-font-lock-keywords-1

-  "Default highlighting for Jennisys mode")

-

-;; syntax

-

-(defvar jennisys-mode-syntax-table nil

-  "Syntax table for jennisys-mode")

-

-(defun jennisys-create-syntax-table ()

-  (if jennisys-mode-syntax-table

-      ()

-    (setq jennisys-mode-syntax-table (make-syntax-table))

-    (set-syntax-table jennisys-mode-syntax-table)

-    (modify-syntax-entry ?' "w" jennisys-mode-syntax-table)

-    (modify-syntax-entry ?_ "w" jennisys-mode-syntax-table)))

-

-;; menu

-

-(require 'easymenu)

-

-(defun jennisys-menu ()

-  (easy-menu-define

-   jennisys-mode-menu (list jennisys-mode-map)

-   "Jennisys Mode Menu." 

-   '("Jennisys"

-     ["Run Boogie" jennisys-run-boogie t]

-     "---"

-     ["Recolor buffer" font-lock-fontify-buffer t]

-     "---"

-     ))

-  (easy-menu-add jennisys-mode-menu))

-

-;; commands

-

-(defun jennisys-command-line (file)

-  (concat "boogie " file))

-

-(defun jennisys-run-boogie ()

-  "run Boogie to check the Jennisys program"

-  (interactive)

-  (let ((f (buffer-name)))

-    (compile (jennisys-command-line f))))

-

-;; setting the mode

-

-(defun jennisys-mode ()

-  "Major mode for editing Jennisys programs.

-

-\\{jennisys-mode-map}"

-  (interactive)

-  (kill-all-local-variables)

-  (jennisys-create-syntax-table)

-  ; hilight

-  (make-local-variable 'font-lock-defaults)

-  (setq font-lock-defaults '(jennisys-font-lock-keywords))

-  ; indentation

-  ; (make-local-variable 'indent-line-function)

-  ; (setq indent-line-function 'jennisys-indent-line)

-  ; menu

-  ; providing the mode

-  (setq major-mode 'jennisys-mode)

-  (setq mode-name "Jennisys")

-  (use-local-map jennisys-mode-map)

-  (font-lock-mode 1)

-  (jennisys-menu)

-  (run-hooks 'jennisys-mode-hook))

-

-(provide 'jennisys-mode)

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()