From 2c9bb6986176a8f5a32ff4f538852d3e281a9b93 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe <tlaplus.net@lemmster.de> Date: Wed, 30 Dec 2020 19:11:15 -0800 Subject: [PATCH] Set release date and increment version number of TLC. [Build] --- general/docs/changelogs/ch1_7_1.md | 12 ++---------- .../org.lamport.tlatools/src/pcal/PcalParams.java | 15 ++++++++++----- .../org.lamport.tlatools/src/tlc2/TLCGlobals.java | 2 +- ...rg.lamport.tla.toolbox.product.product.product | 6 +++--- .../plugin.xml | 2 +- .../tla/toolbox/ui/intro/ToolboxIntroPart.java | 2 +- 6 files changed, 18 insertions(+), 21 deletions(-) diff --git a/general/docs/changelogs/ch1_7_1.md b/general/docs/changelogs/ch1_7_1.md index 45b386f90..5d8971048 100644 --- a/general/docs/changelogs/ch1_7_1.md +++ b/general/docs/changelogs/ch1_7_1.md @@ -3,27 +3,19 @@ The high level changelog is available at http://research.microsoft.com/en-us/um/ ### Additional _noteworthy_ changes -#### Tools - -##### Bugfix -* TLC shows no error *trace* for violations of `TLC!Assert`, ... (regression in 1.7.0) https://github.com/tlaplus/tlaplus/issues/461 +* TLC shows no error *trace* for violations of `TLC!Assert`, ... https://github.com/tlaplus/tlaplus/issues/461 * NoClassDefError when running TLC on Java 1.8. https://github.com/tlaplus/tlaplus/issues/462 * Dot visualization (graphviz) fails due to invalid character ! when spec uses instantiation https://github.com/tlaplus/tlaplus/issues/452 * Simulation mode ignores ASSUMPTIONS. https://github.com/tlaplus/tlaplus/issues/496 * Back to state missing for lasso error trace found by simulation https://github.com/tlaplus/tlaplus/issues/497 * AtNode does not show up in (dot) graph output of semantic explorer 52f3b01 * Replace custom implementation of (heap) sort in TeX with java.utils.Arrays#sort https://github.com/tlaplus/tlaplus/issues/539 -End support for liveness checking and multiple workers in DFID mode because both features are unreliable https://github.com/tlaplus/tlaplus/issues/548 https://github.com/tlaplus/tlaplus/issues/544 - -#### Toolbox - -##### Bugfix +* End support for liveness checking and multiple workers in DFID mode because both features are unreliable https://github.com/tlaplus/tlaplus/issues/548 https://github.com/tlaplus/tlaplus/issues/544 * Multiline trace expressions fail to parse in Toolbox. defe0c74915b1c27c6af2fb55c8163f3574c8918 * 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 * Upgrade Eclipse foundation to its 2020-06 release for better HiDPI support. https://github.com/tlaplus/tlaplus/issues/472 * Toolbox intermittently shows no error trace on an invariant violation https://github.com/tlaplus/tlaplus/issues/538 - ### Checksums sha1sum|file ------------ | ------------- diff --git a/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java b/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java index 22de7b25f..51be055c8 100644 --- a/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java +++ b/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java @@ -18,8 +18,13 @@ public final class PcalParams /** * Parameters to be updated on each new release. */ - public static final String modDate = "10 July 2019"; - public static final String version = "1.9"; + public static final String modDate = "31 December 2020"; + // Can't increment 1.9 to 1.10 because VersionToNumber(str) calculates a lower + // numerical value for 1.10 than it does for 1.9. This breaks the FairSeq?Test + // tests. Until we switch from 1.xx to 2.0, increment versionWeight along with + // version. + public static final int versionWeight = 1902; + public static final String version = "1.11"; /** * SZ Mar 9, 2009: * Added re-initialization method. Since PcalParams class @@ -50,7 +55,7 @@ public final class PcalParams NoDoneDisjunct = false; optionsInFile = false; versionOption = null; - inputVersionNumber = VersionToNumber(PcalParams.version); + inputVersionNumber = PcalParams.versionWeight; PcalTLAGen.wrapColumn = 78; PcalTLAGen.ssWrapColumn = 45; tlaPcalMapping = null ; @@ -247,7 +252,7 @@ public final class PcalParams // way because of the way the code evolved, and no intelligent // design has stepped in to fix it. public static String versionOption = null; - public static int inputVersionNumber = VersionToNumber(PcalParams.version); + public static int inputVersionNumber = PcalParams.versionWeight; // The input file's version number * 1000 // public static boolean readOnly = false; // True iff this is a .pcal input file and the .tla file should @@ -310,7 +315,7 @@ public final class PcalParams PcalDebug.reportError("Illegal version " + ver + " specified."); return false; } - if (vnum > VersionToNumber(PcalParams.version)) { + if (vnum > PcalParams.versionWeight) { PcalDebug.reportError("Specified version " + ver + " later than current version " + PcalParams.version); return false; diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java b/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java index e6aee0b5c..d68116ed6 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java @@ -23,7 +23,7 @@ public class TLCGlobals public static final int DEFAULT_CHECKPOINT_DURATION = (30 * 60 * 1000) + 42; // The current version of TLC - public static String versionOfTLC = "Version 2.15 of Day Month 20??"; + public static String versionOfTLC = "Version 2.16 of 31 December 2020"; // The bound for set enumeration, used for pretty printing public static int enumBound = 2000; diff --git a/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product b/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product index 504bf7316..e79ef3fa9 100644 --- a/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product +++ b/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product @@ -8,10 +8,10 @@ <text> TLA+ Toolbox provides a user interface for TLA+ Tools. -This is Version 1.7.1 of Day Month Year and includes: +This is Version 1.7.1 of 31 December 2020 and includes: - SANY Version 2.2 of 20 April 2020 - - TLC Version 2.15 of 20 April 2020 - - PlusCal Version 1.10 of 20 April 2020 + - TLC Version 2.16 of 31 December 2020 + - PlusCal Version 1.11 of 31 December 2020 - TLATeX Version 1.0 of 20 September 2017 Don't forget to click on help. You can learn about features that you never knew about or have forgotten. diff --git a/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml b/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml index 620d83498..98d54a174 100644 --- a/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml +++ b/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml @@ -30,7 +30,7 @@ </property> <property name="aboutText" - value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.7.1 of Day Month Year and includes:
 - SANY Version 2.2 of 20 April 2020
 - TLC Version 2.15 of 20 April 2020
 - PlusCal Version 1.10 of 20 April 2020
 - TLATeX Version 1.0 of 20 September 2017

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .

Some icons used in the Toolbox were provided by www.flaticon.com"> + value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.7.1 of 31 December 2020 and includes:
 - SANY Version 2.2 of 20 April 2020
 - TLC Version 2.16 of 31 December 2020
 - PlusCal Version 1.11 of 31 December 2020
 - TLATeX Version 1.0 of 20 September 2017

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .

Some icons used in the Toolbox were provided by www.flaticon.com"> </property> <property name="aboutImage" diff --git a/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java b/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java index 5467a41bb..8a8e21c45 100644 --- a/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java +++ b/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java @@ -431,7 +431,7 @@ public class ToolboxIntroPart extends IntroPart implements IIntroPart { final Label lblVersion = new Label(outerContainer, SWT.WRAP); lblVersion.setLayoutData(new GridData(SWT.FILL, SWT.CENTER, false, false, 2, 1)); - lblVersion.setText("Version 1.7.1 of Day Month Year"); + lblVersion.setText("Version 1.7.1 of 31 December 2020"); lblVersion.setBackground(backgroundColor); } -- GitLab