leanprover / leanprover/verso

Is it possible to make a blog with list of posts on frontpage

Open
#962 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Lean
Stars
384
Forks
124
Avg merge
22h 28m
Merged PRs (30d)
10

Description

I have only used medium and hugo before for creating a blog, but both have a home page (frontpage) with a list of the posts.
The current two examples in verso-templates both require a FrontPage, that does not contain the list of posts.

basic-blog:

def blog : Site := site Blog.FrontPage /
  "about" Blog.About
  "blog" Blog.Posts with
    Blog.Posts.FirstPost

blog-features:

def blog : Site := site Blog.FrontPage /
  static "static" ← "static_files"
  "about" Blog.About
  "blog" Blog.Posts with
    Blog.Posts.Comparison
    Blog.Posts.FibIter
    Blog.Posts.Welcome
    Blog.Posts.FirstPost

I tried to create a site without a frontpage, so I could have the posts be the main page:

def blog : Site := site BlogSrc.Posts with
  BlogSrc.Posts.FirstPost

lake build succeeds, but lake exe generate-blog, gives the following error:

No remote data configuration specified, and the default file ./verso-sources.json does not exist.
Generating post ./2025-1-1-first-post
Blog BlogSrc.Posts.«the canonical document object name» not found in traverse pass!
An error was encountered!
make: *** [generate] Error 1

Is there another way to have the posts be on the first page the user sees?

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start by comparing the basic-blog and blog-features examples in verso-templates, then reproduce the lake exe generate-blog failure with the BlogSrc.Posts front page. Trace how the site declaration and traverse pass handle the canonical document object, and identify the supported configuration needed for posts to appear at the site root; done means generation succeeds with the posts on the first page.

Written by the indexing model from the issue text.

Assessment

Domain
documentation
Issue type
Feature
Difficulty
4/5
Estimated time
3-5 days
Activity status
Quiet
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.