Updated README, added CONTRIBUTING and DEVELOPING docs

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

CONTRIBUTING.md

@@ -0,0 +1,71 @@
+Contributing to TLAPM
+---------------------
+
+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.
+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!
+If you open a massive pull request (PR) out of nowhere it is **very unlikely to be merged**.
+Follow this guide to ensure your effort is put to the best possible use.
+
+Always remember that we are all volunteers here.
+Be kind to everybody!
+You can review our Code of Conduct [here](.github/CODE_OF_CONDUCT.md).
+
+The Contribution Process & Style
+--------------------------------
+
+The most important step is to engage with existing developers & maintainers before beginning work.
+The best way to do this is to comment on an issue you want to fix, or open a new issue if a suitable candidate does not exist.
+It is also very helpful to join the [monthly online community meeting](https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfSBwAJ) to introduce yourself and speak with people directly.
+The development team will help you better understand the scope & difficulty of the proposed changes, along with what parts of the codebase they'll touch and what additional tests are required to safely merge them.
+Building & maintaining consensus around these aspects will ensure a smooth review & merge process.
+
+To begin work on your change, fork this repository then create an appropriately-named branch to track your work.
+You will eventually submit a PR between your feature branch and the master branch of this repository, at which point developers & maintainers will review your changes.
+After integrating this feedback your PR will then hopefully be merged.
+
+When creating and submitting your changes, closely follow these guidelines:
+ * **Be surgical:** What is the smallest diff you can make that still accomplishes your goal?
+ Avoid the urge to fix unrelated stylistic issues in a file you are changing.
+ * **Write tests first:** If you're changing a specific part of the codebase, first ensure it has good test coverage; if it does, write a few more tests yourself anyway!
+ Writing tests is a great way to learn how the code functions.
+ If possible, submit your tests in a separate PR so their benefits can be realized immediately.
+ We don't fully subscribe to Test-Driven Development (TDD) but having good existing test coverage of a changed area is a prerequisite to changes being merged.
+ * **Split up your changes:** If parts of your changes provide some benefit by themselves - like additional tests - split them into a separate PR.
+ It is preferable to have several small PRs merged quickly than one large PR that takes longer to review.
+ * **Craft your commits well:** This can require advanced git knowledge (see [DEVELOPING.md](DEVELOPING.md)).
+ Treat your commits as forms of communication, not a way to bludgeon the codebase into shape.
+ You don't need to check this, but ideally the build & tests should pass on every commit.
+ This means you will often be amending commits as you work instead of adding new ones.
+
+When you open a PR against this repo, the continuous integration (CI) checks will run.
+These ensure your changes do not break the build & tests.
+While you can run most of these checks locally, if you'd like to run the CI at any time you can open a PR between your feature branch and the master branch of *your own* fork of this repo.
+
+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.
+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).
+If you have an idea for a new feature, open an issue in this repository to start a discussion.
+In the rare case that a compelling feature requires more fundamental changes to the TLA⁺ language itself, you can [open a RFC](https://github.com/tlaplus/rfcs/issues).
+Often it will be necessary to build community support for your idea; for this you can use the [mailing list](https://groups.google.com/g/tlaplus) and especially the [monthly online community meeting](https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfSBwAJ).
+Expressions of goodwill like volunteering labor to review pending PRs is also appreciated!
+
+Getting Started
+---------------
+
+Take the time to set up your local development environment.
+See [DEVELOPING.md](DEVELOPING.md) for details.
+Have fun, and keep in touch!
+

DEVELOPING.md

@@ -0,0 +1,160 @@
+Overview
+--------
+This file contains basic installation instructions as well as development knowledge & practices for this project.
+You will learn the repository structure, how to build & test the software it contains from your command line interface (CLI), how to set up your interactive development environment (IDE), and several other tidbits.
+This project is mostly written in [OCaml](https://ocaml.org/) with some [Isabelle](https://isabelle.in.tum.de/) code.
+It uses the [Dune](https://dune.build/) build system for OCaml, with [Make](https://www.gnu.org/software/make/) used to compile the backend theorem provers.
+
+Release Channels
+----------------
+You can find official versioned releases on the [GitHub Releases page](https://github.com/tlaplus/tlapm/releases).
+
+Official releases lag the current development frontier by quite some time; thus, you might prefer to clone & build TLAPM yourself, as described below.
+Plans exist to make rolling pre-releases available in the near future.
+
+Dependencies
+------------
+TLAPM 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:
+```sh
+apt install zlib1g-dev gawk time
+```
+On Arch Linux:
+```sh
+pacman -Sy wget time zlib patch diffutils fontconfig gnu-free-fonts
+```
+Install the following dependencies to your path:
+* [OCaml](https://ocaml.org/install) 4.08.1 or later (usually installed using [opam](https://opam.ocaml.org/))
+* [Dune](https://dune.build/install)
+* [Make](https://www.gnu.org/software/make/)
+
+OCaml requires that you initialize an environment within your shell.
+For example, you can create & initialize an OCaml 5.1.0 environment with:
+```sh
+opam switch create 5.1.0
+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
+---------------------
+Clone this repo & open a shell in its root.
+Install OCaml package dependencies with:
+```sh
+make opam-update
+make opam-deps
+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:
+```sh
+make
+```
+Install TLAPM 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:
+```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.
+
+Test TLAPM
+----------
+You can run all tests with:
+```sh
+make test
+```
+You can run specific tests or groups of tests with (for example):
+```sh
+dune runtest test/parser --force --always-show-command-line
+```
+
+IDE Setup
+---------
+You are free to use your own editor, but most people develop this project using VS Code with the [OCaml Platform](https://github.com/ocamllabs/vscode-ocaml-platform) extension.
+
+If you are new to OCaml coming from other programming languages, you might expect the debugger to be an important tool.
+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:
+```sh
+dune utop
+```
+
+Repository Layout
+-----------------
+Here is a diagram of the repository layout.
+There are other files and directories beyond these, but these are the most important:
+```
+/
+├── LICENSE                     # The project license
+├── 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
+├── 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
+├── 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⁺
+├── 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
+├── 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
+└───.github/
+    ├── CODE_OF_CONDUCT.md      # The code of conduct
+    └── workflows/              # GitHub CI workflow definition files
+        ├── ci.yml              # The CI workflow that validates PRs
+        └── release.yml         # CI workflow to publish a release
+```
+
+Using Git
+---------
+
+Git was designed to shine in a federated open source development model.
+You are likely to require use of more of its features here than you would in a corporate development environment.
+Here is a brief primer on using git to develop this project.
+It assumes a basic familiarity with common git operations like clone, commit, push, and pull.
+There are countless free and paid git guides available online; [here](https://www.git-scm.com/doc) are the docs from the git project itself, and [here](https://wizardzines.com/git-cheat-sheet.pdf) is a useful cheat-sheet from Julia Evans.
+
+### PR Conventions
+
+Reshape your PR commits to publishable shape: unless you want all your commits to be squashed into a single commit when the PR is merged, craft each commit with care into a logical series of changes with descriptive messages.
+Modify each commit in place in response to PR feedback.
+
+Unfortunately GitHub does not really support patch series, so if you have multiple PRs that stack on top of each other the only real way to handle it is to wait until each one is accepted before opening the next, or put them into a single PR where each PR is mapped to a single commit with a descriptive message.
+
+### Developer Certificate of Origin (DCO) sign-off
+
+Due to legal disputes in the mid-2000s, all commits to projects under the Linux Foundation are required to contain a [Developer Certificate of Origin (DCO)](https://en.wikipedia.org/wiki/Developer_Certificate_of_Origin) sign-off (note this is different from signing commits with a GPG key).
+This basically says that you (the developer) were entirely responsible for writing the code in the commit and that you are legally permitted to contribute it under a permissive license (it isn't copied from proprietary code, for example).
+In git this is easily done by adding an extra `-s` flag as you commit:
+```bash
+git commit -s -am "Commit message here"
+```
+Don't worry too much about forgetting this; the CI will catch it and GitHub provides a page with simple instructions to retroactively add DCO sign-off to past commits.
+Eventually adding the `-s` flag will become muscle memory.
+

LICENSE

@@ -1,5 +1,5 @@
-Copyright (c) 2008-2013  INRIA and Microsoft Corporation
-All rights reserved.
+Copyright (c) 2008 INRIA and Microsoft Corporation
+Copyright (c) 2023 Linux Foundation
 
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are