chore: use Verso's new lightweight literate programming support#473
chore: use Verso's new lightweight literate programming support#473teorth merged 3 commits intoteorth:mainfrom
Conversation
|
I recognize that this is a major change, and I'm very willing to work with you to make sure that it meets your needs. |
This pull request replaces the custom website generation code with Verso's new lightweight literate programming feature. The main visible differences are: * The site looks a bit different, but the structure is the same * The build process is greatly simplified. Instead of having two internal projects on different Lean versions and a build system that orchestrates them, there is a single project that merely has an extra Verso dependency, with a TOML file to configure things like custom chapter titles. * GitHub Actions is set to use lean-action, which handles the Mathlib cache. * The whole site builds much more quickly. * Verso's integrated search feature is used. It allows searching the both the names of definitions and the text itself, with full-text search using a standard heuristic word stemming system so e.g. searching for "preference" also yields results for "prefers". * Docstrings are all written in Verso. Verso is mostly like Markdown, but it allows you to annotate code snippets that explain whether they're a tactic name, a Lean term, etc. This means you get red squigglies in your IDE for typos, instead of having view the rendered result to find out. It also means that everything is accurately highlighted, so the tactic `intro` is kept separate from the constructor `True.intro`. One thing that this literate programming system does not yet do is integrate with doc-gen. The code that this site is replacing had this integration. As I understand it, this integration was to enable search, so I think the built-in Verso search makes that unnecessary. If there are further use cases that I'm not aware of, please let me know and I'll see what I can do.
david-christiansen
force-pushed
the
easy-literate
branch
from
b8c81b1 to
8e91471
Compare
|
Live version from my repo for review purposes (built from commit 55d5089): https://pimotte.github.io/analysis-ci |
There was a problem hiding this comment.
OOC, where these files moved?
There was a problem hiding this comment.
The build process is greatly simplified. Instead of having two internal projects on different Lean versions and a build system that orchestrates them, there is a single project that merely has an extra Verso dependency, with a TOML file to configure things like custom chapter titles.
I guess this explains it. The whole project is flattened a bit, which is a good thing IMO.
There was a problem hiding this comment.
That's right. The native Verso feature replaces the contents of book, so the contents of analysis all went up by one level to the repository root.
4 participants
This pull request replaces the custom website generation code with Verso's new lightweight literate programming feature.
The main visible differences are:
The site looks a bit different, but the structure is the same
The build process is greatly simplified. Instead of having two internal projects on different Lean versions and a build system that orchestrates them, there is a single project that merely has an extra Verso dependency, with a TOML file to configure things like custom chapter titles.
GitHub Actions is set to use lean-action, which handles the Mathlib cache.
The whole site builds much more quickly.
Verso's integrated search feature is used. It allows searching the both the names of definitions and the text itself, with full-text search using a standard heuristic word stemming system so e.g. searching for "preference" also yields results for "prefers".
Docstrings are all written in Verso. Verso is mostly like Markdown, but it allows you to annotate code snippets that explain whether they're a tactic name, a Lean term, etc. This means you get red squigglies in your IDE for typos, instead of having view the rendered result to find out. It also means that everything is accurately highlighted, so the tactic
introis kept separate from the constructorTrue.intro.One thing that this literate programming system does not yet do is integrate with doc-gen. The code that this site is replacing had this integration. As I understand, it served two purposes: search and getting readers used to the tool. Now that search is integrated, it still needs to be there to build familiarity. This understanding is based on a Zulip discussion. Even though it's included, identifiers do not link to it and it's not in the navigation bar. I did, however, add a link to it to the landing page. Is that sufficient? Do we need a new upstream feature?