lake update blueprint project

Stream: lean4

[Bjørn Kjos-Hanssen]

Usually when I have a working leanblueprint project and try to move it to a new version of Mathlib with lake update, the github action to build the project fails and I am tempted to start a whole new repo.
For example this reports an error associated with pip, "no such option: --global-option".

I'll try editing the .yml file accordingly, hopefully it works... not sure if best practice is to keep fixing old projects or starting a new one.

[Pietro Monticone]

I recommend using the LeanBlueprint CI template featuring the new ecosystem actions

[Pietro Monticone]

The following blueprint.yml should fix the issue:

name: Compile blueprint

on:
  push:
    branches:
      - main
  pull_request:
    branches:
      - main
  workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface

# Cancel previous runs if a new commit is pushed to the same PR or branch
concurrency:
  group: ${{ github.ref }}  # Group runs by the ref (branch or PR)
  cancel-in-progress: true  # Cancel any ongoing runs in the same group

# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
  contents: read          # Read access to repository contents
  pages: write            # Write access to GitHub Pages
  id-token: write         # Write access to ID tokens
  issues: write           # Write access to issues
  pull-requests: write    # Write access to pull requests

jobs:
  build_project:
    runs-on: ubuntu-latest
    name: Build project
    steps:
      - name: Cleanup to free disk space
        uses: jlumbroso/free-disk-space@main
        with:
          tool-cache: false
          android: true # saves approximately 12 GB
          dotnet: false
          haskell: false
          large-packages: false
          docker-images: false
          swap-storage: false

      - name: Checkout project
        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
        with:
          fetch-depth: 0 # Fetch all history for all branches and tags

      - name: Build the project
        uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0
        with:
          use-github-cache: false

      - name: Compile blueprint and documentation
        uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26
        with:
          blueprint: true
          homepage: home_page

[Bjørn Kjos-Hanssen]

Thanks @Pietro Monticone I'm giving it a try now.

[Pietro Monticone]

You need to remove doc-gen4 from the lakefile.toml requirements too:

name = "deontic"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["Deontic"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[require]]
name = "checkdecls"
git = "https://github.com/PatrickMassot/checkdecls.git"
-
- [[require]]
- name = "«doc-gen4»"
- git = "https://github.com/leanprover/doc-gen4"
- rev = "main"

[[lean_lib]]
name = "Deontic"

[Bjørn Kjos-Hanssen]

Your first version already worked actually.

[Pietro Monticone]

Yes, but it’s better for your next lake update to remove an unnecessary dependency from your project config file.

[Artie Khovanov]

hijacking but I am still on lakefile.lean
how do I update to lakefile.toml automatically?

[Pietro Monticone]

The command lake translate-config can be used to automatically convert between the two formats.

[Bjørn Kjos-Hanssen]

Artie Khovanov said:

hijacking but I am still on lakefile.lean
how do I update to lakefile.toml automatically?

Filing under questions I should have known to ask but never thought of