The CSLib Website Sources

The CSLib website is built on a static site generator that uses Lean's documentation tooling as a backend. It is based on the source code of http://lean-lang.org.

The key files are:

• Lang.lean - the main source for cslib.io. This page maps web URLs to specific pages.
  • Lang/Components.lean - the implementation of website components, like screenshot galleries and buttons.
  • Lang/Pages/*.lean - the text of the various pages referred to from Lang.lean

Additional files that may be necessary to modify for larger updates are:

• deps/ - our copies of JavaScript and CSS libraries that we use
• static/ - static files to be hosted directly, including our CSS files

Finding the Content

To edit an existing page, take a look at either Lang.lean. Follow the page's address through the definition of the site structure until you discover a Lean module name.

Update Workflows

There are two main workflows for updating the site:

• GitHub-based: The code can be edited directly in GitHub, which then builds the modified site
• Local: The code can be checked out and edited on a personal computer

In both workflows, we modify both websites by creating a pull request to this repository. From the pull request, the modified version of the site can be previewed, and colleagues can suggest modifications or updates. When the pull request is merged, the updated site contents are automatically deployed and go live. The pull requests are also automatically checked for broken links.

GitHub-Based Updates

Once you find the page to be edited on GitHub, click the "Edit" button that resembles a pencil. GitHub provides documentation for the use of their online editor.

When the edit has been completed, create a new pull request.

Local Updates

Check out the repository, edit the files in question, and then create a PR.

Generating HTML

To build the sites, run

lake run generate

To automatically build upon file save, you can use a tool like entr:

git ls-files | entr -c lake run generate

Previewing the Sites

To preview the sites, run a local server with Verso's built-in server:

lake exe verso-serve _cslib.org

The rendered site is then available at http://localhost:8000/. Pass --port N to use a different port.

Troubleshooting

SubVerso versions

The CI requires that all subprojects used for example code have consistent SubVerso dependency versions. If they get out of sync, run update.sh to fix them.

Lake dependency detection

Lake may not detect all changes to certain files, such as static assets included via include_str or other indirect dependencies. If you make changes that don't seem to be reflected in the generated site, you may need to force a clean rebuild:

lake clean; lake build; lake run generate

Special Content

Some of our content is generated by Lean code to ensure consistent presentation.

Governance Page

On this page, each member is specified by the following data, in order:

• Picture file
• Name for display (this may contain HTML content, e.g. a link)
• Name for image alt text (for accessibility, may not contain HTML content)
• Title (no HTML content)

To add a team member, do the following:

1. Add their picture to static/team/
2. Add their information to one of the specific grounds in Pages/Team.lean

Publications page

The data model for publications is a bit more complicated, because there is a many-to-many relationship between authors and papers. To add a new publication:

1. Define the author. If they have a website, it goes in the second field of the Author datatype.
2. Add the paper to the pubs array, using the existing entries as a guide.