Don't use the the mdBook link preprocessor

docs/README.md

@@ -3,18 +3,20 @@
 The Apalache documentation is written in markdown files in the [./src](./src)
 directory and compiled using [mdbook](https://github.com/rust-lang/mdBook).
 
+To view the documentation, visit https://apalache.informal.systems/docs/ .
+
 ## Building and previewing the documentation
 
 To build the documentation into [../target/docs](../target/docs), run
 
-``` sh
+```sh
 mdbook build
 ```
 
 To start a server that will present a live updated view of the book while you
 edit, run
 
-``` sh
+```sh
 mdbook serve
 ```
 
@@ -30,15 +32,6 @@ Each chapter must link a file: internal links to anchors within files do not
 work. There is an [open issue](https://github.com/rust-lang/mdBook/issues/167)
 to fix this behavior.
 
-### Referring to `README.md` pages
-
-Within the book, any `README.md` page gets converted to an `index.md` page
-during compilation. You can link to `README.md` pages in the `SUMMARY.md`, but
-everywhere else you must write the link pointed towards `index.md`.
-
-There is an [open issue](https://github.com/rust-lang/mdBook/issues/1268) to fix
-this behavior.
-
 ## Internal documentation
 
 Design notes and memos that are part of the documentation of our design process

docs/book.toml

@@ -1,16 +1,19 @@
 [book]
-
 title = "Apalache Documentation"
 authors = ["Igor Konnov", "Jure Kukovec", "Andrey Kuprianov", "Shon Feder"]
 src = "src"
 language = "en"
 
-[build]
+[output.html]
+mathjax-support = true
+git-repository-url = "https://github.com/informalsystems/apalache"
 
+[build]
 build-dir = "../target/docs"
 # Don't create empty files when a chapter doesn't exist
 create-missing = false
+# Don't rename README.md to index.md
+use-default-preprocessors = false
 
-[output.html]
-mathjax-support = true
-git-repository-url = "https://github.com/informalsystems/apalache"
+# Do allow for file inclusion via {{ #include }}
+[preprocessor.links]

docs/src/SUMMARY.md

@@ -1,14 +1,14 @@
 # Summary
 
-[Overview](./README.md)
+[Overview](./index.md)
 
 # Apalache User Manual
 
-- [Introduction](./apalache/README.md)
+- [Introduction](./apalache/index.md)
 - [Getting Started](./apalache/getting-started.md)
     - [Shall I use Apalache or TLC?](./apalache/apalache-or-tlc.md)
     - [System Requirements](./apalache/system-reqs.md)
-    - [Installation](./apalache/installation/README.md)
+    - [Installation](./apalache/installation/index.md)
         - [Prebuilt Packages](./apalache/installation/jvm.md)
         - [Docker](./apalache/installation/docker.md)
         - [Source](./apalache/installation/source.md)
@@ -29,7 +29,7 @@
 
 # TLA+ Language Manual for Engineers
 
-- [Introduction](./lang/README.md)
+- [Introduction](./lang/index.md)
 - [The standard operators of TLA+](./lang/standard-operators.md)
     - [Booleans](./lang/booleans.md)
     - [Control And Nondeterminism](./lang/control-and-nondeterminism.md)
@@ -54,7 +54,7 @@
 
 # Idiomatic TLA+
 
-- [Introduction](./idiomatic/README.md)
+- [Introduction](./idiomatic/index.md)
 - [Keep state variables to the minimum](idiomatic/000keep-minimum-state-variables.md)
 - [Update state variables with assignments](idiomatic/001assignments.md)
 - [Apply primes only to state variables](idiomatic/002primes.md)