Merge tag 'v1.7.1'

.github/FUNDING.yml

+custom: ['https://www.microsoft.com/en-us/research/']

.github/workflows/main.yml

@@ -16,14 +16,14 @@ jobs:
         include: 
         - operating-system: macos-latest
           MVN_COMMAND: mvn -Dmaven.test.skip=true
-          GITHUB_RELEASE_NAME: The Aristotle release
-          TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip
+          GITHUB_RELEASE_NAME: The Clarke release
+          TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.8.0-macosx.cocoa.x86_64.zip
 
         - operating-system: ubuntu-latest
           MVN_COMMAND: xvfb-run mvn -Dtest.skip=true -Dmaven.test.failure.ignore=true 
-          GITHUB_RELEASE_NAME: The Aristotle release
-          TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.7.0-linux.gtk.x86_64.zip
-          TOOLBOX_PRODUCT_ZIP_WIN: TLAToolbox-1.7.0-win32.win32.x86_64.zip
+          GITHUB_RELEASE_NAME: The Clarke release
+          TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.8.0-linux.gtk.x86_64.zip
+          TOOLBOX_PRODUCT_ZIP_WIN: TLAToolbox-1.8.0-win32.win32.x86_64.zip
 
     steps:
 
@@ -93,7 +93,7 @@ jobs:
       ## Build TLC and Toolbox (logger reduces verbosity).
       ##
     - name: Build with Maven (Linux)
-      run: ${{ matrix.MVN_COMMAND }} -Pcodesigning -Dorg.slf4j.simpleLogger.log.org.apache.maven.cli.transfer.Slf4jMavenTransferListener=warn -fae -B verify --file pom.xml
+      run: ${{ matrix.MVN_COMMAND }} -Pcodesigning -Dtycho.disableP2Mirrors=true -Dorg.slf4j.simpleLogger.log.org.apache.maven.cli.transfer.Slf4jMavenTransferListener=warn -fae -B verify --file pom.xml
 
       ##
       ## Create signed apt repository out of Linux Toolbox zip.
@@ -139,9 +139,9 @@ jobs:
            curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=${{matrix.TOOLBOX_PRODUCT_ZIP}} --upload-file toolbox/org.lamport.tla.toolbox.product.product/target/products/${{matrix.TOOLBOX_PRODUCT_ZIP}}
 
-           ID=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json"  | jq '.[]| select(.name == "TLAToolbox-1.7.0.deb") | .id')
+           ID=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json"  | jq '.[]| select(.name == "TLAToolbox-1.8.0.deb") | .id')
            curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
-           curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0.deb --upload-file toolbox/org.lamport.tla.toolbox.product.product/target/TLAToolbox-1.7.0-linux.gtk.amd64.deb
+           curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.8.0.deb --upload-file toolbox/org.lamport.tla.toolbox.product.product/target/TLAToolbox-1.8.0-linux.gtk.amd64.deb
 
            ID=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json"  | jq '.[]| select(.name == "p2repository.zip") | .id')
            curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
@@ -150,23 +150,26 @@ jobs:
            ## Generate changelog
            cd general/docs/changelogs
            ## Append sha1 sum to changelog (last line of changelog has the table header).
-           echo "$(sha1sum ../../../tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar"  >> ch1_7_0.md
-           echo "$(sha1sum ../../../toolbox/org.lamport.tla.toolbox.product.product/target/products/${{matrix.TOOLBOX_PRODUCT_ZIP_WIN}} | cut -f 1 -d " ")|${{matrix.TOOLBOX_PRODUCT_ZIP_WIN}}" >> ch1_7_0.md
-           echo "$(sha1sum ../../../toolbox/org.lamport.tla.toolbox.product.product/target/products/${{matrix.TOOLBOX_PRODUCT_ZIP}} | cut -f 1 -d " ")|${{matrix.TOOLBOX_PRODUCT_ZIP}}" >> ch1_7_0.md
-           echo "TBD|macOS" >> ch1_7_0.md
+           echo "$(sha1sum ../../../tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar"  >> ch1_8_0.md
+           echo "$(sha1sum ../../../toolbox/org.lamport.tla.toolbox.product.product/target/products/${{matrix.TOOLBOX_PRODUCT_ZIP_WIN}} | cut -f 1 -d " ")|${{matrix.TOOLBOX_PRODUCT_ZIP_WIN}}" >> ch1_8_0.md
+           echo "$(sha1sum ../../../toolbox/org.lamport.tla.toolbox.product.product/target/products/${{matrix.TOOLBOX_PRODUCT_ZIP}} | cut -f 1 -d " ")|${{matrix.TOOLBOX_PRODUCT_ZIP}}" >> ch1_8_0.md
+           echo "TBD|macOS" >> ch1_8_0.md
            ## Two above as one-liner without intermediate file.
-           $(jq -n --argjson changelog "$(cat ch1_7_0.md | jq  --raw-input --slurp .)" -f gh-1_7_0.jq > gh-1_7_0.json)
+           $(jq -n --argjson changelog "$(cat ch1_8_0.md | jq  --raw-input --slurp .)" -f gh-1_8_0.jq > gh-1_8_0.json)
            ## Update draft release with latest changelog in case it changed.
            ## https://developer.github.com/v3/repos/releases/#edit-a-release
-           curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE -d @gh-1_7_0.json -X PATCH --header "Content-Type: application/json"
+           curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE -d @gh-1_8_0.json -X PATCH --header "Content-Type: application/json"
 
     - name: Upload assets to INRIA
       if: matrix.operating-system == 'ubuntu-latest'
       run: |
+           ## Thanks Apple for your walled garden! Delete the *unsigned* Toolbox maxOS zip created by the Linux/ubuntu job.  The macOS job below creates and rsyncs a *signed* zip file.
+           rm toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.8.0-macosx.cocoa.x86_64.zip
            ## Upload p2 and apt repository to INRIA machine.
-           rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" -av tlatools/org.lamport.tlatools/dist/tla2tools.jar github@upload.tlapl.us:dist/
-           rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" -av toolbox/org.lamport.tla.toolbox.product.product/target/products/*.zip github@upload.tlapl.us:products/
-           rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" -av toolbox/org.lamport.tla.toolbox.product.product/target/repository/ github@upload.tlapl.us:repository/
+           rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av tlatools/org.lamport.tlatools/dist/tla2tools.jar github@upload.tlapl.us:dist/
+           rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av toolbox/org.lamport.tla.toolbox.product.product/target/products/*.zip github@upload.tlapl.us:products/
+           rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av toolbox/org.lamport.tla.toolbox.product.product/target/repository/ github@upload.tlapl.us:repository/
+           rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av toolbox/org.lamport.tla.toolbox.doc/html/ github@upload.tlapl.us:doc/
 
     ## 
     ## Update all git tags to make the download urls work, i.e.
@@ -179,8 +182,7 @@ jobs:
       run: |
         git config --local user.email "tlaplus-action@github.com"
         git config --local user.name "TLA+ GitHub Action"
-        git tag -f nightly
-        git tag -f v1.7.0
+        git tag -f v1.8.0
         git push https://${{ github.actor }}:${{ secrets.GITHUB_TOKEN }}@github.com/${{ github.repository }}.git --follow-tags --tags --force
 
       ##
@@ -195,6 +197,17 @@ jobs:
            ## github.xml replaces the Tycho pom.xml with a specific one to publish tla2tools.jar.
            mvn deploy:deploy-file -Dgithub.packages.username=${{ github.actor }} -Dgithub.packages.password=${{ secrets.GITHUB_TOKEN }} -Dfile=dist/tla2tools.jar -Durl=https://maven.pkg.github.com/${{ github.repository }} -DpomFile=github.xml -DrepositoryId=github -f github.xml
 
+      ##
+      ## Trigger build of CommunityModule as integration tests.
+      ##
+    - name: Integration tests with CommunityModules
+      if: matrix.operating-system == 'ubuntu-latest'
+      uses: peter-evans/repository-dispatch@v1
+      with:
+          token: ${{ secrets.COMMUNITYMODULES_ACCESS_TOKEN }}
+          repository: tlaplus/CommunityModules
+          event-type: tlaplus-dispatch
+
       ################################# macOS #################################
 
       ##
@@ -235,10 +248,13 @@ jobs:
            security set-key-partition-list -S apple-tool:,apple: -s -k ${{ secrets.APPLE_CERT_PASSWORD }} tla
            ## Unzip, sign, and zip up the TLA Toolbox.
            unzip toolbox/org.lamport.tla.toolbox.product.product/target/products/${{ matrix.TOOLBOX_PRODUCT_ZIP }}
-           codesign --keychain tla --deep --display --entitlements toolbox/org.lamport.tla.toolbox.product.product/entitlements.plist --options runtime --verbose=4 -h -f -s "Developer ID Application: M K (3PCM4M3RWK)" "TLA+ Toolbox.app"
+           codesign --force --identifier org.lamport.tla.toolbox.product.product --keychain tla --deep --display --entitlements toolbox/org.lamport.tla.toolbox.product.product/entitlements.plist --options runtime --verbose=4 -h -f -s "Developer ID Application: M K (3PCM4M3RWK)" "TLA+ Toolbox.app"
            ditto -ck --sequesterRsrc --keepParent "TLA+ Toolbox.app" ${{ matrix.TOOLBOX_PRODUCT_ZIP }}
+           xcrun altool --notarize-app --primary-bundle-id "org.lamport.tla.toolbox.product.product" --username "${{secrets.APPLE_CODESIGN_DEVELOPER_ID}}" --password "${{secrets.APPLE_CODESIGN_DEVELOPER_PASSWORD}}" --file "${{ matrix.TOOLBOX_PRODUCT_ZIP }}"
            ## Upload signed TLAToolbox zip to Github release.
            DRAFT_RELEASE=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases --header "Content-Type: application/json" | jq '.[]| select(.name=="${{ matrix.GITHUB_RELEASE_NAME }}") | .id')
            ID=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json"  | jq '.[]| select(.name == "${{ matrix.TOOLBOX_PRODUCT_ZIP }}") | .id')
            curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=${{ matrix.TOOLBOX_PRODUCT_ZIP }} --upload-file ${{ matrix.TOOLBOX_PRODUCT_ZIP }}
+           ## Upload p2 and apt repository to INRIA machine.
+           rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av ${{ matrix.TOOLBOX_PRODUCT_ZIP }} github@upload.tlapl.us:products/

.jenkins.groovy

@@ -46,7 +46,7 @@ for (x in labels) {
 		      }
 	   	      // the macosx zip on the master node to have it signed with the Apple certificate on macosx.  However, only master
 		      // has the lamport certificate to sign the individual toolbox bundles.
-		      stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip', name: 'toolbox'
+		      stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip', name: 'toolbox'
                     } else {
 			  withMaven(
 			    // Maven installation declared in the Jenkins "Global Tool Configuration"
@@ -153,7 +153,7 @@ node ('master') {
    }
    
    stage('RenderChangelog') { // Render the github flavord markdown to html
-       sh 'grip --context=tlaplus/tlaplus --export ${WORKSPACE}/general/docs/changelogs/ch1_7_0.md ${WORKSPACE}/general/docs/changelogs/changelog.html'
+       sh 'grip --context=tlaplus/tlaplus --export ${WORKSPACE}/general/docs/changelogs/ch1_7_1.md ${WORKSPACE}/general/docs/changelogs/changelog.html'
    }
 }
 
@@ -162,11 +162,11 @@ node ('macos') {
         sh 'rm -rf *'
         unstash 'toolbox'
         sh 'ls -lah'
-        sh 'unzip toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip'
+        sh 'unzip toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip'
         sh 'codesign -f -s "Developer ID Application: M K (3PCM4M3RWK)" -v "TLA+ Toolbox.app" --deep'
-        sh 'ditto -ck --sequesterRsrc --keepParent "TLA+ Toolbox.app" TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip'
-        sh 'mv TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip toolbox/org.lamport.tla.toolbox.product.product/target/products/'
-        stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip', name: 'signed'
+        sh 'ditto -ck --sequesterRsrc --keepParent "TLA+ Toolbox.app" TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip'
+        sh 'mv TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip toolbox/org.lamport.tla.toolbox.product.product/target/products/'
+        stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip', name: 'signed'
     }
 }
 
@@ -188,21 +188,21 @@ node ('master') {
            cd ${WORKSPACE}/general/docs/changelogs
 
            ## Append sha1 sum to changelog (last line of changelog has the table header).
-           echo "$(sha1sum ${WORKSPACE}/tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar"  >> ch1_7_0.md
-           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-win32.win32.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.0-win32.win32.x86_64.zip" >> ch1_7_0.md
-           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip" >> ch1_7_0.md     
-           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-linux.gtk.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.0-linux.gtk.x86_64.zip" >> ch1_7_0.md
+           echo "$(sha1sum ${WORKSPACE}/tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar"  >> ch1_7_1.md
+           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-win32.win32.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.1-win32.win32.x86_64.zip" >> ch1_7_1.md
+           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip" >> ch1_7_1.md     
+           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-linux.gtk.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.1-linux.gtk.x86_64.zip" >> ch1_7_1.md
            
            ## Two above as one-liner without intermediate file.
-           $(jq -n --argjson changelog "$(cat ch1_7_0.md | jq  --raw-input --slurp .)" -f gh-1_7_0.jq > gh-1_7_0.json)
+           $(jq -n --argjson changelog "$(cat ch1_7_1.md | jq  --raw-input --slurp .)" -f gh-1_7_1.jq > gh-1_7_1.json)
 
            ## Get id of existing draft release with given name.
-           DRAFT_RELEASE=$(curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases --header "Content-Type: application/json" | jq '.[]| select(.draft==true and .name=="The Aristotle release") | .id')
+           DRAFT_RELEASE=$(curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases --header "Content-Type: application/json" | jq '.[]| select(.draft==true and .name=="The Brontinus release") | .id')
            echo $DRAFT_RELEASE
 
            ## Update draft release with latest changelog in case it changed.
            ## https://developer.github.com/v3/repos/releases/#edit-a-release
-           curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE -d @gh-1_7_0.json -X PATCH --header "Content-Type: application/json"
+           curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE -d @gh-1_7_1.json -X PATCH --header "Content-Type: application/json"
 
            ## Remove old assets otherwise upload below will error.
            ASSETS=$(curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json" | jq '.[]| .id')
@@ -216,15 +216,15 @@ node ('master') {
             ## tla2tools.jar
             curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=tla2tools.jar --upload-file ${WORKSPACE}/tlatools/org.lamport.tlatools/dist/tla2tools.jar
             ## macOS
-            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip
+            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip
             ## win32
-            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-win32.win32.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-win32.win32.x86_64.zip
+            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-win32.win32.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-win32.win32.x86_64.zip
             ## Linux
-            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-linux.gtk.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-linux.gtk.x86_64.zip
+            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-linux.gtk.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-linux.gtk.x86_64.zip
             ## deb
-            #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-linux.gtk.amd64.deb --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/repository/TLAToolbox-1.7.0-linux.gtk.amd64.deb
+            #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-linux.gtk.amd64.deb --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/repository/TLAToolbox-1.7.1-linux.gtk.amd64.deb
             ## RPM
-            #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-linux.gtk.amd64.rpm --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLA\\+Toolbox-1.7.0~*.x86_64.rpm
+            #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-linux.gtk.amd64.rpm --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLA\\+Toolbox-1.7.1~*.x86_64.rpm
          '''
         }
    }

.travis.yml

  sudo: required
  dist: trusty
  language: java
- jdk: openjdk11
+ jdk: openjdk14
  install: true
 
  env:

CONTRIBUTING.md

@@ -31,7 +31,7 @@ The Toolbox's nightly builds are also made available as a [cask](https://github.
 
 ```bash
 $ brew tap homebrew/cask-versions
-$ brew install tlaplus-toolbox-nightly
+$ brew install tla-plus-toolbox-nightly
 ```
 
 Quality Metrics

general/docs/changelogs/ch1_7_1.md

+### <a href="#latest-tla-files">Click here to jump to the downloads at the bottom of this page!</a>
+
+### Changelog
+The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The [1.7.1 milestone](https://github.com/tlaplus/tlaplus/issues?q=is%3Aissue+milestone%3A1.7.1+is%3Aclosed) lists all completed issues.
+
+### Additional _noteworthy_ changes
+
+#### Tools
+
+##### Feature
+* Improve some of TLC's error messages. e328ae9842620ac028c0ebd2f83033dcb5dbe506
+* Add `TLC!TLCGet("generated")` that equals the number of states generated. fa766305094b698eab3338ed917bd1c8b4542039
+* Prototype: Support multiple TLA+ modules in a single .tla file. 505e073ffe9b9eee8ebe4b375b2dad5f402fa36b
+* Programatically stop simulation with `TLC!TLCSet("exit", TRUE)`. d62b289af42edb2026cda423cc56bb0fe8477b52
+* Prototype: Add an interactive TLA+ REPL. 97afa3c6952e343ee2409366a668ba12afceeef4 ([Screencast](https://asciinema.org/a/3lsDwbmVG0iyZHJ3RbhNycQS0))
+* Drop intermittent stuttering steps from error trace in simulation mode. cfcfafbd964bfef46064fdfeb10c4fd2e4c1839e
+* Return non-zero error codes from SANY on more errors. 10f77cf67f666cda315eaa7337c6cc256d97c8b6
+* [ALIAS](https://github.com/tlaplus/tlaplus/issues/485). f5306c601a2133ebffad6224db93c16663fe5ff5
+* [POSTCONDITION](https://lamport.azurewebsites.net/tla/current-tools.pdf). ced9269895aa6b760fa7d7a35fa61b43eb2a9a0a e9be5d0fa41ba38879b2e92307853a3ad9855542 be394f889f8e22c74e491638c54997d00ee03c88
+* Prototype: Visualize *action* coverage in simulation mode. 3d3259da2d48db44275074cbf6874d477752c59d 3913dd181a5cac755acb1577a6503b6f5d443137
+* Report number of and mean/variance/standard deviation of length of generated traces in simulation mode. d175e317c102b1825e3f9b436e34ed477e5309c9 7a3bcb0302edfc5b2f720002a8561bc5a8552c47
+* Let users set the maximum number of traces to generate in simulation mode. a969d55dbda8cf5750300d82bbdbc37f6df4712f
+
+##### Bugfix
+* TLC shows no error *trace* for violations of `TLC!Assert`, ... (regression in 1.7.0). 19757bdd6aadf7c0e371c40bf591f0d84f12a592
+* State graph visualization in dot format broken for specs with instantiation. a8fc5b1bf6dfb29679848fdd6f15f3c3ada9efa2
+* Simulation mode ignores ASSUMPTIONS. https://github.com/tlaplus/tlaplus/issues/496
+* `TLC!RandomElement` breaks error trace re-construction in simulation mode. e0d64f686dae1aec22728b1acfa40b1a554a7267
+* NoClassDefError when running TLC on Java 1.8. e6bd13ec971c1fa2a165b7068bc0091ab6c510cb
+* Replace custom implementation of (heap) sort in TeX with java.utils.Arrays#sort https://github.com/tlaplus/tlaplus/issues/539 8b52d238eb9f17df98dd795dbb589d9fba4a5822
+
+#### Toolbox
+
+##### Feature
+* Open a Toolbox spec, module, or TLC model in the file manager such as Windows Explorer, Finder, or Nautilus.
+* Proof-of-concept: Remove GraphViz dependency by rendering state graph visualization with embedded browser (macOS & Linux only). 478d8569e84dfb31b982a500947def5c9c813b97
+* Bundle [CommunityModules](https://github.com/tlaplus/CommunityModules) as part of the Toolbox. 3beb7116b97def46fc57fa777c8bb533803ee025
+* Upgrade Eclipse foundation to its 2020-06 release for better HiDPI support. dc67692e17cb75866e7005358255d9849870fc4a
+* Set [`ALIAS`](https://github.com/tlaplus/tlaplus/issues/485) and `POSTCONDITION` in Toolbox's model editor. e8054e8eb913bc87c336882c7c6e1f8565ada1e9 d3cfde5a37d943b95a354d40ad60b8bef07411b2
+* Re-worked PlusCal/TLA+ divergence warning (please manually remove [1.7.0 markers](https://github.com/tlaplus/tlaplus/releases/tag/v1.7.0)). f1cf514c3b334b0968a5ac7fdf14d3e93905b14c e434e139adebf73ed8f9470117031f1ad4b749df 7c61d1a70f03fe4e54142f59487af90745386b74
+
+##### Bugfix
+* Quickly open spec or model in OS file manager. 06280a4f346279a69bb458636d290a027041f006
+* Do not enter `Spec` as next-state relation when restarting model-checking from a state in the error-trace. 7f50021048155a3d085d5d482eede37f09fbf9e5
+* Multiline trace expressions fail to parse in Toolbox. defe0c74915b1c27c6af2fb55c8163f3574c8918
+
+### Contributors
+
+We are grateful for contributions to this release from: [William Schultz](https://github.com/will62794), [Paulo Rafael Feodrippe](https://github.com/pfeodrippe), and [zmatti](https://github.com/zmatti).
+
+<a id="latest-tla-files"/>
+
+### Checksums
+sha1sum|file
+------------ | -------------

general/docs/changelogs/ch1_8_0.md

+### <a href="#latest-tla-files">Click here to jump to the downloads at the bottom of this page!</a>
+
+### Changelog
+The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The [1.8.0 milestone](https://github.com/tlaplus/tlaplus/issues?q=is%3Aissue+milestone%3A1.7.1+is%3Aclosed) lists all completed issues.
+
+### Additional _noteworthy_ changes
+
+#### Tools
+
+##### Feature
+* Improve some of TLC's error messages. e328ae9842620ac028c0ebd2f83033dcb5dbe506
+* Add `TLC!TLCGet("generated")` that equals the number of states generated. fa766305094b698eab3338ed917bd1c8b4542039
+* Prototype: Support multiple TLA+ modules in a single .tla file. 505e073ffe9b9eee8ebe4b375b2dad5f402fa36b
+* Programatically stop simulation with `TLC!TLCSet("exit", TRUE)`. d62b289af42edb2026cda423cc56bb0fe8477b52
+* Prototype: Add an interactive TLA+ REPL. 97afa3c6952e343ee2409366a668ba12afceeef4 ([Screencast](https://asciinema.org/a/3lsDwbmVG0iyZHJ3RbhNycQS0))
+* Drop intermittent stuttering steps from error trace in simulation mode. cfcfafbd964bfef46064fdfeb10c4fd2e4c1839e
+* Return non-zero error codes from SANY on more errors. 10f77cf67f666cda315eaa7337c6cc256d97c8b6
+* [ALIAS](https://github.com/tlaplus/tlaplus/issues/485). f5306c601a2133ebffad6224db93c16663fe5ff5
+* [POSTCONDITION](https://lamport.azurewebsites.net/tla/current-tools.pdf). ced9269895aa6b760fa7d7a35fa61b43eb2a9a0a e9be5d0fa41ba38879b2e92307853a3ad9855542 be394f889f8e22c74e491638c54997d00ee03c88
+* Prototype: Visualize *action* coverage in simulation mode. 3d3259da2d48db44275074cbf6874d477752c59d 3913dd181a5cac755acb1577a6503b6f5d443137
+* Report number of and mean/variance/standard deviation of length of generated traces in simulation mode. d175e317c102b1825e3f9b436e34ed477e5309c9 7a3bcb0302edfc5b2f720002a8561bc5a8552c47
+* Let users set the maximum number of traces to generate in simulation mode. a969d55dbda8cf5750300d82bbdbc37f6df4712f
+
+##### Bugfix
+* TLC shows no error *trace* for violations of `TLC!Assert`, ... (regression in 1.7.0). 19757bdd6aadf7c0e371c40bf591f0d84f12a592
+* State graph visualization in dot format broken for specs with instantiation. a8fc5b1bf6dfb29679848fdd6f15f3c3ada9efa2
+* Simulation mode ignores ASSUMPTIONS. https://github.com/tlaplus/tlaplus/issues/496
+* `TLC!RandomElement` breaks error trace re-construction in simulation mode. e0d64f686dae1aec22728b1acfa40b1a554a7267
+* NoClassDefError when running TLC on Java 1.8. e6bd13ec971c1fa2a165b7068bc0091ab6c510cb
+* Replace custom implementation of (heap) sort in TeX with java.utils.Arrays#sort https://github.com/tlaplus/tlaplus/issues/539 8b52d238eb9f17df98dd795dbb589d9fba4a5822
+
+#### Toolbox
+
+##### Feature
+* Open a Toolbox spec, module, or TLC model in the file manager such as Windows Explorer, Finder, or Nautilus.
+* Proof-of-concept: Remove GraphViz dependency by rendering state graph visualization with embedded browser (macOS & Linux only). 478d8569e84dfb31b982a500947def5c9c813b97
+* Bundle [CommunityModules](https://github.com/tlaplus/CommunityModules) as part of the Toolbox. 3beb7116b97def46fc57fa777c8bb533803ee025
+* Upgrade Eclipse foundation to its 2020-06 release for better HiDPI support. dc67692e17cb75866e7005358255d9849870fc4a
+* Set [`ALIAS`](https://github.com/tlaplus/tlaplus/issues/485) and `POSTCONDITION` in Toolbox's model editor. e8054e8eb913bc87c336882c7c6e1f8565ada1e9 d3cfde5a37d943b95a354d40ad60b8bef07411b2
+* Re-worked PlusCal/TLA+ divergence warning (please manually remove [1.7.0 markers](https://github.com/tlaplus/tlaplus/releases/tag/v1.7.0)). f1cf514c3b334b0968a5ac7fdf14d3e93905b14c e434e139adebf73ed8f9470117031f1ad4b749df 7c61d1a70f03fe4e54142f59487af90745386b74
+
+##### Bugfix
+* Quickly open spec or model in OS file manager. 06280a4f346279a69bb458636d290a027041f006
+* Do not enter `Spec` as next-state relation when restarting model-checking from a state in the error-trace. 7f50021048155a3d085d5d482eede37f09fbf9e5
+* Multiline trace expressions fail to parse in Toolbox. defe0c74915b1c27c6af2fb55c8163f3574c8918
+
+### Contributors
+
+We are grateful for contributions to this release from: [William Schultz](https://github.com/will62794), [Paulo Rafael Feodrippe](https://github.com/pfeodrippe), and [zmatti](https://github.com/zmatti).
+
+<a id="latest-tla-files"/>
+
+### Checksums
+sha1sum|file
+------------ | -------------

general/docs/changelogs/gh-1_7_1.jq

+{
+  "tag_name": "v1.7.1",
+  "name": "The Brontinus release",
+  "draft": false,
+  "prerelease": true,
+  "body": $changelog
+}
\ No newline at end of file

general/docs/changelogs/gh-1_8_0.jq

+{
+  "tag_name": "v1.8.0",
+  "name": "The Clarke release",
+  "draft": false,
+  "prerelease": true,
+  "body": $changelog
+}
\ No newline at end of file

general/docs/contributions.md

@@ -39,6 +39,9 @@ Reasoning about TLA+ sequences currently mainly relies on the lemmas provided in
 
 Most conjectures that users attempt to prove during proof development are in fact not valid. For example, hypotheses needed to prove a step are not provided to the prover, the invariant may not be strong enough etc. When this is the case, the back-end provers time out but do not provide any useful information to the user. The objective of this work is to connect a model generator such as [Nunchaku](https://github.com/nunchaku-inria/nunchaku) to TLAPS that could provide an explanation to the user why the proof obligation is not valid. The main difficulty will be defining a translation from a useful sublanguage of TLA+ set-theoretic expressions to the input language of Nunchaku, which resembles a functional programming language.
 
+#### Warning about unexpanded definitions (difficulty: moderate) (skills: OCaml, TLA+)
+
+A common reason for a proof not to succeed is the failure to tell the prover to expand a definition that needs to be expanded (see section 6.1 of [Proving Safety Properties](https://lamport.azurewebsites.net/tla/proving-safety.pdf) for an example).  In some cases, simple heuristics could indicate that a definition needs to be expanded--for example, if a goal contains a symbol that does not appear in any formula being used to prove it.  The objective is to find and implement such heuristics in a command that the user can invoke to suggest what definitions may need to be expanded.  We believe that this would be an easy way to save users a lot of--especially beginning users.
 
 TLA Toolbox
 -----------

general/ide/README.md

@@ -2,13 +2,13 @@ Eclipse Oomph is a tool to simplify and automate the setup of Eclipse developmen
 
 [A screencast is available that captures the written instructions below.](https://vimeo.com/190224035)
 
-0. Requires a recent - at the time of writing this is 13 - JDK (Java Development Environment) - AdoptOpenJDK is recommended.
+0. Requires a recent - at the time of writing this is 14 - JDK (Java Development Environment) - AdoptOpenJDK is recommended.
 1. Install the Oomph Eclipse installer from [https://wiki.eclipse.org/Eclipse_Installer](https://wiki.eclipse.org/Eclipse_Installer)
 2. Start the downloaded Oomph installer
 3. Switch to "Advanced Mode" by clicking the button in the right upper corner depicted with three horizontal lines
 4. Select "Eclipse Platform" on the Product list (expand "Eclipse.org" node)
-  1. Choose "2019-09" from the Product Version combobox at the bottom ![Choose Platform](https://raw.githubusercontent.com/lemmy/tlaplus/master/general/ide/images/00_PlatformSelection.png)
-     1. You can try to use a more recent version of Eclipse, however if you run into troubles during the installation and set-up, choose "2019-09" instead.
+  1. Choose "2020-03" from the Product Version combobox at the bottom ![Choose Platform](https://raw.githubusercontent.com/lemmy/tlaplus/master/general/ide/images/00_PlatformSelection.png)
+     1. You can try to use a more recent version of Eclipse, however if you run into troubles during the installation and set-up, choose "2020-03" instead.
 5. On the next screen, expand "Github Project" in the tree and select the check-box left to "TLA+" 
   1. Verify that "TLA+" shows up under "Project" at the bottom table and that the "Master" stream is selected ![Chose Project](https://raw.githubusercontent.com/lemmy/tlaplus/master/general/ide/images/01_ProjectSelection.png)
 6. On the next page, select whether to use anonymous Github access (read-only) from the "TLA+ Github Repository" dropdown list ![Chose anonymous access](https://raw.githubusercontent.com/lemmy/tlaplus/master/general/ide/images/02_Variables.png)

general/ide/TLA.setup

@@ -63,8 +63,6 @@
         name="org.eclipse.swtbot.feature.group"/>
     <requirement
         name="org.eclipse.ajdt.feature.group"/>
-    <requirement
-        name="org.eclipse.m2e.feature.feature.group"/>
     <requirement
         name="org.eclipse.pde.feature.group"/>
     <requirement
@@ -80,15 +78,15 @@
     <repository
         url="http://download.eclipse.org/technology/swtbot/releases/latest/"/>
     <repository
-        url="http://download.eclipse.org/tools/ajdt/48/dev/update/"/>
+        url="http://download.eclipse.org/tools/ajdt/410/dev/update/"/>
     <repository
         url="http://download.eclipse.org/technology/m2e/releases/"/>
     <repository
         url="http://download.eclipse.org/e4/snapshots/org.eclipse.e4.tools/latest/"/>
     <repository
-        url="jar:https://dl.bintray.com/abstratt-oss/abstratt-oss/com/abstratt/eclipsegraphviz/com.abstratt.eclipsegraphviz.repository/2.5.201812/com.abstratt.eclipsegraphviz.repository-2.5.201812.zip!/"/>
+        url="jar:https://raw.githubusercontent.com/tlaplus/tlaplus/master/toolbox/org.lamport.tla.toolbox.product.product/cachedTargetPlatform/com.abstratt.eclipsegraphviz.repository-2.5.201812.zip!/"/>
     <repository
-        url="https://download.eclipse.org/rcptt/release/2.4.3/repository/"/>
+        url="https://download.eclipse.org/rcptt/release/2.5.1/repository/"/>
     <repository
         url="http://andrei.gmxhome.de/eclipse/"/>
     <description>Install the tools needed in the IDE to work with the source code for ${scope.project.label}</description>

pom.xml

@@ -78,7 +78,7 @@
 		<module>toolbox/org.lamport.tla.toolbox.product.product</module>
 
 		<!-- Finally run UI tests on fully built product (AUT) -->
-		<module>toolbox/org.lamport.tla.toolbox.product.uitest</module>
+<!--		<module>toolbox/org.lamport.tla.toolbox.product.uitest</module>-->
 	</modules>
 
 	<!-- tycho requires maven >= 3.0 -->
@@ -92,7 +92,7 @@
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
 
 		<!-- https://wiki.eclipse.org/Tycho/Release_Notes/1.4 -->
-		<tycho-version>1.5.0</tycho-version>
+		<tycho-version>1.5.1</tycho-version>
 
 		<!-- no default here -->
 		<tycho.test.vm.argline>-Xmx500m -Xdebug -Xrunjdwp:transport=dt_socket,address=1044,server=y,suspend=n</tycho.test.vm.argline>
@@ -123,7 +123,7 @@
 		<!-- Align toolbox.version with the version in
 			 org.lamport.tla.toolbox.product.product.product
 			 product.version. -->
-		<toolbox.version>1.7.0</toolbox.version>
+		<toolbox.version>1.8.0</toolbox.version>
 
 		<!-- This is used in org.lamport.tla.toolbox.product.uitest but
 			has been placed at the top level should it need be referenced
@@ -264,6 +264,13 @@
 				<artifactId>target-platform-configuration</artifactId>
 				<version>${tycho-version}</version>
 				<configuration>
+				    <!-- Some dependencies such as jline referenced by org.lamport.tlatools   -->
+				    <!-- cannot be found in the Toolbox's target platform (TLAToolbox.target) -->
+				    <!-- because the dependencies are not made available in p2 repositories.  -->
+				    <!-- However, sometimes OSGi-fied dependencies are made available on      -->
+				    <!-- Maven Central.  'pomDependencies' makes this build look there too.    -->
+				    <!-- https://wiki.eclipse.org/Tycho/Target_Platform#.22POM_dependencies_consider.22 -->
+                    <pomDependencies>consider</pomDependencies>
 					<!-- recommended: use p2-based target platform resolver -->
 					<resolver>p2</resolver>
 					<ignoreTychoRepositories>true</ignoreTychoRepositories>

tlatools/org.lamport.tlatools/.classpath

@@ -17,6 +17,8 @@
 	<classpathentry kind="src" path="test-verify"/>
 	<classpathentry kind="src" path="test-benchmark"/>
 	<classpathentry kind="lib" path="lib/javax.mail/mailapi-1.6.3.jar"/>
+	<classpathentry kind="lib" path="lib/jline/jline-reader-3.14.1.jar"/>
+	<classpathentry kind="lib" path="lib/jline/jline-terminal-3.14.1.jar"/>
 	<classpathentry kind="lib" path="lib/jpf.jar"/>
 	<classpathentry kind="lib" path="lib/jmh/jmh-core-1.21.jar"/>
 	<classpathentry kind="lib" path="lib/jmh/commons-math3-3.2.jar"/>

tlatools/org.lamport.tlatools/META-INF/MANIFEST.MF

@@ -32,7 +32,6 @@ Export-Package: pcal,
  tlc2.tool.impl,
  tlc2.tool.liveness,
  tlc2.tool.management,
- tlc2.tool.other,
  tlc2.tool.queue,
  tlc2.util,
  tlc2.value,
@@ -44,6 +43,8 @@ Eclipse-BundleShape: dir
 Require-Bundle: org.aspectj.runtime;bundle-version="1.6.0";resolution:=optional;x-installation:=greedy,
  org.junit;bundle-version="4.12.0";resolution:=optional;x-installation:=greedy,
  javax.mail;bundle-version="1.4.0";resolution:=optional,
- org.easymock;bundle-version="2.4.0";resolution:=optional
+ org.easymock;bundle-version="2.4.0";resolution:=optional,
+ org.jline.reader;bundle-version="3.14.1";resolution:=optional,
+ org.jline.terminal;bundle-version="3.14.1";resolution:=optional
 Bundle-ClassPath: .
 Automatic-Module-Name: org.lamport.tlatools

tlatools/org.lamport.tlatools/customBuild.xml

@@ -137,6 +137,8 @@
 			<classpath refid="project.classpath" />
 			<classpath>
 				<pathelement location="lib/javax.mail/mailapi-1.6.3.jar" />
+				<pathelement location="lib/jline/jline-terminal-3.14.1.jar" />
+				<pathelement location="lib/jline/jline-reader-3.14.1.jar" />
 			</classpath>
 		</javac>
 
@@ -250,6 +252,29 @@
 		</unzip>
 		<touch file="target/classes/META-INF/javamail.default.address.map"/>
 
+		<unzip src="lib/jline/jline-terminal-3.14.1.jar" dest="${class.dir}">
+			<patternset>
+				<include name="**/*.*"/>
+			</patternset>
+		</unzip>
+
+		<unzip src="lib/jline/jline-reader-3.14.1.jar" dest="${class.dir}">
+			<patternset>
+				<include name="**/*.*"/>
+			</patternset>
+		</unzip>
+
+		<!-- Include a few LICENSE files -->
+		<copy todir="${class.dir}">
+			<fileset dir="lib/jline">
+				<include name="jline-LICENSE.txt" />
+			</fileset>
+			<fileset dir="src/org/apache/commons/math3/">
+				<include name="CommonsMath-NOTICE.txt" />
+				<include name="CommonsMath-LICENSE.txt" />
+			</fileset>
+		</copy>
+
 
 		<!-- create a JAR file for the users -->
 		<mkdir dir="${dist.dir}" />
@@ -275,6 +300,12 @@
 					src/tla2sany/parser/Token.09-09-07,
 					src/tla2sany/parser/TokenMgrError.09-09-07"/>
 			<fileset dir="${doc.dir}" includes="License.txt"/>
+			<fileset dir="${test.class.dir}">
+				<include name="**/tlc2/tool/CommonTestCase*.class" />
+				<include name="**/tlc2/tool/liveness/ModelCheckerTestCase*.class" />
+				<include name="**/tlc2/TestMPRecorder*.class" />
+				<include name="**/util/IsolatedTestCaseRunner*.class" />
+			</fileset>
 			<manifest>
 				<attribute name="Built-By" value="${user.name}" />
 				<attribute name="Build-Tag" value="${env.BUILD_TAG}" />
@@ -285,7 +316,7 @@
 				<!-- The jar files contains many main classes (SANY, TEX, pcal, ...) --> 
                 <!-- but lets consider TLC the one users primarily use. --> 
 				<attribute name="Main-class" value="tlc2.TLC" />
-				<attribute name="Class-Path" value="CommunityModules.jar" />
+				<attribute name="Class-Path" value="CommunityModules-deps.jar CommunityModules.jar" />
 				<!-- Git revision -->
 				<attribute name="X-Git-Branch" value="${git.branch}" />
 				<attribute name="X-Git-Tag" value="${git.tag}" />
@@ -304,7 +335,7 @@
 	</target>
 
 	<!-- Compiles the TLA+ tools *test* code -->
-	<target name="compile-test" unless="test.skip">
+	<target name="compile-test">
 		<!-- compile unit tests -->
 		<mkdir dir="${test.class.dir}" />
 		<javac includeantruntime="false" srcdir="${test.dir}" destdir="${test.class.dir}" debug="true" verbose="false" source="1.8" target="1.8">
@@ -355,6 +386,8 @@
 				<pathelement location="lib/objenesis-2.1.jar" />
 				<pathelement location="lib/easymock-3.3.1.jar" />
 				<pathelement location="lib/javax.mail/mailapi-1.6.3.jar" />
+				<pathelement location="lib/jline/jline-terminal-3.14.1.jar" />
+				<pathelement location="lib/jline/jline-reader-3.14.1.jar" />
 				<pathelement location="test-model/UserModuleOverrideFromJar.jar" />
 				<pathelement path="${class.dir}" />
 				<pathelement path="${test.class.dir}" />
@@ -388,6 +421,8 @@
 					<exclude name="**/CommonTestCase.java" />
 					<exclude name="**/ModelCheckerTestCase.java" />
 					<exclude name="**/PCalModelCheckerTestCase.java" />
+					<exclude name="**/TraceExpressionSpecTest.java" />
+					<exclude name="**/TraceExpressionSpecSafetyTest.java" />
 					<exclude name="**/SuiteTestCase.java" />
 					<exclude name="**/SuiteETestCase.java" />
 					<exclude name="**/DistributedTLCTestCase.java" />
@@ -479,6 +514,8 @@
 				<pathelement location="lib/objenesis-2.1.jar" />
 				<pathelement location="lib/easymock-3.3.1.jar" />
 				<pathelement location="lib/javax.mail/mailapi-1.6.3.jar" />
+				<pathelement location="lib/jline/jline-terminal-3.14.1.jar" />
+				<pathelement location="lib/jline/jline-reader-3.14.1.jar" />
 				<pathelement location="test-model/UserModuleOverrideFromJar.jar" />
 				<pathelement path="${class.dir}" />
 				<pathelement path="${test.class.dir}" />
@@ -549,6 +586,8 @@
 						<exclude name="**/CommonTestCase.java" />
 						<exclude name="**/ModelCheckerTestCase.java" />
 						<exclude name="**/PCalModelCheckerTestCase.java" />
+						<exclude name="**/TraceExpressionSpecTest.java" />
+						<exclude name="**/TraceExpressionSpecSafetyTest.java" />
 						<exclude name="**/SuiteTestCase.java" />
 						<exclude name="**/SuiteETestCase.java" />
 						<exclude name="**/DistributedTLCTestCase.java" />
@@ -576,6 +615,10 @@
 						<exclude name="**/DetlefsTest.java" />
 						<exclude name="**/StarkMutexTest.java" />
 						<exclude name="**/SimpleMultiProcTest.java" />
+						<!-- The test checks if Tool/FastTool methods are correctly inlined during (long) 
+						     model-checking. It fails with this target but passes with test.  I assume
+						     this is because test-dist records coverage, which, perhaps, interferes with inlining. -->
+						<exclude name="**/InliningTest.java" />
 					</fileset>
 				</batchtest>
 				<batchtest fork="yes" todir="${test.reports}">

tlatools/org.lamport.tlatools/lib/jline/jline-LICENSE.txt

+Copyright (c) 2002-2018, the original author or authors.
+All rights reserved.
+
+https://opensource.org/licenses/BSD-3-Clause
+
+Redistribution and use in source and binary forms, with or
+without modification, are permitted provided that the following
+conditions are met:
+
+Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer
+in the documentation and/or other materials provided with
+the distribution.
+
+Neither the name of JLine nor the names of its contributors
+may be used to endorse or promote products derived from this
+software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING,
+BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY
+AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO
+EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY,
+OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED
+AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING
+IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED
+OF THE POSSIBILITY OF SUCH DAMAGE.
+

tlatools/org.lamport.tlatools/ossrh.xml

@@ -17,7 +17,7 @@
 	<groupId>org.lamport</groupId>
 	<artifactId>tla2tools</artifactId>
 	<name>TLA+ Tools</name>
-	<version>1.7.0-SNAPSHOT</version>
+	<version>1.7.1-SNAPSHOT</version>
 	<description>The TLC model checker, the syntax and semantic checker SANY, the PlusCal translator, and the LaTeX pretty printer.</description>
 	<packaging>jar</packaging>