Convert from AsciiDoctor to Material for MkDocs

[thatplguy]

This PR is an experiment in using Material for MkDocs to design a single, consolidated docs page – see this ticket for why I picked Material for MkDocs.

I've incorporated my progress on the language reference (in docs/reference) and accompanying general CN documentation (in docs/specifications), along with the structure of the CN tutorial (in docs/getting-started/tutorials) and the contents of the first tutorial section – porting from asciidoctor was pretty straightforward.

Here's what it looks like:

You can build and run it on localhost:8000 as follows:

# Install Material for MkDocs
pip install mkdocs-material

# In the cn-tutorial root directory, run
mkdocs serve

I'd like to hear your thoughts on:

1. Is it worth having a single documentation website that also contains the tutorial, or would you prefer the tutorial remain separate?
2. Should we use Material for MkDocs? Feel free to comment on this ticket as well. (If we decide to use something else, it won't be hard to shift the language reference content to a new platform.)
3. What do you think about the overall structure – does the top-level navigation make sense content-wise?
4. Thoughts on the language reference and spec documentation so far? There's more content to add, and @cp526 I'll probably be bugging you in the near future to help me understand the missing bits 🙂

[bcpierce00]

Is it worth having a single documentation website that also contains the tutorial, or would you prefer the tutorial remain separate?

The tutorial should definitely be integrated with other docs.

Should we use Material for MkDocs? Feel free to comment on https://github.com/GaloisInc/VERSE-Toolchain/issues/119 as well. (If we decide to use something else, it won't be hard to shift the language reference content to a new platform.)

Looks fine. (One little thing I notice is that the "include an example here" idiom is a bit verbose and requires writing the name of the file to include twice, which is not nice. This can obviously be solved by a little preprocessing, as we're doing now, but perhaps there's a cleaner fix.)

What do you think about the overall structure – does the top-level navigation make sense content-wise?

Haven't gone over it with a fine-tooth comb yet, but to a first approximation it looks pretty good.

We'll want to finalize and merge the new notation branch before converting the tutorial fully to this format.

[thatplguy]

Thanks @bcpierce00. Here's what I see as next steps:

1. @cp526 should take a look and veto/approve switching to mkdocs
2. Finalize and merge the new notation branch
3. Convert the tutorial to mkdocs on this branch (I can do this)
4. Finalize and merge this branch, and use mkdocs going forward

[cp526]

Since the naming conventions branch is now merged, we're no longer blocked on that here. I'm happy for us to go ahead with the Material on mkDocs scheme for the unified CN documentation.

[thatplguy]

Great, thank you @cp526!

[septract]

My PR #40 is not about the content of the tutorial but rather the CI setup around the Coq examples. So that should not block merging this once it's ready. The Coq stuff needs to be resolved but we're going to wait until the repo split (whenever that happens).

[thatplguy]

@cp526 @bcpierce00 this is ready to go. There are no semantic changes to the tutorial, but I did rearrange the structure so that each chapter is in a separate file.

Do you want to take a look before I merge this?

[cp526]

LGTM. @bcpierce00 ?

[bcpierce00]

I'm having trouble building... I guess it's a searchpath thing because mkdocs-material is installed...

make mkdir -p docs/exercises mkdir -p docs/solutions mkdocs build --strict Error: MkDocs encountered an error parsing the configuration file: while constructing a Python object cannot find module 'material.extensions.emoji' (No module named 'material') in "/Users/bcpierce/bcp24work/projects/verse/cn-tutorial/mkdocs.yml", line 68, column 24

pip3 install mkdocs-material Defaulting to user installation because normal site-packages is not writeable Requirement already satisfied: mkdocs-material in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (9.5.43) Requirement already satisfied: babel~=2.10 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (2.16.0) Requirement already satisfied: colorama~=0.4 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (0.4.6) Requirement already satisfied: jinja2~=3.0 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (3.1.4) Requirement already satisfied: markdown~=3.2 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (3.7) Requirement already satisfied: mkdocs-material-extensions~=1.3 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (1.3.1) Requirement already satisfied: mkdocs~=1.6 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (1.6.1) Requirement already satisfied: paginate~=0.5 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (0.5.7) Requirement already satisfied: pygments~=2.16 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (2.18.0) Requirement already satisfied: pymdown-extensions~=10.2 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (10.12) Requirement already satisfied: regex>=2022.4 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (2024.9.11) Requirement already satisfied: requests~=2.26 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-material) (2.32.3) Requirement already satisfied: MarkupSafe>=2.0 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from jinja2~=3.0->mkdocs-material) (3.0.2) Requirement already satisfied: importlib-metadata>=4.4 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from markdown~=3.2->mkdocs-material) (8.5.0) Requirement already satisfied: click>=7.0 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs~=1.6->mkdocs-material) (8.1.7) Requirement already satisfied: ghp-import>=1.0 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs~=1.6->mkdocs-material) (2.1.0) Requirement already satisfied: mergedeep>=1.3.4 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs~=1.6->mkdocs-material) (1.3.4) Requirement already satisfied: mkdocs-get-deps>=0.2.0 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs~=1.6->mkdocs-material) (0.2.0) Requirement already satisfied: packaging>=20.5 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs~=1.6->mkdocs-material) (24.1) Requirement already satisfied: pathspec>=0.11.1 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs~=1.6->mkdocs-material) (0.12.1) Requirement already satisfied: pyyaml-env-tag>=0.1 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs~=1.6->mkdocs-material) (0.1) Requirement already satisfied: pyyaml>=5.1 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs~=1.6->mkdocs-material) (6.0.2) Requirement already satisfied: watchdog>=2.0 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs~=1.6->mkdocs-material) (6.0.0) Requirement already satisfied: charset-normalizer<4,>=2 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from requests~=2.26->mkdocs-material) (3.4.0) Requirement already satisfied: idna<4,>=2.5 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from requests~=2.26->mkdocs-material) (3.10) Requirement already satisfied: urllib3<3,>=1.21.1 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from requests~=2.26->mkdocs-material) (2.2.3) Requirement already satisfied: certifi>=2017.4.17 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from requests~=2.26->mkdocs-material) (2024.8.30) Requirement already satisfied: python-dateutil>=2.8.1 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from ghp-import>=1.0->mkdocs~=1.6->mkdocs-material) (2.9.0.post0) Requirement already satisfied: zipp>=3.20 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from importlib-metadata>=4.4->markdown~=3.2->mkdocs-material) (3.20.2) Requirement already satisfied: platformdirs>=2.2.0 in /Users/bcpierce/Library/Python/3.9/lib/python/site-packages (from mkdocs-get-deps>=0.2.0->mkdocs~=1.6->mkdocs-material) (4.3.6) Requirement already satisfied: six>=1.5 in /Applications/Xcode.app/Contents/Developer/Library/Frameworks/Python3.framework/Versions/3.9/lib/python3.9/site-packages (from python-dateutil>=2.8.1->ghp-import>=1.0->mkdocs~=1.6->mkdocs-material) (1.15.0)

On Fri, Nov 1, 2024 at 6:53 AM Christopher Pulte @.***> wrote:

LGTM. @bcpierce00 https://urldefense.com/v3/__https://github.com/bcpierce00__;!!IBzWLUs!WresZoGbmiRA4xNlnNOmjKtL4LCzi5ixKR94-uMKXfyoSbw8u5ld01gMmKTa1smX3RmKBQLwNHq8Q6Uqx0wtSWirDkJO$ ?

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/pull/80*issuecomment-2451686615__;Iw!!IBzWLUs!WresZoGbmiRA4xNlnNOmjKtL4LCzi5ixKR94-uMKXfyoSbw8u5ld01gMmKTa1smX3RmKBQLwNHq8Q6Uqx0wtSaKGTmch$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQCZE5Z4QMJU6YPHBOPTZ6NMS7AVCNFSM6AAAAABM7NTJ2SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINJRGY4DMNRRGU__;!!IBzWLUs!WresZoGbmiRA4xNlnNOmjKtL4LCzi5ixKR94-uMKXfyoSbw8u5ld01gMmKTa1smX3RmKBQLwNHq8Q6Uqx0wtSQJCpBCu$ . You are receiving this because you were mentioned.Message ID: @.***>

[bcpierce00]

OK, I can build it now, and I agree from a bit of spot-checking that it looks pretty good. I'm fine with merging.

I do have a few questions though about what's included in the layout -- in particular, I don't understand what's included in the sidebars...

In the main text area, the headers are Specifications, Special comments, and Kinds of Specs. But the second and third of these don't appear in the list on the left. What does appear on the left is what seem to be subheaders in the main text, but there are some on the left that do not seem to appear in the main text. So... what goes on the left, what goes on the right, what goes both and what goes neither?

[thatplguy]

The top and sidebars are defined in mkdocs.yaml (the nav key at the bottom) and are defined independently from what appears in the main text. Top menu bar items are the outermost level, followed by the left sidebar. The right sidebar is the table of contents for the page being viewed. In this case, that's where "Special comments" and "Kinds of specs" appear.

Here's an example.

nav:
  - Getting started:                                # Top menu item 1
    - README.md                                     # Default page shown when "Getting started"
                                                    # menu item is clicked
    - Installation: getting-started/installation.md # Left menu item 1
    - "Hello world": getting-started/hello-world.md # Left menu item 2
    - Tutorials:                                    # Left menu group heading (bolded)
      - getting-started/tutorials/README.md         # Default page shown when "Tutorials" is clicked
      - "Basic usage": getting-started/tutorials/basic-usage.md
  - Specifications:                                 # Top menu item 2

[bcpierce00]

OK, I see -- it makes more sense now.

One thing that would have helped me would be to adjust the fonts a bit on the left-hand side -- make the "Getting Started" at the top left larger than the boldface headers below it (which should themselves, IMO, be a bit larger than the other text there).