README: updated description of TLAPS vs TLAPM

Signed-off-by: Andrew Helwer <[email protected]>

Author: ahelwer

CONTRIBUTING.md

@@ -1,11 +1,11 @@
-Contributing to TLAPM
+Contributing to TLAPS
 ---------------------
 
 TL;DR: engage maintainers early & often, be surgical in your changes, and write lots of tests.
 
 We welcome contributions to this open source project!
 Before beginning work, please take some time to familiarize yourself with our development processes and expectations.
-TLAPM is used to validate safety-critical systems, so maintaining quality is paramount.
+TLAPS is used to validate safety-critical systems, so maintaining quality is paramount.
 The existing code can also be quite complicated to modify and it is difficult to review changes effectively.
 So, there are several practices that are necessary for having a good contribution experience.
 The last thing anybody wants is for you to feel as though you have wasted your time!
@@ -53,7 +53,7 @@ Contribution Possibilities
 These tools have a large number existing issues to fix, which you can see on the repo's [issues tab](https://github.com/tlaplus/tlapm/issues).
 
 Non-code contributions are particularly desired!
-TLAPM documentation needs a lot of work.
+TLAPS documentation needs a lot of work.
 The docs are hosted at https://proofs.tlapl.us and live in this repo in the [doc/web](doc/web) directory.
 
 For new features, there are a number of [substantial improvements we'd like to see implemented](todo.txt).

DEVELOPING.md

@@ -8,16 +8,16 @@ It uses the [Dune](https://dune.build/) build system for OCaml, with [Make](http
 Release Channels
 ----------------
 Past versioned releases can be downloaded from the [GitHub Releases page](https://github.com/tlaplus/tlapm/releases).
-For the latest development version, download the builds attached to the [1.6.0 rolling pre-release](https://github.com/tlaplus/tlapm/releases/tag/1.6.0-pre) or follow the instructions below to build TLAPM from source.
+For the latest development version, download the builds attached to the [1.6.0 rolling pre-release](https://github.com/tlaplus/tlapm/releases/tag/1.6.0-pre) or follow the instructions below to build TLAPS from source.
 
 Dependencies
 ------------
-TLAPM development & use is only supported on Unix-like systems, such as:
+TLAPS development & use is only supported on Unix-like systems, such as:
 * Any modern Linux
 * macOS
 * Windows Subsystem for Linux
 
-For building TLAPM, some Linux distros require additional packages beyond the base install; on Debian/Ubuntu:
+For building TLAPS, some Linux distros require additional packages beyond the base install; on Debian/Ubuntu:
 ```sh
 apt install zlib1g-dev gawk time
 ```
@@ -38,7 +38,7 @@ eval $(opam env --switch=5.1.0)
 ```
 You can put the `eval` statement in your shell init file (`~/.bashrc` or similar) to ensure your shell always has an active OCaml environment.
 
-Build & Install TLAPM
+Build & Install TLAPS
 ---------------------
 Clone this repo & open a shell in its root.
 Install OCaml package dependencies with:
@@ -49,26 +49,26 @@ make opam-deps-opt
 ```
 Package dependencies are unfortunately not yet declarative, but [will be in the future](https://github.com/tlaplus/tlapm/issues/158#issuecomment-2455455589).
 
-Compile the embedded dependencies and TLAPM with:
+Compile the embedded dependencies and TLAPS with:
 ```sh
 make
 ```
-Install TLAPM to your local OCaml environment with:
+Install TLAPS to your local OCaml environment with:
 ```sh
 make install
 ```
 This should put `tlapm` on your path from your local OCaml environment, but if not you can run:
 ```sh
 opam exec -- tlapm --help
 ```
-Compile a TLAPM release distributable with:
+Compile a TLAPS release distributable with:
 ```sh
 make release
 ```
 This will output a file to `_build/tlaps-$GIT_COMMMIT_HASH-$ARCH-$OS.tar.gz`; for example, running `make release` on Linux produced the file `_build/tlaps-a7a3a0a-x86_64-linux-gnu.tar.gz`.
-This file can be used the same as any downloaded TLAPM release.
+This file can be used the same as any downloaded TLAPS release.
 
-Test TLAPM
+Test TLAPS
 ----------
 You can run all tests with:
 ```sh
@@ -87,7 +87,7 @@ If you are new to OCaml coming from other programming languages, you might expec
 This is not so!
 The OCaml debugger is not often used, and [you will encounter many problems](https://github.com/tlaplus/tlapm/discussions/143#discussioncomment-10277989) when trying to use it.
 Instead (as befits a functional language), people use a REPL when analyzing parts of the codebase.
-The [UTop](https://opam.ocaml.org/blog/about-utop/) REPL (aka toplevel) works well; you can enter a UTop instance with TLAPM libraries available by running:
+The [UTop](https://opam.ocaml.org/blog/about-utop/) REPL (aka toplevel) works well; you can enter a UTop instance with TLAPS libraries available by running:
 ```sh
 dune utop
 ```
@@ -102,26 +102,26 @@ There are other files and directories beyond these, but these are the most impor
 ├── README.md                   # Basic info about the project
 ├── DEVELOPING.md               # This document
 ├── CONTRIBUTING.md             # How to contribute to the project
-├── hints.txt                   # Some tips on effectively writing TLAPM proofs
+├── hints.txt                   # Some tips on effectively writing TLAPS proofs
 ├── todo.txt                    # Feature wishlist
 ├── dune-project                # Top-level Dune project file (generates tlapm.opam)
 ├── Makefile                    # Makefile for installing dependencies & launching Dune builds
 ├── index.html                  # proofs.tlapl.us root page; currently redirects to docs
 ├── deps/                       # Makefiles for dependencies (LS4, Isabelle, Z3, etc.)
-├── doc/                        # Sources for TLAPM documentation on proofs.tlapl.us
+├── doc/                        # Sources for TLAPS documentation on proofs.tlapl.us
 ├── examples/                   # Some example proofs that can be used as tests
 ├── isabelle/                   # Embedding of non-temporal parts of TLA⁺ in Isabelle
-├── library/                    # The TLAPM standard modules for TLA⁺
+├── library/                    # The TLAPS standard modules for TLA⁺
 ├── translate/                  # External library for translating temporal logic formulas to LS4
 ├── zenon/                      # The vendored source code of the Zenon theorem prover
 ├── misc/
-│   └── tla_mode/               # A TLAPM mode for Emacs
-├── lsp/                        # A language server for checking TLA⁺ proofs with TLAPM
+│   └── tla_mode/               # A TLAPS mode for Emacs
+├── lsp/                        # A language server for checking TLA⁺ proofs with TLAPS
 ├── src/                        # Main TLAPM source code directory
 │   ├── dune                    # Dune build file
 │   ├── tlapm.ml                # The main entrypoint to the TLAPM CLI
 │   └── tlapm_lib.mli           # Main interface for TLAPM when used as a library
-├── test/                       # Tests for TLAPM
+├── test/                       # Tests for TLAPS
 └── .github/
     ├── CODE_OF_CONDUCT.md      # The code of conduct
     └── workflows/              # GitHub CI workflow definition files

README.md

@@ -1,19 +1,20 @@
-The TLA⁺ Proof Manager (`tlapm`)
-================================
+The TLA⁺ Proof System
+=====================
 [![Build & Test](https://github.com/tlaplus/tlapm/actions/workflows/ci.yml/badge.svg?branch=main)](https://github.com/tlaplus/tlapm/actions/workflows/ci.yml)
 
-This repository hosts the TLA⁺ Proof Manager TLAPM, formerly known as TLAPS.
-TLAPM translates TLA⁺ proof constructs into forms understood by an array of backend solvers & theorem provers, enabling machine-checked proofs of correctness for TLA⁺ specifications.
-TLAPM's development is managed by the [TLA⁺ Foundation](https://foundation.tlapl.us/).
+This repository hosts what is collectively called the TLA⁺ Proof System, or TLAPS.
+It consists of the TLA⁺ Proof Manager `tlapm` that interprets TLA⁺ proofs & manages their state, as well as interfaces to automatic backend provers such as [SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) solvers like [Z3](https://github.com/Z3Prover/z3), the [tableau](https://en.wikipedia.org/wiki/Method_of_analytic_tableaux) prover [Zenon](https://github.com/zenon-prover/zenon), the [Isabelle](https://isabelle.in.tum.de/)/TLA⁺ object logic, and the LS4 decision procedure for [propositional temporal logic](https://en.wikipedia.org/wiki/Linear_temporal_logic).
+
+TLAPS development is managed by the [TLA⁺ Foundation](https://foundation.tlapl.us/).
 For documentation, see http://proofs.tlapl.us.
 For information on TLA⁺ generally, see http://tlapl.us.
 
 Installation & Use
 ------------------
 Past versioned releases can be downloaded from the [GitHub Releases page](https://github.com/tlaplus/tlapm/releases).
-For the latest development version, download the builds attached to the [1.6.0 rolling pre-release](https://github.com/tlaplus/tlapm/releases/tag/1.6.0-pre) or follow the instructions in [`DEVELOPING.md`](DEVELOPING.md) to build TLAPM from source.
+For the latest development version, download the builds attached to the [1.6.0 rolling pre-release](https://github.com/tlaplus/tlapm/releases/tag/1.6.0-pre) or follow the instructions in [`DEVELOPING.md`](DEVELOPING.md) to build TLAPS from source.
 
-Once TLAPM is installed, run `tlapm --help` to see documentation of the various command-line parameters.
+Once TLAPS is installed, run `tlapm --help` to see documentation of the various command-line parameters.
 Check the proofs in a simple example spec in this repo by running:
 ```sh
 tlapm examples/Euclid.tla
@@ -22,14 +23,14 @@ Documentation is hosted at http://proofs.tlapl.us, or can be viewed locally from
 
 Developing & Contributing
 -------------------------
-For instructions on building & testing TLAPM as well as setting up a development environment, see [DEVELOPING.md](DEVELOPING.md).
+For instructions on building & testing TLAPS as well as setting up a development environment, see [DEVELOPING.md](DEVELOPING.md).
 
 We welcome your contributions to this open source project!
-TLAPM is used in safety-critical systems, so we have a contribution process in place to ensure quality is maintained; read [CONTRIBUTING.md](CONTRIBUTING.md) before beginning work.
+TLAPS is used in safety-critical systems, so we have a contribution process in place to ensure quality is maintained; read [CONTRIBUTING.md](CONTRIBUTING.md) before beginning work.
 
 Authors
 -------
-The following people were instrumental in creating TLAPM:
+The following people were instrumental in creating TLAPS:
 - [Kaustuv Chaudhuri](https://chaudhuri.info/) (@[chaudhuri](https://github.com/chaudhuri))
 - Denis Cousineau
 - [Damien Doligez](http://cambium.inria.fr/~doligez/) (@[damiendoligez](https://github.com/damiendoligez))