6. Websites🔗

Verso's website genre is a static site generator. It contains two Verso Genres: Page and Post, which are identical except for their metadata:

def

Verso.Genre.Blog.Page : Genre
Verso.Genre.Blog.Page : Genre

An ordinary web page that is not a blog post.

def

Verso.Genre.Blog.Post : Genre
Verso.Genre.Blog.Post : Genre

A blog post.

Both feature the same set of extensions:

inductive type

Verso.Genre.Blog.BlockExt : Type
Verso.Genre.Blog.BlockExt : Type

The additional blocks available in pages and posts.

Constructors

highlightedCode (opts : Blog.CodeOpts)
  (highlighted : SubVerso.Highlighting.Highlighted) :
  Blog.BlockExt

Highlighted Lean code.

message (summarize : Bool)
  (msg : SubVerso.Highlighting.Highlighted.Message)
  (expandTraces : List Lean.Name) : Blog.BlockExt

Highlighted Lean messages.

lexedText (content : Blog.LexedText) : Blog.BlockExt

Lexed text, to be displayed with highlighted syntax.

htmlDiv (classes : String) : Blog.BlockExt

When rendered, the content is wrapped in a <div> with the given classes.

htmlWrapper (tag : String)
  (attributes : Array (String × String)) : Blog.BlockExt

When rendered, the content is wrapped in the specified HTML tag.

htmlDetails (classes : String) (summary : Output.Html) :
  Blog.BlockExt

When rendered, the content is wrapped in a <details> tag with the given summary.

blob (html : Output.Html) : Blog.BlockExt

A blob of HTML. The contents are discarded.

component (name : Lean.Name) (data : Lean.Json) :
  Blog.BlockExt

A reference to a component.

docstring (indent : Nat) (declName? : Option Lean.Name) :
  Blog.BlockExt

A Lean docstring that was indented indent spaces in the original source.

docstringSection (level : Nat) : Blog.BlockExt

A section in a Lean docstring.

Lean docstrings may contain nested headers, but they are not sections of the document as a whole. The contents of a docstring section are expected to be a paragraph that contains the section's title, followed by the actual content.

inductive type

Verso.Genre.Blog.InlineExt : Type
Verso.Genre.Blog.InlineExt : Type

The additional inline elements available in pages and posts.

Constructors

highlightedCode (opts : Blog.CodeOpts)
  (highlighted : SubVerso.Highlighting.Highlighted) :
  Blog.InlineExt

Highlighted Lean code.

message (msg : SubVerso.Highlighting.Highlighted.Message)
  (expandTraces : List Lean.Name) : Blog.InlineExt

Highlighted Lean messages.

lexedText (content : Blog.LexedText) : Blog.InlineExt

Lexed text, to be displayed with highlighted syntax.

customHighlight
  (highlighted : SubVerso.Highlighting.Highlighted) :
  Blog.InlineExt

Highlighted code that is not necessarily from Lean.

label (name : Lean.Name) : Blog.InlineExt

A label to serve as a cross-reference target.

ref (name : Lean.Name) : Blog.InlineExt

A reference to a label.

pageref (name : Lean.Name) (id? : Option String) :
  Blog.InlineExt

A reference to a page or post's internal name as a Lean value, to be shown as a link. If id? is some X, then the link is suffixed with #X.

htmlSpan (classes : String) : Blog.InlineExt

An HTML span element with the given classes.

blob (html : Output.Html) : Blog.InlineExt

A blob of HTML. The contents are discarded.

component (name : Lean.Name) (data : Lean.Json) :
  Blog.InlineExt

A reference to a component.

However, their metadata are different:

structure

Verso.Genre.Blog.Page.Meta : Type
Verso.Genre.Blog.Page.Meta : Type

The metadata used for non-blog-post pages

Constructor

Verso.Genre.Blog.Page.Meta.mk

Fields

showInNav : Bool

Whether to hide this page/part from navigation entries

htmlId : Option String

The HTML ID to assign to the header

structure

Verso.Genre.Blog.Post.Meta : Type
Verso.Genre.Blog.Post.Meta : Type

The metadata used for blog posts

Constructor

Verso.Genre.Blog.Post.Meta.mk

Fields

date : Blog.Date

The post's date. By default, this is used in the URL as well as included in the content.

authors : List String

The authors of the post

categories : List Post.Category

The categories in which to include the post

draft : Bool

If true, the post is not rendered by default

htmlId : Option String

The HTML ID to assign to the header

6.1. Generating a Site🔗

Blogs should have an executable that invokes blogMain on the appropriate site and theme, forwarding on command-line arguments. It is responsible for traversing the site and generating the HTML.

def

Verso.Genre.Blog.blogMain (theme : Blog.Theme) (site : Blog.Site)
  (linkTargets : Code.LinkTargets Blog.TraverseContext := { })
  (options : List String)
  (components : Blog.Components := by exact %registered_components)
  (header : String := Output.Html.doctype) : IO UInt32
Verso.Genre.Blog.blogMain
  (theme : Blog.Theme) (site : Blog.Site)
  (linkTargets :
    Code.LinkTargets
      Blog.TraverseContext :=
    { })
  (options : List String)
  (components : Blog.Components := by
    exact %registered_components)
  (header : String :=
    Output.Html.doctype) :
  IO UInt32

Generates the HTML for site.

Parameters:

theme is the theme used to render content.
site is the site to be generated.
options are the command-line options provided by a user.

Optional parameters:

linkTargets specifies how to create hyperlinks from Lean code to further documentation. By default, no links are generated.
components contains the implementation of the components. This is automatically filled out from a table.
header is emitted prior to each HTML document. By default, it produces a <doctype>, but it can be overridden to integrate with other static site generators.

6.2. Configuring a Site🔗

The URL layout of a site is specified via a Site:

inductive type

Verso.Genre.Blog.Site : Type
Verso.Genre.Blog.Site : Type

A specification of the layout of an entire site

Constructors

page (id : Lean.Name) (text : Part Page)
  (contents : Array Blog.Dir) : Blog.Site

The root of the site is a page

blog (id : Lean.Name) (text : Part Page)
  (contents : Array Blog.BlogPost) : Blog.Site

The root of the site is a blog with its associated posts

inductive type

Verso.Genre.Blog.Dir : Type
Verso.Genre.Blog.Dir : Type

A directory within the layout of a site.

Constructors

page (name : String) (id : Lean.Name) (text : Part Page)
  (contents : Array Blog.Dir) : Blog.Dir

The directory's root is the provided page

blog (name : String) (id : Lean.Name) (text : Part Page)
  (contents : Array Blog.BlogPost) : Blog.Dir

The directory's root is a blog

static (name : String) (files : System.FilePath) : Blog.Dir

The directory's root contains static files, copied from files when the site is generated

These are usually constructed using a small embedded configuration language.

A blog is rendered using a theme, which is a collection of templates. Templates are monadic functions that construct Html from a set of dynamically-typed parameters.

structure

Verso.Genre.Blog.Theme : Type
Verso.Genre.Blog.Theme : Type

A specification of how to render a site.

Constructor

Verso.Genre.Blog.Theme.mk

Fields

primaryTemplate : Blog.Template

The template used to render every page. It should construct an HTML value for the entire page, including the <html> element.

In the <head> element, it should invoke builtinHeader to ensure that the required dependencies are present and that Verso-specific initialization is performed.

In the body, it should check whether the parameter "posts" of type Html is present. If so, the page being rendered is a blog index, so it should place the parameter's value as a list of posts. If "categories" of type Post.Categories is present, it should render the contents as a category list.

The parameter "content" of type Html contains the content of the page. It should be placed accordingly in the result.

pageTemplate : Blog.Template

Pages are rendered using pageTemplate, with the result being passed in the "content" parameter to primaryTemplate. This template should use the "title" and "content" parameters to construct the contents of the page.

postTemplate : Blog.Template

Blog posts are rendered using pageTemplate, with the result being passed in the "content" parameter to primaryTemplate. This template should use the "title" and "content" parameters to construct the contents of the post. Additionally, the "metadata" template of type "Post.PartMetadata" may be present; if so, it can be used to render the author, date, and categories of the post.

archiveEntryTemplate : Blog.Template

The template used to summarize a blog post in a post archive. It receives the parameters "post", which contains the post, and "summary", which contains the HTML summary to display.

categoryTemplate : Blog.Template

The template used to display a category at the top of a category's post list. It receives one parameter, "category", which contains a Post.Category.

adHocTemplates : Array String → Option Blog.Template.Override

Customize the rendering of a given path by replacing the template and providing additional parameters

cssFiles : Array (String × String)

CSS files to be referenced in <head> and added to generated code.

jsFiles : Array (String × String × Bool)

JS files to be referenced in <head> or at the end of <body> and added to generated code.

def

Verso.Genre.Blog.Template : Type
Verso.Genre.Blog.Template : Type

A procedure for producing HTML from parameters. An abbreviation for TemplateM Html

def

Verso.Genre.Blog.TemplateM (α : Type) : Type
Verso.Genre.Blog.TemplateM (α : Type) :
  Type

A monad that provides template instantiation via dynamically-typed parameters.

def

Verso.Genre.Blog.Template.param {α : Type} [TypeName α] (key : String) :
  Blog.TemplateM α
Verso.Genre.Blog.Template.param {α : Type}
  [TypeName α] (key : String) :
  Blog.TemplateM α

Returns the value of the given template, if it exists. If it does not exist or if it exists but has the wrong type, an exception is thrown.

def

Verso.Genre.Blog.Template.param? {α : Type} [TypeName α]
  (key : String) : Blog.TemplateM (Option α)
Verso.Genre.Blog.Template.param?
  {α : Type} [TypeName α] (key : String) :
  Blog.TemplateM (Option α)

Returns the value of the given template, if it exists. If it exists but has the wrong type, an exception is thrown.

def

Verso.Genre.Blog.Template.builtinHeader : Blog.TemplateM Output.Html
Verso.Genre.Blog.Template.builtinHeader :
  Blog.TemplateM Output.Html

Contains the contents of <head> that are needed for proper functioning of the site.