Switch to Furo theme

[Halbaroth]

I dislike rtd theme we use for our sphinx documentation. This PR replaces it by Furo theme. This theme is more responsive.

[Halbaroth]

Uhm, strange. It seems that building failed but the dependencies are correctly installed and it works on my computer. I will investigate.

[bclement-ocp]

This is a visual documentation changes that needs visuals to be reviewed. Can you build the theme on your own GitHub Pages account and provide a link so that we can see what it looks like?

This should also allow to test the bit of JS code we have for multi-version support that may or may not need to be adapted to this new theme.

I would normally be a bit uncomfortable changing the documentation theme this way in a rush before the release, and think this should have been discussed more (I don't really like the ReadTheDoc theme we are using either, but I don't know that Furo is the one we want to use to replace it) beforehand. That said — we are already making changes to the structure of the documentation (splitting languages and models etc.), so it is better to bundle it with the visual change if possible, to make it a single user-visible change.

[Halbaroth]

Sure we should check. Besides your menu to switch between versions hasn't been pushed on latest and v2.5.4.

[Halbaroth]

The result: https://halbaroth.github.io/alt-ergo/next/
I didn't find a way to test it without pushing the PR on my next branch.

The menu is broken, I will fix it.

[Halbaroth]

I would normally be a bit uncomfortable changing the documentation theme this way in a rush before the release, and think this should have been discussed more (I don't really like the ReadTheDoc theme we are using either, but I don't know that Furo is the one we want to use to replace it) beforehand. That said — we are already making changes to the structure of the documentation (splitting languages and models etc.), so it is better to bundle it with the visual change if possible, to make it a single user-visible change.

I think there is no risk to change the theme before the release. This documentation is not a part of the opam package. If we ran into a problem just after the release, we can easily rollback to the previous theme.

[bclement-ocp]

Sure we should check. Besides your menu to switch between versions hasn't been pushed on latest and v2.5.4.

That's intentional because it would require back-porting the changes to v2.5.4 (but actually I can add the menu manually).

(Note that latest is just a symlink to whatever version is the latest)

[bclement-ocp]

After a quick look around — that looks better than ReadTheDocs but there seems to be some issues/glitches.

The sub-section headers are not rendered properly in the side bar

These should be sub-headers of the AB why3 plugin section otherwise it is confusing, see current

Tables look very ugly:

Maybe we have some custom CSS interfering? They look OK on the Furo demo

I have also noticed that we have some rendering glitches due to not setting properly the language on code blocks, but that is unrelated. I will do a pass to fix these.

[Halbaroth]

I have also noticed that we have some rendering glitches due to not setting properly the language on code blocks, but that is unrelated. I will do a pass to fix these.

Please do not. I did it ;)

[bclement-ocp]

I think there is no risk to change the theme before the release. This documentation is not a part of the opam package. If we ran into a problem just after the release, we can easily rollback to the previous theme.

The risk is in the perception by users. I hate it when projects change website looks left and right and find it disorienting, and so I'd like to minimize the changes we make to the website for released versions.

[Halbaroth]

The option navigation_depth is not supported yet by Furo: pradyunsg/furo#674
We have some workarounds or we can try another theme which supports this option.

[bclement-ocp]

sh is the lexer for (ba)sh scripts; console should be used for interactive sessions.

[bclement-ocp]

If we are fixing language for code blocks here there are also some on the "Model generation" page that use the default alt-ergo lexer but should use the smt-lib lexer instead.

[Halbaroth]

If we are fixing language for code blocks here there are also some on the "Model generation" page that use the default alt-ergo lexer but should use the smt-lib lexer instead.

I know but I already fix that in another PR.