diff --git a/book.toml b/book.toml index 66183a2..8e79453 100644 --- a/book.toml +++ b/book.toml @@ -1,6 +1,14 @@ +[preprocessor.last-changed] +command = "mdbook-last-changed" +renderer = ["html"] [book] authors = ["Federico Ponzi"] language = "en" multilingual = false src = "src" title = "TLA+ Wiki" + +[output.html] +# Optional: Your repository URL used in the link. +git-repository-url = "https://github.com/FedericoPonzi/tlaplus-wiki" +additional-css = ["last-changed.css"] \ No newline at end of file diff --git a/last-changed.css b/last-changed.css new file mode 100644 index 0000000..682e897 --- /dev/null +++ b/last-changed.css @@ -0,0 +1,6 @@ +footer { + font-size: 0.7em; + text-align: center; + border-top: 1px solid black; + margin: 30px 0; + } \ No newline at end of file diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 998de33..bc39597 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -1,24 +1,31 @@ # Summary - [TLA+ Wiki intro](./intro.md) - - [Contributing]() + - [Contributing](./contributing.md) ---- - [TLA+ Codebase](./codebase/intro.md) - [Contributing](./codebase/contributing.md) - - [Setting up the development environment](./codebase/ide.md) + - [Setting up the development environment](./codebase/devenv.md) - [CI/CD overview](./codebase/ci-cd.md) - [Codebase Architecture Walkthrough](./codebase/architecture.md) - [Codebase Idiosyncrasies](./codebase/idiosyncrasies.md) - [Wishlist](./codebase/wishlist.md) - [Benchmarks]() - [SANY]() - - [JPF]() + - [Java Path Finder](./codebase/jpf.md) - []() -- [Learning TLA+]() +- [Learning TLA+](./learning/intro.md) - [Lamport's video tutorial]() - [Example repo]() - [Notable repos]() -- [Using TLA+ and TLC](./using/intro.md) + - [Books]() + - [TLA]() + - [Typed Model Values]() + - [Pluscal]() + - []() + - [TLA+ Vs xxx](./learning/tla-comparisons.md) +- [Learning TLAP]() +- [Tools](./using/intro.md) - [Vscode extension](./using/vscode.md) - [Toolbox](./using/toolbox.md) - [TLC CLI](./using/tlc-cli.md) diff --git a/src/codebase/ci-cd.md b/src/codebase/ci-cd.md index f02b775..bbc4e41 100644 --- a/src/codebase/ci-cd.md +++ b/src/codebase/ci-cd.md @@ -1 +1,6 @@ # CI/CD overview +The CI/CD is currently handled by Github Actions. + +The tests are run as part of every PR and for every merge to main. The codebase is built against both Mac and Linux. + + diff --git a/src/codebase/ide.md b/src/codebase/devenv.md similarity index 100% rename from src/codebase/ide.md rename to src/codebase/devenv.md diff --git a/src/codebase/intro.md b/src/codebase/intro.md index 4524b70..c42e085 100644 --- a/src/codebase/intro.md +++ b/src/codebase/intro.md @@ -1,4 +1,6 @@ # TLA+ codebase -The tlatools codebase is a complex one, there are over 600k lines of code, in over 2000 files, written over 20+ years. And yet as the best distributed systems modelling tool on the market today, maintaining and improving it is critical. +The tlaplus codebase is very complex. There are over 600k lines of code, in over 2000 files, written over 20+ years. And yet as the best distributed systems modelling tool on the market today, maintaining and improving it is critical. -This overview is meant to orient new programmers as well as reorient existing ones. \ No newline at end of file +TLA+ should be regarded as a piece of mission critical software, like a cryptography library. This means that it cannot accept any kind of change that could potentially break it. Especially because being open source software means that somebody will also need to spend time fixing it. + +This chapter is meant to orient new programmers that want to navigate the codebase and start contributing, as well as reorient existing ones. diff --git a/src/codebase/jpf.md b/src/codebase/jpf.md new file mode 100644 index 0000000..25745c0 --- /dev/null +++ b/src/codebase/jpf.md @@ -0,0 +1,5 @@ +# Java Path Finder +Java Path Finder is a project developed by nasa for model checking Java bytecode. See [https://github.com/javapathfinder/jpf-core](https://github.com/javapathfinder/jpf-core). + +JPF is used to test some of the tla+ classes. + diff --git a/src/contributing.md b/src/contributing.md new file mode 100644 index 0000000..35a85fb --- /dev/null +++ b/src/contributing.md @@ -0,0 +1,5 @@ +# Contributing + +To contribute to this book, you will need a Github Account. + + diff --git a/src/intro.md b/src/intro.md index 5cc5e5b..8c89f05 100644 --- a/src/intro.md +++ b/src/intro.md @@ -1,3 +1,19 @@ # TLA+ Wiki intro -Welcome to TLA+ wiki. If you find errors, or have suggestions or feedback, please create a PR or an issue. +Welcome to TLA+ wiki. This wiki was created in response to the [2024 TLA+ community survey](http://discuss.tlapl.us/pdfW4MH5_0fKx.pdf). +More specifically, it aims to address the following feedbacks: + +1. **Difficulty Understanding Existing Codebase and Documentation**: Respondents note challenges in comprehending the existing codebase and documentation. The lack of clear structure and architecture documentation, as well as the complexity of the Java codebase, pose significant obstacles for newcomers. +2. **Navigation and Documentation**: Navigating the various TLA+ resources and finding relevant documentation is identified as a challenge. Respondents note scattered and sometimes non-existent documentation, making it difficult to find the most relevant resources and assistance. +3. Documentation and Tooling: There is a strong consensus on the need for improved documentation, particularly in the form of better organised and comprehensive resources. This includes better documentation for the entire project, better release cycles for all TLA+ tools, and centralised documentation on a website rather than PDFs. + + +The takeaway also sums up the mission of this wiki well: + +> **Streamlining Documentation**: There's a clear demand for better-organised documentation and centralised resources with a more modern interface to cater to users' preferences for accessible and comprehensive guidance. + + +This is a community-backed effort, so please if you find errors or suggestions/ideas/feedback, please create a PR or an issue. + +If you want to contribute, please check [Contributing](contributing.md) page with detailed step by step. The source of this website is hosted [here](https://github.com/FedericoPonzi/tlaplus-wiki/). + diff --git a/src/learning.md b/src/learning.md deleted file mode 100644 index ffdb276..0000000 --- a/src/learning.md +++ /dev/null @@ -1 +0,0 @@ -# Learning TLA+ diff --git a/src/learning/intro.md b/src/learning/intro.md new file mode 100644 index 0000000..3e5554b --- /dev/null +++ b/src/learning/intro.md @@ -0,0 +1,2 @@ +# Learning TLA+ and Model Checking + diff --git a/src/learning/tla-comparisons.md b/src/learning/tla-comparisons.md new file mode 100644 index 0000000..0fec2ad --- /dev/null +++ b/src/learning/tla-comparisons.md @@ -0,0 +1,2 @@ +# TLA+ Vs xxx +This page describes how does TLA+ compare to over specification and model checking tools.