Generated websites

[pdmosses]

Summary: A prototype of an enhanced agda-stdlib website has been generated: https://pdmosses.github.io/agda-stdlib/. Comments and suggestions for improvement are welcome!

The official agda-stdlib website at https://agda.github.io/agda-stdlib/ provides hyperlinked highlighted listings of all the library source files (and the accompanying README files). Each occurrence of a name in the web pages is linked to its declaration. A CI workflow action generates the website remotely, and deploys it to GitHub Pages whenever changes are pushed to the GitHub repository.

The official website is a valuable resource for browsing the library in ordinary web browsers (online or locally) without needing to download or install anything. Browsing the library online directly in GitHub is quite impractical, due to the difficulty of manually locating the declarations of referenced names.

In my view, however, the official library website currently has some significant deficiencies:

1. Search: Global textual search in the library is not supported.
2. Module navigation: The only support for navigating the module hierarchy is a huge flat list of module names. The deeply-nested hierarchy of modules makes it difficult to get an overview of the topmost levels.
3. Current module: Although hovering over a name shows the name of the module where the name is declared, the module name is not usually visible (except in the browser address bar) after clicking on the name and jumping to the declaration.
4. Scroll to top: It can be tedious to scroll to the top of a page (especially when browsing on a mobile device).
5. Dark mode: The pages are displayed with white background: it appears that switching the system appearance to dark does not affect the page rendering, and there is no toggle to switch to a dark background. Moreover, the highlighting palette used is unusable for dark backgrounds.
6. Version switching: The web pages do not display a menu for switching between different versions of the library.

I have generated a prototype of a library website that aims to address the above deficiencies:

1. Search: All pages provide access to global textual search. On larger displays, the search field is shown directly in the panel above the page content; on smaller displays, the field appears after clicking on an icon.
2. Module navigation: When browsing the library on larger displays, a navigation panel is shown on the left, displaying the top level of the library directory hierarchy; on smaller displays, the panel appears after clicking on an icon. Clicking on a directory name (or a > icon) in the navigation panel expands the name to display its next level; if the name is also a module name, the page shows the code of that module code.
3. Current module: On larger displays, the name of the module currently being browsed is highlighted in the navigation menu.
4. Scroll to top: If you start scrolling towards the top, a Back to top button appears at the top of the displayed code.
5. Dark mode: All pages provide a toggle to switch the current preference between light, dark, and automatic mode. The highlighting palette for dark mode is different from that used for light mode.
6. Version switching: All pages provide a version selector at the top.

A website generated from the gen-website branch of a fork of the agda/agda-stdlib repository has been published at https://pdmosses.github.io/agda-stdlib/. (Additional versions can easily be added.)

Comments and suggestions for improvement are welcome!

The styling of the generated websites can be customised, if desired, by adding CSS in a subdirectory of docs. The colors used for the light and dark highlighting can also be adjusted.

Generation process

The make commands used to generate the new website are explained in a section of the repository README file. The files added to support generation are the Makefile, mkdocs.yml, and the contents of the docs directory.

The standard Agda library does not currently contain any literate Agda files (although there is an open issue about that). The make  command used to generate the new website currently recognises only *.agda and *.lagda files. Literate prose is treated as plain text, and inserted verbatim in the web pages. However, the generated web page source files are actually Markdown, and Markdown markup in the prose is automatically rendered by the underlying website builder (MkDocs); it’s unclear whether that should be regarded as a bug or a feature… A cleaner approach would be to support *.lagda.md instead of *.lagda files – LaTeX math in Markdown is nicely rendered on webpages.

I have not yet tried to integrate the new website generation process into the workflow for releasing new versions of agda-stdlib and generating the official website. Currently, the new website is generated locally, and deployed by make commands based on mike.

Other websites generated from Agda libraries

• https://unimath.github.io/agda-unimath/
• https://martinescardo.github.io/TypeTopology/

There are also some websites generated from literate Agda sources that have significantly more structure than libraries:

• https://plfa.github.io/
• https://1lab.dev/
• https://hyrax.cbaberle.com/Hyrax/

[jamesmckinna]

@pdmosses My 👍 seems very weak by way of praise for the magnificent effort on display (sic) here.

I would be tempted to suggest adopting your approach as a drop-in replacement for our existing workflow (the gh-pages workflow is an additional, currently manual, step after release, and I have more than once unwittingly introduced inconsistencies into that process in the past), not least for your careful delineation 1-6 of existing UX characteristics ... and the corresponding deficiencies in our current setup, and the correspondingly careful way in which you have tackled each one here.

I further like that, in line with our existing minimal approach to documentation, that the pages themselves are largely unadorned, and I assume that issues around the use of Literate Agda/Markdown are largely (entirely) orthogonal to the basic architecture presented here. Moreover, such issues are more by way of policy rather than implementation, as well as the need for a consistent style to emerge if richer source input is to be accepted (I don't think that there is serious obstruction to doing so at this stage).

Beyond this, I'm not sure I'm (yet!?) competent to comment on the CI/YAML engineering involved here, so shoutouts to maintainers and users with greater experience here for comment.

[MatthewDaggitt]

This looks like a big improvement! If you did want to open a PR which integrated this into the workflow for the current release process, I would definitely be in favour of upgrading to this from the current website setup.

[martinescardo]

I would be interested in having this for TypeTopology!