Merge commit 'b7af7718' (before move)

.github/CODE_OF_CONDUCT.md

+# Contributor Covenant Code of Conduct
+
+## Our Pledge
+
+In the interest of fostering an open and welcoming environment, we as
+contributors and maintainers pledge to make participation in our project and
+our community a harassment-free experience for everyone, regardless of age, body
+size, disability, ethnicity, sex characteristics, gender identity and expression,
+level of experience, education, socio-economic status, nationality, personal
+appearance, race, religion, or sexual identity and orientation.
+
+## Our Standards
+
+Examples of behavior that contributes to creating a positive environment
+include:
+
+* Using welcoming and inclusive language
+* Being respectful of differing viewpoints and experiences
+* Gracefully accepting constructive criticism
+* Focusing on what is best for the community
+* Showing empathy towards other community members
+
+Examples of unacceptable behavior by participants include:
+
+* The use of sexualized language or imagery and unwelcome sexual attention or
+  advances
+* Trolling, insulting/derogatory comments, and personal or political attacks
+* Public or private harassment
+* Publishing others' private information, such as a physical or electronic
+  address, without explicit permission
+* Other conduct which could reasonably be considered inappropriate in a
+  professional setting
+
+## Our Responsibilities
+
+Project maintainers are responsible for clarifying the standards of acceptable
+behavior and are expected to take appropriate and fair corrective action in
+response to any instances of unacceptable behavior.
+
+Project maintainers have the right and responsibility to remove, edit, or
+reject comments, commits, code, wiki edits, issues, and other contributions
+that are not aligned to this Code of Conduct, or to ban temporarily or
+permanently any contributor for other behaviors that they deem inappropriate,
+threatening, offensive, or harmful.
+
+## Scope
+
+This Code of Conduct applies within all project spaces, and it also applies when
+an individual is representing the project or its community in public spaces.
+Examples of representing a project or community include using an official
+project e-mail address, posting via an official social media account, or acting
+as an appointed representative at an online or offline event. Representation of
+a project may be further defined and clarified by project maintainers.
+
+## Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behavior may be
+reported by contacting the project team. All
+complaints will be reviewed and investigated and will result in a response that
+is deemed necessary and appropriate to the circumstances. The project team is
+obligated to maintain confidentiality with regard to the reporter of an incident.
+Further details of specific enforcement policies may be posted separately.
+
+Project maintainers who do not follow or enforce the Code of Conduct in good
+faith may face temporary or permanent repercussions as determined by other
+members of the project's leadership.
+
+## Attribution
+
+This Code of Conduct is adapted from the [Contributor Covenant][homepage], version 1.4,
+available at https://www.contributor-covenant.org/version/1/4/code-of-conduct.html
+
+[homepage]: https://www.contributor-covenant.org
+
+For answers to common questions about this code of conduct, see
+https://www.contributor-covenant.org/faq
+

.github/workflows/main.yml

+name: CI
+
+on: [push]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v2
+      with:
+        # Number of commits to fetch. 0 indicates all history.
+        # jgit task nested in customBuild.xml fails without history.
+        fetch-depth: '0'
+
+    - name: Set up JDK 11
+      uses: actions/setup-java@v1
+      with:
+        java-version: 11.0.3
+
+    - uses: actions/cache@v1
+      with:
+        path: ~/.m2/repository
+        key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }}
+        restore-keys: |
+            ${{ runner.os }}-maven-
+    - name: Build with Maven
+      run: mvn -Dmaven.test.skip=true -Dorg.slf4j.simpleLogger.log.org.apache.maven.cli.transfer.Slf4jMavenTransferListener=warn -fae -B verify --file pom.xml
\ No newline at end of file

.gitignore

@@ -33,3 +33,5 @@ tlatools/test-model/CodePlexBug08/checkpoint/
 tlatools/test-model/CallGotoUnlabeledTest.old
 junit[0-9]*.properties
 junitvmwatcher[0-9]*.properties
+test.jfr
+*.jfr

.jenkins.groovy

+//def labels = ['windows', 'master', 'macos'] // labels for Jenkins node types we will build on
+def labels = ['master', 'macos']
+def builders = [:]
+for (x in labels) {
+    def label = x // Need to bind the label variable before the closure - can't do 'for (label in labels)'
+
+    // Create a map to pass in to the 'parallel' step so we can fire all the builds at once
+    builders[label] = {
+      node(label) {
+	   stage('Preparation') { // for display purposes
+	      // Get some code from a GitHub repository
+	      git url: 'https://github.com/tlaplus/tlaplus.git'
+	   }
+	   stage('Tools') {
+		withAnt(installation: 'apache ant', jdk: 'Java11') {
+			if (isUnix()) {
+			    sh "ant -f tlatools/customBuild.xml info compile compile-test dist test-dist"
+			} else {
+			    bat "ant -f tlatools\\customBuild.xml info compile compile-test dist test-dist"
+			}
+		}
+	   }
+
+	   stage ('RecordTestAndCoverageTools') {
+	       junit 'tlatools/target/surefire-reports/onJar/*.xml'
+	      // collect jacoco results for TLC
+	      jacoco classPattern: 'tlatools/class', exclusionPattern: '**/*Test*.class', execPattern: 'tlatools/target/code-coverage.exec', sourcePattern: 'tlatools/src'
+	   }
+
+	   stage('Toolbox') {
+	      // Run the maven build
+		   if (label == 'master') {
+		      wrap([$class: 'Xvnc', takeScreenshot: false, useXauthority: true]) {
+			  withMaven(
+			    // Maven installation declared in the Jenkins "Global Tool Configuration"
+			    maven: '3.5.4',
+			    jdk: 'Java11',
+			    mavenLocalRepo: '.repository',
+			    options: [jacocoPublisher(disabled: true)]) {
+
+			    // Run the maven build
+			    sh "mvn -Pcodesigning -U clean verify -Dmaven.test.failure.ignore=true -Dtest.skip=true"
+
+			  } // withMaven will discover the generated Maven artifacts, JUnit Surefire & FailSafe & FindBugs reports...
+		      }
+	   	      // 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: 'org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.6.1-macosx.cocoa.x86_64.zip', name: 'toolbox'
+                    } else {
+			  withMaven(
+			    // Maven installation declared in the Jenkins "Global Tool Configuration"
+			    maven: '3.5.4',
+			    jdk: 'Java11',
+			    mavenLocalRepo: '.repository',
+			    options: [jacocoPublisher(disabled: true)]) {
+
+			    // Run the maven build
+			    if (isUnix()) {
+				    sh "mvn -U clean verify -Dmaven.test.failure.ignore=true -Dtest.skip=true"
+			    } else {
+				    bat "mvn -U clean verify -Dmaven.test.failure.ignore=true -Dtest.skip=true"
+			    }
+
+			  } // withMaven will discover the generated Maven artifacts, JUnit Surefire & FailSafe & FindBugs reports...
+                    }
+	   }
+
+	   stage ('RecordTestToolbox') {
+	       junit '**/target/surefire-reports/*.xml'
+	   }
+      }
+    }
+}
+parallel builders
+
+// Rest runs on master node alone
+
+node ('master') {
+	
+   stage ('ReportSonarQube') {
+       withSonarQubeEnv {
+            withMaven(
+                // Maven installation declared in the Jenkins "Global Tool Configuration"
+                maven: '3.5.4',
+                jdk: 'Java11') {
+                sh "mvn $SONAR_MAVEN_GOAL -Dsonar.login=$SONAR_AUTH_TOKEN -Dsonar.host.url=$SONAR_HOST_URL -Dsonar.branch=master"
+            }
+       }
+   }
+   
+   stage('p2Tests') {
+      wrap([$class: 'Xvnc', takeScreenshot: false, useXauthority: true]) {
+       sh '''
+          rm -rf TLAToolbox-?.?.?-linux.gtk.x86_64.zip
+		rm -rf toolbox/
+
+		## copy currently released Toolbox and extract it (We want to make sure that we can update from it to this build)
+		wget http://dl.tlapl.us/tlatoolbox/products/TLAToolbox-1.6.0-linux.gtk.x86_64.zip
+		unzip -qq TLAToolbox*.zip
+
+		cd toolbox/
+		
+		## Update current Toolbox release to this version
+		./toolbox -nosplash -application org.eclipse.equinox.p2.director \
+		-repository file://${WORKSPACE}/org.lamport.tla.toolbox.product.product/target/repository \
+		-uninstallIU org.lamport.tla.toolbox.product.product \
+		-installIU org.lamport.tla.toolbox.product.product \
+		-profileProperties org.eclipse.update.install.features=true
+
+		## Use Toolbox's p2 director to install the test feature into the previuos toolbox release to verify the update above worked and didn't trash anything.
+		./toolbox -nosplash -application org.eclipse.equinox.p2.director \
+		-repository file://${WORKSPACE}/org.lamport.tla.toolbox.p2repository/target/repository/ \
+		-installIU org.lamport.tla.toolbox.feature.uitest.feature.group
+
+		## Run the SWTBot smoke tests to check product zips
+		./toolbox -nosplash -application org.eclipse.swtbot.eclipse.junit.headless.swtbottestapplication \
+		-testApplication org.lamport.tla.toolbox.application \
+		-product org.lamport.tla.toolbox.product.standalone.product \
+		-nouithread \
+		-testPluginName org.lamport.tla.toolbox.tool.tlc.ui.uitest \
+		formatter=org.apache.tools.ant.taskdefs.optional.junit.PlainJUnitResultFormatter \
+		formatter=org.apache.tools.ant.taskdefs.optional.junit.XMLJUnitResultFormatter,org.lamport.tla.toolbox.tool.tlc.ui.uitest.SmokeTests.xml \
+		-className org.lamport.tla.toolbox.SmokeTests \
+		-data workspace$(date +%s) \
+		-clean
+
+		cp *.xml ${WORKSPACE}/
+       '''
+      }
+   }
+
+   stage ('RecordTestP2UpdateManager') {
+       // Collect junit output for p2 smoke tests
+       junit 'toolbox/org.lamport.tla.toolbox.tool.tlc.ui.uitest.SmokeTests.xml'
+   }
+   
+   stage('CreateRPMFile') {
+       sh '''
+        cd org.lamport.tla.toolbox.product.product/target/
+        fakeroot alien --to-rpm --scripts TLAToolbox-?.?.?-linux.gtk.amd64.deb
+        cp TLA*.rpm products/
+       '''
+   }
+   
+   stage('CreateAPTRepo') {
+       sh '''
+        chmod -x org.lamport.tla.toolbox.product.product/createAptRepo.sh
+        cp org.lamport.tla.toolbox.product.product/target/*.deb org.lamport.tla.toolbox.product.product/target/repository/
+        cd org.lamport.tla.toolbox.product.product/target/repository/
+        bash -x ../../createAptRepo.sh .
+       '''
+   }
+   
+   stage('RenderChangelog') { // Render the github flavord markdown to html
+       sh 'grip --context=tlaplus/tlaplus --export ${WORKSPACE}/general/docs/changelogs/ch1_6_1.md ${WORKSPACE}/general/docs/changelogs/changelog.html'
+   }
+}
+
+node ('macos') {
+    stage('SignToolbox') {
+        sh 'rm -rf *'
+        unstash 'toolbox'
+        sh 'ls -lah'
+        sh 'unzip org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.6.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.6.1-macosx.cocoa.x86_64.zip'
+        sh 'mv TLAToolbox-1.6.1-macosx.cocoa.x86_64.zip org.lamport.tla.toolbox.product.product/target/products/'
+        stash includes: 'org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.6.1-macosx.cocoa.x86_64.zip', name: 'signed'
+    }
+}
+
+node ('master') {
+   stage('Archive') {
+      unstash 'signed'
+      fingerprint '**/org.lamport.tla.toolbox.product.product/target/repository/, **/org.lamport.tla.toolbox.product.product/target/products/*.zip, **/org.lamport.tla.toolbox.product.product/target/products/*.deb, **/tlatools/dist/, **/org.lamport.tla.toolbox.doc/html/'
+
+      archiveArtifacts '**/general/docs/changelogs/changelog.html, **/org.lamport.tla.toolbox.product.product/target/org.lamport.tla.toolbox.product.product-1.4.0-SNAPSHOT.zip, **/org.lamport.tla.toolbox.p2repository/target/repository/, **/org.lamport.tla.toolbox.product.product/target/repository/, **/org.lamport.tla.toolbox.product.product/target/products/*.zip, **/org.lamport.tla.toolbox.product.product/target/products/*.deb, **/org.lamport.tla.toolbox.product.product/target/products/*.rpm, **/org.lamport.tla.toolbox.product.product/target/products/32bit_x86/*, **/tlatools/dist/, **/org.lamport.tla.toolbox.doc/html/'
+   }
+}
+
+node ('master') {
+   stage ('DraftGithubRelease') {
+	if (env.JOB_NAME == 'Release-HEAD-master-Toolbox') {
+         sh '''
+           #!/bin/bash
+
+           cd ${WORKSPACE}/general/docs/changelogs
+
+           ## Append sha1 sum to changelog (last line of changelog has the table header).
+           echo "$(sha1sum ${WORKSPACE}/tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar"  >> ch1_6_1.md
+           echo "$(sha1sum ${WORKSPACE}/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.6.1-win32.win32.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.6.1-win32.win32.x86_64.zip" >> ch1_6_1.md
+           echo "$(sha1sum ${WORKSPACE}/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.6.1-macosx.cocoa.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.6.1-macosx.cocoa.x86_64.zip" >> ch1_6_1.md     
+           echo "$(sha1sum ${WORKSPACE}/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.6.1-linux.gtk.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.6.1-linux.gtk.x86_64.zip" >> ch1_6_1.md
+           
+           ## Two above as one-liner without intermediate file.
+           $(jq -n --argjson changelog "$(cat ch1_6_1.md | jq  --raw-input --slurp .)" -f gh-1_6_1.jq > gh-1_6_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')
+           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_6_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')
+           for id in $(echo "$ASSETS"); do
+              ## DELETE /repos/:owner/:repo/releases/assets/:asset_id
+              curl -sS -X DELETE -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/assets/$id
+           done
+           
+            ## p2 repository
+            #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=repository.zip --upload-file ${WORKSPACE}/org.lamport.tla.toolbox.p2repository/target/repository/repository.zip
+            ## 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/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.6.1-macosx.cocoa.x86_64.zip --upload-file ${WORKSPACE}/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.6.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.6.1-win32.win32.x86_64.zip --upload-file ${WORKSPACE}/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.6.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.6.1-linux.gtk.x86_64.zip --upload-file ${WORKSPACE}/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.6.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.6.1-linux.gtk.amd64.deb --upload-file ${WORKSPACE}/org.lamport.tla.toolbox.product.product/target/repository/TLAToolbox-1.6.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.6.1-linux.gtk.amd64.rpm --upload-file ${WORKSPACE}/org.lamport.tla.toolbox.product.product/target/products/TLA\\+Toolbox-1.6.1~*.x86_64.rpm
+         '''
+        }
+   }
+}
+
+
+

CONTRIBUTING.md

@@ -6,6 +6,33 @@ Generally, we welcome contributions from volunteers. A number of [improvements w
 
 Except for [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Home.html), the TLA<sup>+</sup> tools are maintained in Eclipse. [For instructions on how to setup the Eclipse IDE, please go to general/ide/README.md.](https://github.com/tlaplus/tlaplus/tree/master/general/ide).
 
+Nightly Builds
+--------------
+
+Nightly builds of the [Toolbox](https://nightly.tlapl.us/products/) and [tla2tools](https://nightly.tlapl.us/dist/) are found at https://nightly.tlapl.us/products/ and https://nightly.tlapl.us/dist/, the [up-to-date changelog](https://nightly.tlapl.us/changelog.html) is at https://nightly.tlapl.us/changelog.html.  The Toolbox contains the latest version of tla2tools.jar for command-line usage in its root directory.
+
+It is also possible to configure the Toolbox to [automatically update to nightly (experimental) builds](https://nightly.tlapl.us/doc/update/update-preferences.html).  
+
+Note that it is called nightly for historical reasons, but builds are actually triggered by commits.
+
+#### Linux
+
+For dpkg-based Linux derivates such as Debian and Ubuntu, you can add the Toolbox's nightly package repository to your source list:
+
+```
+$ cat /etc/apt/sources.list.d/tlaplus.list
+deb https://nightly.tlapl.us/toolboxUpdate/ ./
+$ curl -fsSL https://tla.msr-inria.inria.fr/jenkins.pub | sudo apt-key add -
+```
+
+#### macOS
+
+The Toolbox's nightly builds are also made available as a [cask](https://github.com/Homebrew/homebrew-cask-versions/blob/master/Casks/tla-plus-toolbox-nightly.rb) through [homebrew versions](https://github.com/Homebrew/homebrew-cask-versions#usage):
+
+```bash
+$ brew tap homebrew/cask-versions
+$ brew install tlaplus-toolbox-nightly
+```
 
 Quality Metrics
 ---------------

azure-pipelines.yml

@@ -3,6 +3,12 @@
 # Add steps that analyze code, save build artifacts, deploy, and more:
 # https://docs.microsoft.com/azure/devops/pipelines/languages/java
 
+## https://docs.microsoft.com/en-us/azure/devops/pipelines/caching/?view=azure-devops#can-i-clear-a-cache
+variables:
+  MAVEN_CACHE_FOLDER: $(Pipeline.Workspace)/.m2/repository
+  MAVEN_OPTS: '-Dmaven.repo.local=$(MAVEN_CACHE_FOLDER)'
+
+
 jobs:
 
 - job: Linux
@@ -29,7 +35,7 @@ jobs:
   timeoutInMinutes: 0
 
   pool:
-    vmImage: 'vs2017-win2016'
+    vmImage: 'windows-2019'
 
   steps:
   - task: Maven@3
@@ -49,13 +55,13 @@ jobs:
   timeoutInMinutes: 0
 
   pool:
-    vmImage: 'macOS-10.13'
+    vmImage: 'macOS-10.14'
 
   steps:
   - task: Maven@3
     inputs:
       mavenPomFile: 'pom.xml'
-      mavenOptions: '-Xmx3072m -Dmaven.test.skip=true -Dorg.slf4j.simpleLogger.log.org.apache.maven.cli.transfer.Slf4jMavenTransferListener=warn'
+      mavenOptions: '-Xmx3072m -Dtest.skip=true -Dorg.slf4j.simpleLogger.log.org.apache.maven.cli.transfer.Slf4jMavenTransferListener=warn'
       options: '-fae -B'
       javaHomeOption: 'JDKVersion'
       jdkVersionOption: '1.11'

general/docs/Notarization_in_macOS.md

+## Adventures In macOS Notarization
+
+Due to [Issue 280](https://github.com/tlaplus/tlaplus/issues/280) we have been code signing the application. Beginning in January, 2020, users of Catalina (macOS 10.15) and later will need have their applications also be 'notarized.'
+
+A Java Program Manager at Microsoft, [wrote a Dummies guide](https://medium.com/@gdams/dummies-guide-to-notarizing-your-runtime-a1e9105b2c21) to notarizing which i attempted to apply to the Toolbox application, all from a Catalina install with XCode 11. Notes from following this, plus "insights" discovered from going wrong in the following and then Googling elsewhere, are below.
+
+### The Results, first
+
+I was able to get the .app notarized successfully with Apple; even after that, inquiring as to its signed status using `spctl` would still state that the app was rejected.
+
+In addition, after running the Toolbox the first time, subsequent queries using `spctl` would then tell me:
+```
+TLA+ Toolbox.app: a sealed resource is missing or invalid
+```
+
+The people at Eclipse are [successfully signing and notarizing 2019-09,](https://bugs.eclipse.org/bugs/show_bug.cgi?id=550135) so signing & notarizing RCPs are possible.
+
+### Signing certificates and passwords
+
+As done in 280, the signing certificates need be installed locally via XCode. Also make sure that you have logged into your account at developer.apple.com and have agreed to all of the latest AppConnect agreements, or you will get a message like
+```
+1 package(s) were not uploaded because they had problems:
+	/var/folders/fn/y4q2v5yx5fd0h7t20ss1qr780000gn/T/9C150E6E-4CD2-4C7C-828B-06B374C4A7ED/org.lamport.tla.toolbox.product.product.itmsp - Error Messages:
+		You must first sign the relevant contracts online. (1048)
+```
+when trying to notarize.
+
+Also, notarizing with Apple requires authentication, of course, during the upload. However, authentication with Apple is now always 2FA; to that extent, you must [generate an app-specific password.](https://support.apple.com/en-us/HT204397)
+
+Once you have an app-specific password, cram it in your KeyChain by doing something like:
+```
+xcrun altool --store-password-in-keychain-item "AC_PASSWORD" -u "your@apple.id" -p abcd-efgh-ijkl-mnop
+```
+
+Now you can refer to it in the KeyChain using an appropriate scheme, which we'll see later.
+
+### The routine
+
+Assuming you have built the Toolbox application change directories to be sitting in the directory containing `TLA+ Toolbox.app`
+
+#### The 'entitlements' file
+
+I cribbed this content from the medium.com article and saved it as 'entitlements.plist'
+```
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
+<plist version="1.0">
+<dict>
+    <key>com.apple.security.cs.allow-jit</key>
+    <true/>
+    <key>com.apple.security.cs.allow-unsigned-executable-memory</key>
+    <true/>
+    <key>com.apple.security.cs.disable-executable-page-protection</key>
+    <true/>
+    <key>com.apple.security.cs.allow-dyld-environment-variables</key>
+    <true/>
+    <key>com.apple.security.cs.disable-library-validation</key>
+    <true/>
+</dict>
+</plist>
+```
+
+#### Signing the app
+
+Now i signed the app itself with:
+```
+codesign --entitlements entitlements.plist --options runtime --timestamp -f -s "Developer ID Application: My Company Name (XXXX)" -v "TLA+ Toolbox.app" --deep
+```
+verifying the signing at this point shows:
+```
+loki@apalina Desktop % spctl --verbose=4 --assess --type execute "TLA+ Toolbox.app"
+TLA+ Toolbox.app: rejected
+source=Unnotarized Developer ID
+loki@apalina Desktop % codesign --verify -vvvv "TLA+ Toolbox.app"
+TLA+ Toolbox.app: valid on disk
+TLA+ Toolbox.app: satisfies its Designated Requirement
+loki@apalina Desktop %
+```
+
+#### Having Apple notarize the thing
+
+I then ZIP'd up the .app and then handed it over to Apple with (this is where we reference the app-specific password we crammed in the KeyChain):
+```
+loki@apalina Desktop % xcrun altool --notarize-app --primary-bundle-id "org.lamport.tla.toolbox.product.product" --username "your@apple.id" --password "@keychain:AC_PASSWORD" --file "TLA+ Toolbox.app.zip"
+No errors uploading 'TLA+ Toolbox.app.zip'.
+RequestUUID = de01d0fe-a88e-44fa-802f-da62ec93e994
+loki@apalina Desktop %
+```
+
+You can check the status with:
+```
+loki@apalina Desktop % xcrun altool --notarization-info de01d0fe-a88e-44fa-802f-da62ec93e994 --username "your@apple.id" --password "@keychain:AC_PASSWORD"
+No errors getting notarization info.
+
+          Date: 2019-10-30 22:21:36 +0000
+          Hash: 18eafe5a64abeef722316df47fb5c1f7249a7943df5bc65dccb5d697d00ba55d
+    LogFileURL: https://osxapps-ssl.itunes.apple.com/itunes-assets/Enigma113/v4/72/43/75/72xxx05a68b8c/developer_log.json?accessKey=xxx%3D
+   RequestUUID: de01d0fe-a88e-44fa-802f-da62ec93e994
+        Status: success
+   Status Code: 0
+Status Message: Package Approved
+loki@apalina Desktop %
+```
+and the service also sends an email when the process has finished.
+
+#### Done?
+
+At this point, unpacking the ZIP i uploaded and then verifying the signature on the .app shows:
+```
+loki@apalina Desktop % spctl --verbose=4 --assess --type execute "TLA+ Toolbox.app"
+TLA+ Toolbox.app: rejected
+source=Notarized Developer ID
+loki@apalina Desktop %
+```
+the app is still rejected, whatever that means; though the submission has been notarized.
+
+There is the notion of stapling (so that this notarization can be seen on machines that have no internet access,) however doing this:
+```
+loki@apalina Desktop % xcrun stapler staple "TLA+ Toolbox.app"
+Processing: /Users/loki/Desktop/TLA+ Toolbox.app
+Processing: /Users/loki/Desktop/TLA+ Toolbox.app
+The staple and validate action worked!
+loki@apalina Desktop % spctl --verbose=4 --assess --type execute "TLA+ Toolbox.app"
+TLA+ Toolbox.app: rejected
+source=Notarized Developer ID
+loki@apalina Desktop %
+```
+affects nothing obvious concerning the rejection.

general/docs/changelogs/ch1_6_0.md

@@ -108,3 +108,7 @@ Please check out the upcoming TLA+ conf at [http://conf.tlapl.us/](http://conf.t
 
 ### A note to macOS users
 Startup on macOS version 10.14 (Mojave) will fail with "TLA+ Toolbox can't be opened because Apple cannot check it for malicious software.".  Please make sure to follow the instructions outlined in [GitHub issue #320](https://github.com/tlaplus/tlaplus/issues/320) to address this problem.
+
+### Checksums
+sha1sum|file
+------------ | -------------
\ No newline at end of file

general/docs/changelogs/ch1_6_1.md

+### Changelog
+The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The [1.6.1 milestone](https://github.com/tlaplus/tlaplus/issues?q=is%3Aissue+milestone%3A1.6.1+is%3Aclosed) lists all completed issues.
+
+
+### Additional noteworthy changes
+
+#### TLC
+* Annotation-based loading of TLC module overrides for TLA+ operators. eb42f9ed462782c1577ec7433a993b770959437e
+* More powerful TLC module overrides that can programmatically manipulate a successor state. bb64cfd921c2e8846f47a5818d85cd0e8f2aa2c5
+* Write snapshots of state graph in dot/gv format after every new state. 305f38b1b7f68a0f4885615e7a148c3bf83aad95
+* A number of additions pertaining to working with trace expressions have been added to the command line tool `tlc2.TLC` and a new peer command line tool `tlc2.TraceExplorer` - see [GitHub Issue 393](https://github.com/tlaplus/tlaplus/issues/393) for an overview and background. Salient points include:
+ * Running TLC with both the `-generateSpecTE` flag will enable 'tool mode' output and, in the event that the model check encounters errors, generate a `SpecTE.tla` and `SpecTE.cfg` file pair that captures
+ the state trace reconstruction in an Init-Next relation spec.
+   * This `SpecTE.tla` will, by default, be a monolithic file, prefaced by the tool output, followed a the `SpecTE` MODULE definition which includes all extended non-StandardModule TLA code as well.
+     * To prevent the monolith inclusion of dependent TLA code, specify `nomonolith` after the `-generateSpecTE`
+ * Running TLC with `-h` now displays a usage page reminiscent of a standard man page.
+ * TraceExplorer exposes four capabilities:
+   * running the TraceExplorer with no spec name puts the TraceExplorer into a mode to receive input via stdin (e.g in order to pipe tool-mode output from TLC)
+   * pretty-printing: given an existing tool-mode output from a previous model check run (or piping in such output), pretty-printing will display an output stack to the terminal in basically the same format as one would see in the Toolbox's Error Viewer
+   * SpecTE generation: given an existing tool-mode output from a previous model check run (or piping in such output), create a `SpecTE.tla` and `SpecTE.cfg` file pair - this **will not** be a monolithic version.
+   * Expression exploration: given an existing tool-mode output from a previous model check run (or piping in such output), and file of expressions, one per line:
+     * create a `SpecTE.tla` and `SpecTE.cfg` file pair if one doesn't exist
+     * then create a `TE.tla` and `TE.cfg` file pair which extends SpecTE and contains appropriate conjunctions featuring the expressions
+     * then run model checking on this TE spec, both creating a `TE.out` and dumping the tool-mode output to stdout
+     * then do a courtesy pretty-print of the output. Pretty-printing in this scenario will ANSI-bold the expressions and their evaluated values
+   * Single expression exploration: as a sort of REPL-adjacent, any single TLA+ expression can be evaluated.
+   * running `tlc2.TraceExplorer` with no arguments, or `-h` will display helpful usage verbiage
+
+#### Toolbox
+
+##### Preferences
+* The Toolbox now supports selecting a Dark theme via `General → Appearance`.
+* The "Show Evaluate Constant Expression in its own tab" preference has been moved from `TLA+ Preferences → TLC Model Checker` to `TLA+ Preferences → Model Editor`.
+* The `TLA+ Preferences → TLAPS` preference subtree has been altered:
+ * the previous page at `TLA+ Preferences → TLAPS` is now at `TLA+ Preferences → TLAPS → Color Predicates`.
+ * The page previously at `TLA+ Preferences → TLAPS → Additional Preferences` is now renamed to `TLA+ Preferences → TLAPS → Other Preferences`.
+ * Non-color-predicate-related preferences from `TLA+ Preferences → TLAPS → Additional Preferences` have been moved into `TLA+ Preferences → TLAPS`.
+ * `TLA+ Preferences → TLAPS` now also features the ability to set a file system location for the `tlapm` executable should the Toolbox not be able to find it.
+* On macOS, you can now set the preference to have the operating system open PDFs with your default PDF viewer via `TLA+ Preferences → PDF Viewer`.
+
+##### Spec Editor
+* The spec editor now allows the collapsing of block comments, PlusCal code, and the TLA+ translation of PlusCal code. The first line of each of these types of runs should feature a minus icon in the line number gutter. Clicking on this icon will collapse the run; while in a collapsed state, holding the mouse over the, now: plus, icon will show the collapsed text as a tooltip.
+ * Please review the help page for the PlusCal translator in the Toolbox for guidance
+ as to how the comment block surround the PlusCal algorithm should be written.
+ * The preferences pane found at `TLA+ Preferences → Module Editor` allows for the setting of the default folding preferences (e.g 'always fold block comments when opening a specification in the editor.')
+* The spec editor also allows the collapsing of a contiguous run of two or more single line comments (where a single line comment is defined as a line starting with 0 or more spaces and or tabs, followed by a `\*`)
+* The translation of PlusCal code now generates a checksum of this code and the resulting TLA+ code; this checksum is calculated again when a model is executed and if it has changed, either a warning dialog will be displayed (if executed via the Toolbox) or a log warning will be emitted (if TLC is executed on the command line.)
+ * If you make a change to the generated TLA+ code, but do not want to be warned by the Toolbox of the divergence, you can delete only the TLA checksum (e.g `\** END TRANSLATION TLA-9b285153d0358878d62b88c9d4a6a047` → `\** END TRANSLATION`.) You will still be warned if the PlusCal code content is found to have changed without re-translating.
+* If attempting to generate a PDF of a spec fails because the `pdflatex` executable could not be found, a more informative warning dialog is now displayed for the user, including a way to directly open the Toolbox preference page specifying executable location.
+* The ability to user the prover against a spec will now be disabled while the spec fails to be successfully parsed.
+
+##### Model Editor
+* The style of the display of definitions in the "Definition Override" section in the Spec Options tab can be defined in the `TLA+ Preferences → Model Editor` preferences. There are two styles currently; given a `Definition` from a `Module Name` referenced in the primary spec like `InstanceName == INSTANCE ModuleName WITH ...`, then the two available styles are:
+ * `Definition [Module Name]`
+ * `InstanceName!Definition`
+* The Initial predicate / Next-state text areas were no longer interpreting a TAB as 'advance focus' due to a regression introduced when we moved to multi-line support for these text areas in 1.6.0. Both text areas now interpret a TAB as a focus advance; a TAB in the 'Init:' text area moves focus to the 'Next:' text area and a TAB in that text area advances the focus to the 'What is the model?' section.
+* New models now open a Model Editor instance with only a single tab - the Model Overview page. Running the model will open the Results tab, or should the user want to work immediately with evaluating constant expressions, there is a link at the bottom of the Model Overview page which will open the Results tab (as well as the Constant Expressions tab should the user have configured their preferences to show this in its own tab.)
+* Warn when checking liveness under action or state constraints (see [Specifying Systems](https://lamport.azurewebsites.net/tla/book.html) section 14.3.5 on page 247 for details).
+
+##### Spec Explorer
+* Right-clicking on model snapshots was incorrectly presenting the choice to rename the snapshot; this has been corrected.
+* Renaming specifications now correctly cleans up after itself [and should no longer prevent models from being opened.](https://github.com/tlaplus/tlaplus/issues/339)
+* Previously, opening a spec while the current spec had a dirty editor open, and to which the user chose to `Cancel` the offer to save the dirtied editor, resulted in the Toolbox continuing to open the new spec. This has been fixed - the opening process is halted and the original spec remains open.
+* Deleting a spec which has a currently dirty editor open for it, in which the user Cancel-s out of the dialog warning that the user is closing a dirty editor and asking whether they want to Don't Save, or Cancel, or Save, was continuing with the deletion of the spec. [It now stops the deletion process.](https://github.com/tlaplus/tlaplus/issues/375)
+
+##### Trace Explorer
+* The Error-Trace can now be filtered to omit one or more variables and/or expressions. Clicking on the filter icon, when filtering is not on, will display a dialog allowing the user to select from the set of variables and expressions found in the trace; alternatively, the user may ALT-click on a variable or expression in the Error-Trace tree view which will then omit that variable or expression. ([Screencast](https://raw.githubusercontent.com/tlaplus/tlaplus/master/general/docs/changelogs/screencasts/error-trace-filtering.gif))
+ * Also provided in the Error-Trace filtering dialog is the ability to hide variables whose values have not changed. For a variable that has changed at sometime during the trace, it may be displayed in either only the frames in which its value has changed, or in every frame of the trace. ([Screencast](https://raw.githubusercontent.com/tlaplus/tlaplus/master/general/docs/changelogs/screencasts/show_hide_changed_variables.gif))
+ * While filtering is enabled, a checkbox will be displayed above the variable value viewing text area allowing this area to display all the variables, or only the filtered variables, when a state is selected in the Error-Trace tree.
+* [Allow Trace-Explorer to extend additional TLA+ modules](https://github.com/tlaplus/tlaplus/issues/342) ([Screencast](https://raw.githubusercontent.com/tlaplus/tlaplus/master/general/docs/changelogs/screencasts/ExtendModulesForTraceExplorer.gif))
+* Export Error-Trace to system's clipboard ([Screencast](https://raw.githubusercontent.com/tlaplus/tlaplus/master/general/docs/changelogs/screencasts/ExportErrorTrace.gif))
+* Model checking can now be started using any given frame shown in the Error-Trace. Right-clicking on any location row will display a context menu giving the user the opportunity to run the model checking starting at that state. ([Screencast](https://raw.githubusercontent.com/tlaplus/tlaplus/master/general/docs/changelogs/screencasts/model_check_from_error_trace_state.gif))
+
+### Running checking in Ad Hoc mode
+* We have ended support for launching workers via JNLP; more information can be found on the master server's web page when running in this mode (e.g http://localhost:10996)
+
+### A note to macOS users
+Startup on macOS version 10.14 (Mojave) will fail with "TLA+ Toolbox can't be opened because Apple cannot check it for malicious software.".  Please make sure to follow the instructions outlined in [GitHub issue #320](https://github.com/tlaplus/tlaplus/issues/320) to address this problem.
+
+### Checksums
+sha1sum|file
+------------ | -------------

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

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

general/docs/contributions.md

@@ -53,3 +53,8 @@ We raised an [enhancement request for the jclouds toolkit](https://issues.apache
 
 #### Finish Unicode support (difficulty: easy) (skills: Eclipse, SANY)
 A few [outstanding issues](https://github.com/tlaplus/tlaplus/issues?q=is%3Aissue+is%3Aopen+label%3AUnicode) prevent the integration of the Unicode support into the Toolbox. In addition to the open issues, adding unit tests would be welcomed. A [nightly/ci Jenkins build](https://tla.msr-inria.inria.fr/build/job/M-HEAD-pron-unicode-Toolbox.product.standalone/) is available.
+
+TLA+ Tools
+----------
+#### Pretty Print to HTML (difficulty: easy) (skills: Java, HTML)
+TLA+ has a great pretty-printer to TeX (`tla2tex`), but HTML is becoming a de-facto document standard, especially for content shared online. HTML also has other advantages, such as the ability to automatically add hyperlinks from symbols to their definitions, and allow for collapsing and expanding proofs. The existing `tla2tex` code already contains most of the necessary parsing and typesetting pre-processing (like alignment), and could serve as a basis for an HTML pretty-printer. A [prototype already exists](https://github.com/tlaplus/tlaplus/issues/146).

general/ide/README.md

@@ -2,12 +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 11 - JDK (Java Development Environment) - OpenJDK is recommended.
-1. Install the Oomph Eclipse installer from https://wiki.eclipse.org/Eclipse_Installer
+0. Requires a recent - at the time of writing this is 13 - 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 "2018-12" as the product version at the bottom ![Chose Platform](https://raw.githubusercontent.com/lemmy/tlaplus/master/general/ide/images/00_PlatformSelection.png)
+  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.
 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

@@ -80,7 +80,7 @@
     <repository
         url="http://download.eclipse.org/technology/swtbot/releases/latest/"/>
     <repository
-        url="http://download.eclipse.org/tools/ajdt/47/dev/update/"/>
+        url="http://download.eclipse.org/tools/ajdt/48/dev/update/"/>
     <repository
         url="http://download.eclipse.org/technology/m2e/releases/"/>
     <repository
@@ -88,7 +88,7 @@
     <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!/"/>
     <repository
-        url="https://download.eclipse.org/rcptt/release/2.4.1/repository/"/>
+        url="https://download.eclipse.org/rcptt/release/2.4.3/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>
@@ -185,7 +185,4 @@
       xsi:type="setup:ProjectCatalog"
       href="index:/org.eclipse.setup#//@projectCatalogs[name='com.github']"/>
   <description>TLA+ provides the tlatools and the TLA+Toolbox</description>
-  <setup:PreferenceTask
-      key="/instance/org.eclipse.ui/defaultPerspectiveId"
-      value="org.eclipse.jdt.ui.JavaPerspective"/>
 </setup:Project>

org.lamport.tla.toolbox.doc/META-INF/MANIFEST.MF

@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: TLA+ Toolbox Help
 Bundle-SymbolicName: org.lamport.tla.toolbox.doc; singleton:=true
-Bundle-Version: 1.5.4.qualifier
+Bundle-Version: 1.6.1.qualifier
 Bundle-RequiredExecutionEnvironment: J2SE-1.4
 Bundle-Vendor: Simon Zambrovski, Leslie Lamport
 Bundle-ActivationPolicy: lazy

org.lamport.tla.toolbox.doc/html/gettingstarted/preferences.html

@@ -80,6 +80,7 @@ Click on the appropriate item in the following list to see what options
 these preference pages provide you with.
 </P>
 <ul>
+<li> <A href="../model/model-editor-preferences.html"> Model Editor Preferences</A></li>
 <li> <A href="module-editor-preferences.html"> Module Editor Preferences</A></li>
 <li> <A href="../spec/pretty-printing.html"> PDF Viewer Preferences</A></li>
 <li> <A href="../spec/parsing.html"> TLA+ Parser Preferences </A></li>