Merge remote-tracking branch 'upstream/main' into docgen-dump-docstrings

Author: david-christiansen

.github/workflows/ci.yml

@@ -196,7 +196,7 @@ jobs:
 
             - name: Upload docs to artifact storage
               if: github.ref_type != 'tag' && github.ref != 'refs/heads/main'
-              uses: actions/upload-artifact@v6
+              uses: actions/upload-artifact@v7
               with:
                   name: "Verso manual (PDF and HTML)"
                   path: |
@@ -235,7 +235,7 @@ jobs:
 
             - name: Upload HTML manual for PR deployment
               if: github.event_name == 'pull_request'
-              uses: actions/upload-artifact@v6
+              uses: actions/upload-artifact@v7
               with:
                   name: html-manual-for-deploy
                   path: _out/html-multi

.github/workflows/commit-convention.yml

@@ -0,0 +1,63 @@
+name: Check PR title follows commit convention
+
+on:
+    pull_request:
+        types: [opened, edited, reopened]
+    merge_group:
+
+jobs:
+    check-pr-title:
+        name: "PR title follows commit convention"
+        runs-on: ubuntu-latest
+        steps:
+            - name: Check PR title
+              uses: actions/github-script@v8
+              with:
+                  script: |
+                      let title;
+                      if (context.eventName === 'merge_group') {
+                          // The merge commit message's first line is the commit subject
+                          title = context.payload.merge_group.head_commit.message.split('\n')[0];
+                      } else {
+                          title = context.payload.pull_request.title;
+                      }
+
+                      const types = ['feat', 'fix', 'doc', 'style', 'refactor', 'test', 'chore', 'perf'];
+                      const typePattern = types.join('|');
+                      const regex = new RegExp(`^(${typePattern}): .+$`);
+
+                      const errors = [];
+
+                      if (!regex.test(title)) {
+                          errors.push(`PR title does not match the required format: \`<type>: <subject>\``);
+                          errors.push(`Allowed types: ${types.join(', ')}`);
+                          errors.push(`Example: \`fix: correct typo in documentation\``);
+                          errors.push(`Example: \`feat: add RSS feed support\``);
+                      } else {
+                          // Extract subject (part after ": ")
+                          const colonIndex = title.indexOf(': ');
+                          const subject = title.substring(colonIndex + 2);
+
+                          if (/^[A-Z]/.test(subject)) {
+                              errors.push(`Subject must not start with a capital letter: \`${subject}\``);
+                          }
+
+                          if (subject.endsWith('.')) {
+                              errors.push(`Subject must not end with a period: \`${subject}\``);
+                          }
+                      }
+
+                      if (errors.length > 0) {
+                          const message = [
+                              'PR title does not follow the commit convention.',
+                              '',
+                              `Title: \`${title}\``,
+                              '',
+                              ...errors.map(e => `- ${e}`),
+                              '',
+                              'Format: `<type>: <subject>`',
+                          ].join('\n');
+                          core.setFailed(message);
+                      } else {
+                          core.info(`PR title is valid: ${title}`);
+                      }

.github/workflows/pr-deploy.yml

@@ -26,7 +26,7 @@ jobs:
                   sourceRunId: ${{ github.event.workflow_run.id }}
 
             - name: Download HTML manual artifact
-              uses: dawidd6/action-download-artifact@v15
+              uses: dawidd6/action-download-artifact@v16
               with:
                   run_id: ${{ github.event.workflow_run.id }}
                   name: html-manual-for-deploy

doc/UsersGuide/Releases.lean

@@ -6,7 +6,7 @@ Author: Emilio J. Gallego Arias
 
 import VersoManual
 
-import UsersGuide.Releases.«v4_29_0_rc2»
+import UsersGuide.Releases.«v4_29_0»
 import UsersGuide.Releases.«v4_28_0»
 
 open Verso Genre Manual
@@ -27,5 +27,5 @@ Verso versioning follows Lean's.
 This means that we release a new version for each Lean release, usually once per month.
 In particular, note that Verso doesn't follow the [semantic versioning model](https://semver.org/).
 
-{include 0 UsersGuide.Releases.«v4_29_0_rc2»}
+{include 0 UsersGuide.Releases.«v4_29_0»}
 {include 0 UsersGuide.Releases.«v4_28_0»}

doc/UsersGuide/Releases/v4_29_0_rc2.lean doc/UsersGuide/Releases/v4_29_0.leandoc/UsersGuide/Releases/v4_29_0_rc2.lean renamed to doc/UsersGuide/Releases/v4_29_0.lean

@@ -11,10 +11,11 @@ open Verso.Genre
 -- To allow ```` below
 set_option linter.verso.markup.codeBlock false
 
-#doc (Manual) "Verso 4.29.0-rc2 (unreleased)" =>
+#doc (Manual) "Verso 4.29.0 (unreleased)" =>
 %%%
-tag := "release-v4.29.0-rc2"
-file := "v4.29.0-rc2"
+tag := "release-v4.29.0"
+file := "v4.29.0"
 %%%
 
-* [fix: Verso folding ranges / TOC for Lean.Doc syntax and #doc](https://github.com/leanprover/verso/pull/768)
+* Fix Verso folding ranges / TOC for Lean.Doc syntax and #doc (#768)
+* Align Blog inline Lean role naming with Manual; add `{lean}` and deprecate `{leanInline}` (#762)

lake-manifest.json

@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "361b8036c32b1cc18223b295c1e30bbd094688ad",
+   "rev": "3f5c2d5f84f7575a01b6d92916f4e914cefff51d",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc1
+leanprover/lean4:v4.29.0-rc2

src/tests/Tests/VersoBlog.lean

@@ -85,3 +85,23 @@ example : base = 40 := rfl
 ```lean post +error
 #check scratch
 ```
+
+-- Regression test for inline Lean role naming in Blog:
+-- canonical `{lean}` works without warnings.
+#docs (Post) inlineLeanRoleNames "Inline Lean Role Names" :=
+```leanInit post
+```
+
+Canonical role: {lean post}`Nat.succ 1`.
+
+/--
+warning: `{leanInline}` is deprecated; use `{lean}` instead.
+-/
+#docs (Post) inlineLeanRoleNamesDeprecated "Inline Lean Role Names (deprecated alias)" :=
+```leanInit post2
+```
+
+Legacy role: {leanInline post2}`Nat.succ 1`.
+
+#guard inlineLeanRoleNames.toPart.content.size > 0
+#guard inlineLeanRoleNamesDeprecated.toPart.content.size > 0

src/verso-blog/VersoBlog.lean

@@ -599,8 +599,7 @@ where
     modifyInfoState fun s => { s with trees := f s.trees }
 
 open SubVerso.Highlighting Highlighted in
-@[role]
-def leanInline : RoleExpanderOf LeanInlineConfig
+private def leanInlineImpl : RoleExpanderOf LeanInlineConfig
   | config, elts => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"lean block") <| do
     let #[code] := elts
       | throwError "Expected precisely one code element"
@@ -675,6 +674,19 @@ def leanInline : RoleExpanderOf LeanInlineConfig
 
       `(Inline.other (Blog.InlineExt.highlightedCode { contextName := $(quote config.exampleContext.getId) } $(quote hls)) #[Inline.code $(quote str.getString)])
 
+@[role lean]
+def leanCanonical : RoleExpanderOf LeanInlineConfig :=
+  leanInlineImpl
+
+@[role]
+def leanInline : RoleExpanderOf LeanInlineConfig
+  | config, elts => do
+    if h : 0 < elts.size then
+      logWarningAt elts[0] "`{leanInline}` is deprecated; use `{lean}` instead."
+    else
+      logWarning "`{leanInline}` is deprecated; use `{lean}` instead."
+    leanInlineImpl config elts
+
 open Lean.Elab.Tactic.GuardMsgs
 export WhitespaceMode (exact lax normalized)
 

src/verso-blog/VersoBlog/Component.lean

@@ -275,19 +275,21 @@ elab_rules : command
     let dirName := x.getId ++ `directive |> mkIdentFrom x
     let (toHtml?, other) ← splitToHtml contents
     let noJson ← argNames.mapM deJson
-    let arr : TSyntax `Lean.Parser.Term.doSeqItem ←
-      if !argNames.isEmpty then
-        `(Lean.Parser.Term.doSeqItem|
-          let .arr #[$(argNames.map (·.1)),*] := json
-            | HtmlT.logError s!"Expected array, got {json}"
-              return .empty)
-      else `(Lean.Parser.Term.doSeqItem|pure ())
     let toHtml ← toHtml?.mapM fun tm =>
-      `(Lean.Parser.Term.structInstField|
-        toHtml id json goI goB contents := do
-              $arr
-              $noJson*
-              ($tm id json goI goB contents))
+      if argNames.isEmpty then
+        `(Lean.Parser.Term.structInstField|
+          toHtml id json goI goB contents := do
+                ($tm id json goI goB contents))
+      else
+        `(Lean.Parser.Term.structInstField|
+          toHtml id json goI goB contents := do
+                match json with
+                | .arr #[$(argNames.map (·.1)),*] => do
+                  $noJson*
+                  ($tm id json goI goB contents)
+                | _ => do
+                  HtmlT.logError s!"Expected array, got {json}"
+                  return .empty)
     let other := toHtml.toArray ++ other
     let cmd2 ←
       `(command|
@@ -325,19 +327,21 @@ elab_rules : command
     let compName := x.getId ++ `comp |> mkIdentFrom x
     let (toHtml?, other) ← splitToHtml contents
     let noJson ← argNames.mapM deJson
-    let arr : TSyntax `Lean.Parser.Term.doSeqItem ←
-      if !argNames.isEmpty then
-        `(Lean.Parser.Term.doSeqItem|
-          let .arr #[$(argNames.map (·.1)),*] := json
-            | HtmlT.logError s!"Expected array, got {json}"
-              return .empty)
-      else `(Lean.Parser.Term.doSeqItem|pure ())
     let toHtml ← toHtml?.mapM fun tm =>
-      `(Lean.Parser.Term.structInstField|
-        toHtml id json goI contents := do
-              $arr
-              $noJson*
-              ($tm id json goI contents))
+      if argNames.isEmpty then
+        `(Lean.Parser.Term.structInstField|
+          toHtml id json goI contents := do
+                ($tm id json goI contents))
+      else
+        `(Lean.Parser.Term.structInstField|
+          toHtml id json goI contents := do
+                match json with
+                | .arr #[$(argNames.map (·.1)),*] => do
+                  $noJson*
+                  ($tm id json goI contents)
+                | _ => do
+                  HtmlT.logError s!"Expected array, got {json}"
+                  return .empty)
     let other := toHtml.toArray ++ other
     let cmd2 ←
       `(command|