[BUG] links broken

[lemmy]

Links at the bottom of e.g. https://github.com/informalsystems/apalache/tree/unstable/docs/src are broken.

[shonfeder]

The markdown files are now used as the sources for the manual we build with mdBook: https://apalache.informal.systems/docs

As you can see, the links work in the manual.

Because of a shortcoming in mdBook (rust-lang/mdBook#984) we must choose between either letting the README.md files serve as landing pages when you open a directory in github or keeping links to README.md files working in both the raw markdown and the compiled end result. We have initially opted for the former, but maybe we should instead prefer the latter. We could preserve linking if we rename all README.md's in subdirs to index.md.

[konnov]

@lemmy, how did you reach these links? Both github pages and the README.md are pointing to the docs at apalache.informal.systems.

[lemmy]

My entry point was github.com/informalsystems/apalache. It's what I'm used to because of the issue tracker, commits, ...

[konnov]

There was one broken link in README.md, addressed in #498. It is a good question what to do, if the reader navigates directly to docs.

[shonfeder]

The readme of the docs directory currently makes it very clear that we compile the sources: https://github.com/informalsystems/apalache/tree/unstable/docs

I'll also add a link to compiled docs from there, and note that this is where one should go to read them.

My suggestion for linkability is that we rename all the README.md files to index.md files. This will work well for people who want to browse the source in their editors (me, for instance ;)), and will also work for people who want to use github interface,with the added bonus of making it clearer that that's not the recommended view port :)

[konnov]

So index.md will not be rendered by default? That makes sense.

[shonfeder]

index.md will still be rendered, we just won't have README.mds in most directories of the docs, or if we do, they won't be part of the docs properly (as a rule) but will be actual readme's for looking at the source.

I think this is better practice really, the other way is just jumping through unnecessary hoops to accommodate github's UI choices, and it's not needed any longer now that we are building and serving the docs in a more usable form.