Updated version to 0.6

dominique-unruh · Nov 11, 2020 · bba6a50 · bba6a50
1 parent 3178c75
commit bba6a50
Show file tree

Hide file tree

Showing 4 changed files with 32 additions and 35 deletions.
diff --git a/.circleci/config.yml b/.circleci/config.yml
@@ -7,7 +7,7 @@ orbs:
 
 workflows:
   version: 2
-  linux:
+  macos:
     jobs:
       - test:
           filters:
@@ -19,7 +19,7 @@ workflows:
 jobs:
   test:
 
-    machine: {image: ubuntu-2004:202010-01}
+    macos: {xcode: 11.6.0}
 
     steps:
       - checkout
@@ -31,26 +31,26 @@ jobs:
       # Download and cache Isabelle
       - restore_cache:
           keys:
-            - v2-isabelle-2019-linux
+            - v2-isabelle-2019-macos
       - run:
           name: Downloading Isabelle 2019 (if needed)
           shell: bash
           command: |
             if ! [ -e "$HOME/install/Isabelle2019" ]; then
               mkdir -p ~/install
-              case linux in
+              case macos in
                 windows)
                   curl "https://isabelle.in.tum.de/website-Isabelle2019/dist/Isabelle2019.exe" -o /tmp/isabelle.exe
                   7z x -y -o"$HOME/install" /tmp/isabelle.exe;;
                 linux|macos)
-                  curl https://isabelle.in.tum.de/website-Isabelle2019/dist/Isabelle2019_linux.tar.gz | tar -x -z -C ~/install;;
+                  curl https://isabelle.in.tum.de/website-Isabelle2019/dist/Isabelle2019_macos.tar.gz | tar -x -z -C ~/install;;
                 *) false;;
               esac
             fi
       - save_cache:
           paths:
-            - ~/install/Isabelle2019
-          key: v2-isabelle-2019-linux
+            - ~/install/Isabelle2019.app/Isabelle
+          key: v2-isabelle-2019-macos
 
       # Download and cache AFP
       - restore_cache:
@@ -83,48 +83,48 @@ jobs:
             echo v3 > ~/isabelle-thys-checksums # Adding a tag to be able to enforce rebuilding
       - restore_cache:
           keys:
-            - v4-isabelle-heaps-2019-linux-QRHL-{{ checksum "~/isabelle-thys-checksums" }}
-            - v4-isabelle-heaps-2019-linux-QRHL-
-            - v3-isabelle-heaps-2019-linux-QRHL-
+            - v4-isabelle-heaps-2019-macos-QRHL-{{ checksum "~/isabelle-thys-checksums" }}
+            - v4-isabelle-heaps-2019-macos-QRHL-
+            - v3-isabelle-heaps-2019-macos-QRHL-
       - run:
           name: Building QRHL theories
           shell: bash
           command: |
             set -e
-            if ! sha1sum -c ~/qrhl-sha1sum; then
-              case linux in
+            if ! shasum -c ~/qrhl-sha1sum; then
+              case macos in
                 windows)
                   # TODO: Under windows, need a different invocation, check whether this works
-                  ~/install/Isabelle2019/contrib/cygwin/bin/bash ~/install/Isabelle2019/bin/isabelle build -o threads=4 -v -b -d ~/install/afp-2019/thys -d . QRHL;;
+                  ~/install/Isabelle2019.app/Isabelle/contrib/cygwin/bin/bash ~/install/Isabelle2019.app/Isabelle/bin/isabelle build -o threads=4 -v -b -d ~/install/afp-2019/thys -d . QRHL;;
                 *)
-                  ~/install/Isabelle2019/bin/isabelle build -o threads=8 -v -b -d ~/install/afp-2019/thys -d . QRHL;;
+                  ~/install/Isabelle2019.app/Isabelle/bin/isabelle build -o threads=8 -v -b -d ~/install/afp-2019/thys -d . QRHL;;
               esac
             fi
-            sha1sum ~/isabelle-thys-checksums > ~/qrhl-sha1sum
+            shasum ~/isabelle-thys-checksums > ~/qrhl-sha1sum
             cat ~/qrhl-sha1sum
       - save_cache:
           paths:
             - ~/.isabelle
             - ~/qrhl-sha1sum
-          key: v4-isabelle-heaps-2019-linux-QRHL-{{ checksum "~/isabelle-thys-checksums" }}
+          key: v4-isabelle-heaps-2019-macos-QRHL-{{ checksum "~/isabelle-thys-checksums" }}
 
       # Download and cache dependencies
       - restore_cache:
           keys:
-            - v1-dependencies-linux-{{ checksum "build.sbt" }}
-            - v1-dependencies-linux-
+            - v1-dependencies-macos-{{ checksum "build.sbt" }}
+            - v1-dependencies-macos-
       - run:
           name: Downloading build dependencies (if needed)
 
           shell: bash
           command: |
-            if ! sha1sum -c ~/dependencies-sha1sum; then
+            if ! shasum -c ~/dependencies-sha1sum; then
               mkdir -p ~/install
               curl -Ls https://git.io/sbt > ~/install/sbt
               chmod +x ~/install/sbt
               ~/install/sbt update test/update </dev/null
             fi
-            sha1sum build.sbt > ~/dependencies-sha1sum
+            shasum build.sbt > ~/dependencies-sha1sum
       - save_cache:
           paths:
             - ~/install/sbt
@@ -134,19 +134,19 @@ jobs:
             - $LOCALAPPDATA\Coursier\Cache
             - ~/.cache/coursier
             - ~/dependencies-sha1sum
-          key: v1-dependencies-linux-{{ checksum "build.sbt" }}
+          key: v1-dependencies-macos-{{ checksum "build.sbt" }}
 
       - run:
           name: Running tests
           shell: bash
           command: |
-            case linux in
+            case macos in
               windows)
                 # Isabelle process calls rebaseall and then fails, unless we deactivate it
-                > ~/install/Isabelle2019/contrib/cygwin/isabelle/rebaseall
-                ISABELLE_HOME="`cygpath -w ~/install/Isabelle2019`";;
+                > ~/install/Isabelle2019.app/Isabelle/contrib/cygwin/isabelle/rebaseall
+                ISABELLE_HOME="`cygpath -w ~/install/Isabelle2019.app/Isabelle`";;
               linux|macos)
-                ISABELLE_HOME=~/install/Isabelle2019;;
+                ISABELLE_HOME=~/install/Isabelle2019.app/Isabelle;;
             esac
 
             echo "isabelle-home = $ISABELLE_HOME" > qrhl-tool.conf

diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-VERSION="0.6alpha"
+VERSION="0.6"
 SOURCES := $(shell find src) $(wildcard *.qrhl) $(wildcard *.thy) doc/manual.pdf
 
 qrhl.zip : target/universal/qrhl-$(VERSION).zip

diff --git a/README.md b/README.md
@@ -1,9 +1,6 @@
 [![Build Status](https://travis-ci.com/dominique-unruh/qrhl-tool.svg?branch=master)](https://travis-ci.com/dominique-unruh/qrhl-tool)
 [![Gitter chat](https://img.shields.io/badge/gitter-chat-brightgreen.svg)](https://gitter.im/dominique-unruh/qrhl-tool?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)
 
-**This describes the installation process for the development snapshot. See [here](https://github.com/dominique-unruh/qrhl-tool/blob/31b2ef3c9b91e74e0e1bc56b476e211e03590672/README.md) for instructions
-for [v0.5](https://github.com/dominique-unruh/qrhl-tool/releases/tag/v0.5).**
-
 # Binary installation
 
 The binaries require Linux, OS/X, or Windows to run.
@@ -27,18 +24,18 @@ and enter `java -version` or `emacs -version`, respectively, and see whether the
 
 ## Installation
 
-Simply unpack `qrhl.zip`. This will create a directory called `qrhl-0.6alpha`.
+Simply unpack `qrhl.zip`. This will create a directory called `qrhl-0.6`.
 
-In the `qrhl-0.6alpha` directory, edit the file `qrhl-tool.conf`: 
+In the `qrhl-0.6` directory, edit the file `qrhl-tool.conf`: 
 Add the configuration keys `isabelle-home = <where you unpackaged Isabelle2019>`
 and `afp-home = <where you unpackaged AFP>`.
 
 To update, simply extract the new version.
-(But make sure to save your `qrhl-tool.conf`.)
+(But make sure to backup your `qrhl-tool.conf` as it will be overwritten.)
 
 ## Executing the demos
 
-In the `qrhl-0.6alpha` directory, execute `proofgeneral.{sh,bat}`.
+In the `qrhl-0.6` directory, execute `proofgeneral.{sh,bat}`.
 
 This will open emacs running ProofGeneral configured for the qrhl
 tool.  Open one of the example files in `examples/`,
@@ -65,7 +62,7 @@ Then open and edit the file normally.
 
 * Make sure that [sbt](https://www.scala-sbt.org/) (Scala Build Tool) is on the path.
 * Use `git clone https://github.com/dominique-unruh/qrhl-tool.git` to download the sources.
-* Use `git checkout master` (replace `master` by the version/git revision you wish to compile, e.g., `v0.5`). 
+* Use `git checkout master` (replace `master` by the version/git revision you wish to compile, e.g., `v0.6`). 
 * Create a `qrhl-tool.conf` file as described in the binary installation section above.
 * Run `./proofgeneral.sh` or `./run-isabelle.sh` as described above (this will (re)compile the sources if needed).
 * Run `bin/qrhl` to run the tool on the command line.

diff --git a/build.sbt b/build.sbt
@@ -10,7 +10,7 @@ lazy val root = (project in file("."))
 
 name := "qrhl"
 
-version := "0.6alpha"
+version := "0.6"
 
 scalaVersion := "2.13.3"