diff --git a/general/docs/microsoft-release.txt b/general/docs/microsoft-release.txt index f665aa5380b15165e7bf1e7f5c27401390f873a7..de3fe941f399a11fef5361193858c0196019562a 100644 --- a/general/docs/microsoft-release.txt +++ b/general/docs/microsoft-release.txt @@ -216,6 +216,7 @@ Version 1.5.0 - 11 May 2015 - Improvements to the Decompose Proof command. - Improvements to the TLC Errors view, including ability to show trace in reverse order. + - Has some changes to the way the Toolbox handles its subwindows. - Fixes all known bugs in TLC's liveness checking. - Fixes bug in TLC that caused infinite looping if a recursively defined operator is used as an operator argument in its own diff --git a/org.lamport.tla.toolbox.doc/html/prover/prover.html b/org.lamport.tla.toolbox.doc/html/prover/prover.html index d644d3bdcbe8584c3a437117a903ca8effbbd4fd..9afb9931eae43d18ab324a11e9fc26a52bf92f5a 100644 --- a/org.lamport.tla.toolbox.doc/html/prover/prover.html +++ b/org.lamport.tla.toolbox.doc/html/prover/prover.html @@ -1,80 +1,80 @@ -<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"> -<!-- This is file org.lamport.tla.toobox.doc/html/prover/prover.html --> -<html> -<head> - <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> - <LINK href="../style.css" rel="stylesheet" type="text/css"> - - <title>Proofs</title> -</head> -<!-- a comment --> - -<body> -<h1>Proofs</h1> - -<p> -The current version of the TLA+ language contains -several features not described in - <em><a href= - "http://research.microsoft.com/en-us/um/people/lamport/tla/book.html" - target="_blank"> - Specifying Systems</a></em>. - -Chief among them are constructs for writing hierarchically structured -proofs. - -The differences between the current and previous versions of TLA, including -the proof language, are described - <a href="http://research.microsoft.com/en-us/um/people/lamport/tla/tla2.html" - target="_blank">here</a>. -</p> - -<p> - -The Toolbox aids reading and writing hierarchically structured TLA+ proofs -by providing commands to view just the part of the structure that you -want to see. - -These commands are described in the subtopic -<A href="reading.html">Viewing and Editing Structured -Proofs</A>. -</p> - -<p> -TLAPS, the TLA+ Proof System, can be used to mechanically -check TLA+ proofs. - -You can select the parts of a proof to be checked, and you can have the -Toolbox display which steps' proofs have and have not been -checked. - -The <a href="runningTlaps.html">Running TLAPS</a> subtopic -describes how to run it from the Toolbox. - -But before you can run TLAPS, you must install it on your computer. - -Instructions for doing this, as well as an explanation of how to use -TLAPS, is on -<A href="http://msr-inria.inria.fr/~doligez/tlaps/" target="_blank">the TLAPS -web page</A>. - -As described on that page, if you are using Windows, you will also have -to install -<a href="http://www.cygwin.com/" target="_blank">Cygwin</a> on your computer. -</p> - -<p> -When using TLAPS, you will need to use the module <code>TLAPS.tla</code> and perhaps other -TLAPS library modules. The TLAPS download page will tell you in what -folder (directory) those modules are. The -<a href="../gettingstarted/tla-preferences.html#library-folders">TLA+ Preferences</a> page will allow -you to declare that modules from that folder should be usable in your specifications. -</p> -<dl> -<hr><dt><b><font color=#0000c0>Subtopics</font></b></dt> -<dd> <A href="reading.html">Viewing and Editing Structured Proofs</A></dd> -<dd> <A href="runningTlaps.html">Running TLAPS</A></dd> -</dl> -<a href = "../contents.html">↑ TLA+ Toolbox User's Guide</a> -</hr> -</body> +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"> +<!-- This is file org.lamport.tla.toobox.doc/html/prover/prover.html --> +<html> +<head> + <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> + <LINK href="../style.css" rel="stylesheet" type="text/css"> + + <title>Proofs</title> +</head> +<!-- a comment --> + +<body> +<h1>Proofs</h1> + +<p> +The current version of the TLA+ language contains +several features not described in + <em><a href= + "http://research.microsoft.com/en-us/um/people/lamport/tla/book.html" + target="_blank"> + Specifying Systems</a></em>. + +Chief among them are constructs for writing hierarchically structured +proofs. + +The differences between the current and previous versions of TLA, including +the proof language, are described + <a href="http://research.microsoft.com/en-us/um/people/lamport/tla/tla2.html" + target="_blank">here</a>. +</p> + +<p> + +The Toolbox aids reading and writing hierarchically structured TLA+ proofs +by providing commands to view just the part of the structure that you +want to see. + +These commands are described in the subtopic +<A href="reading.html">Viewing and Editing Structured +Proofs</A>. +</p> + +<p> +TLAPS, the TLA+ Proof System, can be used to mechanically +check TLA+ proofs. + +You can select the parts of a proof to be checked, and you can have the +Toolbox display which steps' proofs have and have not been +checked. + +The <a href="runningTlaps.html">Running TLAPS</a> subtopic +describes how to run it from the Toolbox. + +But before you can run TLAPS, you must install it on your computer. + +Instructions for doing this, as well as an explanation of how to use +TLAPS, on +<A href="https://tla.msr-inria.inria.fr/tlaps/content/Home.html" target="_blank">the TLAPS +web page</A>. + +As described on that page, if you are using Windows, you will also have +to install +<a href="http://www.cygwin.com/" target="_blank">Cygwin</a> on your computer. +</p> + +<p> +When using TLAPS, you will need to use the module <code>TLAPS.tla</code> and perhaps other +TLAPS library modules. The TLAPS download page will tell you in what +folder (directory) those modules are. The +<a href="../gettingstarted/tla-preferences.html#library-folders">TLA+ Preferences</a> page will allow +you to declare that modules from that folder should be usable in your specifications. +</p> +<dl> +<hr><dt><b><font color=#0000c0>Subtopics</font></b></dt> +<dd> <A href="reading.html">Viewing and Editing Structured Proofs</A></dd> +<dd> <A href="runningTlaps.html">Running TLAPS</A></dd> +</dl> +<a href = "../contents.html">↑ TLA+ Toolbox User's Guide</a> +</hr> +</body> diff --git a/org.lamport.tla.toolbox.doc/html/prover/runningTlaps.html b/org.lamport.tla.toolbox.doc/html/prover/runningTlaps.html index 2c33a30883bd87070a995e1ac957786beef09f2a..8598fbe9f5f5f1922a76e6f0e0250a2bdef85c65 100644 --- a/org.lamport.tla.toolbox.doc/html/prover/runningTlaps.html +++ b/org.lamport.tla.toolbox.doc/html/prover/runningTlaps.html @@ -393,11 +393,12 @@ This option tells the PM what SMT solver to use. See the <a href= - "http://msr-inria.inria.fr/~doligez/tlaps/advanced-tutorial.html#backends" - target="_blank">Using different backends</a> -section of the advanced -<a href="http://msr-inria.inria.fr/~doligez/tlaps/" - target="_blank">TLAPS documentation</a>. + "https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html#solvers" + target="_blank">SMT solvers</a> +section of the +<a href= + "https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html" + target="_blank">Tactics page</a>. (This field specifies the argument of the PM's <code>--solver</code> option.)