From fc3fc594f84cbe31523f09e77e3bb2c0765e2195 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 6 Nov 2026 14:52:52 +0100 Subject: [PATCH] fix: make the header tag linter respond to edits after a header Before, adding a tag to a header could leave the header with an obsolete linter message until an edit caused re-elaboration. Now, it notices and removes it correctly. No-Changelog: bug fix --- README.md | 5 +- doc/UsersGuide/Basic.lean | 1 + .../Entries/BlogExampleSubprojects.lean | 2 + .../Releases/Entries/BlogLeanRole.lean | 2 + doc/UsersGuide/Releases/Entries/BuildLog.lean | 2 + .../Releases/Entries/CodeColorVariables.lean | 2 + .../Releases/Entries/DevelopmentServer.lean | 2 + doc/UsersGuide/Releases/Entries/Diagrams.lean | 2 + .../Releases/Entries/DocSourceRanges.lean | 2 + .../Entries/DocstringLabeledGroups.lean | 2 + .../ExtensionDescriptorVisibility.lean | 2 + .../Releases/Entries/ExtraStep.lean | 2 + .../Releases/Entries/FoldingRanges.lean | 2 + .../Releases/Entries/FullPageSearch.lean | 2 + .../Releases/Entries/HeadingIds.lean | 2 + .../Entries/InlineLeanElaboration.lean | 2 + .../Releases/Entries/InlineLeanInfoview.lean | 2 + doc/UsersGuide/Releases/Entries/LeanHtml.lean | 2 + .../Releases/Entries/LegacyInlineRoles.lean | 2 + .../Entries/LinkFootnoteResolution.lean | 2 + .../Releases/Entries/LiterateHtmlKatex.lean | 2 + .../Releases/Entries/LiterateProgramming.lean | 2 + .../Releases/Entries/ManualMarginalia.lean | 2 + .../Releases/Entries/MethodInMultiVerso.lean | 2 + .../Releases/Entries/ReleaseNotesChapter.lean | 2 + .../Releases/Entries/RoleDiagnostics.lean | 2 + .../Releases/Entries/SearchPriority.lean | 2 + .../Releases/Entries/SubprojectRefactor.lean | 2 + .../Releases/Entries/TeXBlockParagraphs.lean | 2 + .../Releases/Entries/TestFramework.lean | 2 + .../Releases/Entries/TestWidget.lean | 2 + .../Releases/Entries/UpstreamParser.lean | 2 + .../Entries/VersionedReleaseNotes.lean | 2 + .../Releases/Entries/VersoMainInterpret.lean | 2 + src/tests/VersoTests/Linters.lean | 130 ++++++ .../VersoTests/VersoManual/HeaderTags.lean | 143 +++++++ .../test-cases/header_tag_action.lean | 17 + .../header_tag_action.lean.expected.out | 106 +++++ .../header_tag_action_other_line.lean | 21 + ...er_tag_action_other_line.lean.expected.out | 30 ++ .../header_tag_metadata_action.lean | 19 + ...ader_tag_metadata_action.lean.expected.out | 110 +++++ .../test-cases/header_tag_title_action.lean | 15 + .../header_tag_title_action.lean.expected.out | 104 +++++ src/verso-manual/VersoManual/Linters.lean | 378 ++++++++++++------ 45 files changed, 1022 insertions(+), 121 deletions(-) create mode 100644 src/tests/VersoTests/VersoManual/HeaderTags.lean create mode 100644 src/tests/interactive/test-cases/header_tag_action.lean create mode 100644 src/tests/interactive/test-cases/header_tag_action.lean.expected.out create mode 100644 src/tests/interactive/test-cases/header_tag_action_other_line.lean create mode 100644 src/tests/interactive/test-cases/header_tag_action_other_line.lean.expected.out create mode 100644 src/tests/interactive/test-cases/header_tag_metadata_action.lean create mode 100644 src/tests/interactive/test-cases/header_tag_metadata_action.lean.expected.out create mode 100644 src/tests/interactive/test-cases/header_tag_title_action.lean create mode 100644 src/tests/interactive/test-cases/header_tag_title_action.lean.expected.out diff --git a/README.md b/README.md index 5998f025d..a43bccc19 100644 --- a/README.md +++ b/README.md @@ -130,6 +130,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 34, 0⟩ breaking := false @@ -142,7 +144,8 @@ Added a development server for previewing generated HTML locally. ``` Every entry module declares a `release_note` alongside its `#doc` to -associate extra metadata with the description. +associate extra metadata with the description. The entry's tag is +given by `release_note`, so the header tag linter is switched off. The version should be the one currently under development. When `lean-toolchain` names a stable release, that release is already diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index b22cab944..8cd1ccd5e 100644 --- a/doc/UsersGuide/Basic.lean +++ b/doc/UsersGuide/Basic.lean @@ -21,6 +21,7 @@ set_option pp.rawOnError true #doc (Manual) "Writing Documentation in Lean with Verso" => %%% +tag := "verso" shortTitle := "Documentation with Verso" authors := ["David Thrane Christiansen"] %%% diff --git a/doc/UsersGuide/Releases/Entries/BlogExampleSubprojects.lean b/doc/UsersGuide/Releases/Entries/BlogExampleSubprojects.lean index 907576b75..3bee10f00 100644 --- a/doc/UsersGuide/Releases/Entries/BlogExampleSubprojects.lean +++ b/doc/UsersGuide/Releases/Entries/BlogExampleSubprojects.lean @@ -10,6 +10,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases open Verso.Code.External +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 35, 0⟩ breaking := true diff --git a/doc/UsersGuide/Releases/Entries/BlogLeanRole.lean b/doc/UsersGuide/Releases/Entries/BlogLeanRole.lean index e6bbcfbdf..c75604821 100644 --- a/doc/UsersGuide/Releases/Entries/BlogLeanRole.lean +++ b/doc/UsersGuide/Releases/Entries/BlogLeanRole.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 29, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/BuildLog.lean b/doc/UsersGuide/Releases/Entries/BuildLog.lean index c4426b5e5..1d8b86af3 100644 --- a/doc/UsersGuide/Releases/Entries/BuildLog.lean +++ b/doc/UsersGuide/Releases/Entries/BuildLog.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 31, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/CodeColorVariables.lean b/doc/UsersGuide/Releases/Entries/CodeColorVariables.lean index f0ef49365..d23f89b24 100644 --- a/doc/UsersGuide/Releases/Entries/CodeColorVariables.lean +++ b/doc/UsersGuide/Releases/Entries/CodeColorVariables.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 34, 0⟩ breaking := true diff --git a/doc/UsersGuide/Releases/Entries/DevelopmentServer.lean b/doc/UsersGuide/Releases/Entries/DevelopmentServer.lean index 60bfd3b96..057d150f5 100644 --- a/doc/UsersGuide/Releases/Entries/DevelopmentServer.lean +++ b/doc/UsersGuide/Releases/Entries/DevelopmentServer.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 33, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/Diagrams.lean b/doc/UsersGuide/Releases/Entries/Diagrams.lean index 4b3982bf7..bac2d6e5f 100644 --- a/doc/UsersGuide/Releases/Entries/Diagrams.lean +++ b/doc/UsersGuide/Releases/Entries/Diagrams.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 30, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/DocSourceRanges.lean b/doc/UsersGuide/Releases/Entries/DocSourceRanges.lean index 8b03f01c7..3ede4dac9 100644 --- a/doc/UsersGuide/Releases/Entries/DocSourceRanges.lean +++ b/doc/UsersGuide/Releases/Entries/DocSourceRanges.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 31, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/DocstringLabeledGroups.lean b/doc/UsersGuide/Releases/Entries/DocstringLabeledGroups.lean index 4c14ae2f9..17c4fed36 100644 --- a/doc/UsersGuide/Releases/Entries/DocstringLabeledGroups.lean +++ b/doc/UsersGuide/Releases/Entries/DocstringLabeledGroups.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 32, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/ExtensionDescriptorVisibility.lean b/doc/UsersGuide/Releases/Entries/ExtensionDescriptorVisibility.lean index 74c0d02ed..35b623ec2 100644 --- a/doc/UsersGuide/Releases/Entries/ExtensionDescriptorVisibility.lean +++ b/doc/UsersGuide/Releases/Entries/ExtensionDescriptorVisibility.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 32, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/ExtraStep.lean b/doc/UsersGuide/Releases/Entries/ExtraStep.lean index f09b01be8..f47a07e7d 100644 --- a/doc/UsersGuide/Releases/Entries/ExtraStep.lean +++ b/doc/UsersGuide/Releases/Entries/ExtraStep.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 31, 0⟩ breaking := true diff --git a/doc/UsersGuide/Releases/Entries/FoldingRanges.lean b/doc/UsersGuide/Releases/Entries/FoldingRanges.lean index 9f80c2779..5c2b01797 100644 --- a/doc/UsersGuide/Releases/Entries/FoldingRanges.lean +++ b/doc/UsersGuide/Releases/Entries/FoldingRanges.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 29, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/FullPageSearch.lean b/doc/UsersGuide/Releases/Entries/FullPageSearch.lean index d87d9f8b9..05c43b370 100644 --- a/doc/UsersGuide/Releases/Entries/FullPageSearch.lean +++ b/doc/UsersGuide/Releases/Entries/FullPageSearch.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 30, 0⟩ breaking := true diff --git a/doc/UsersGuide/Releases/Entries/HeadingIds.lean b/doc/UsersGuide/Releases/Entries/HeadingIds.lean index 4440b0c21..3b5dc3172 100644 --- a/doc/UsersGuide/Releases/Entries/HeadingIds.lean +++ b/doc/UsersGuide/Releases/Entries/HeadingIds.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 36, 0⟩ breaking := true diff --git a/doc/UsersGuide/Releases/Entries/InlineLeanElaboration.lean b/doc/UsersGuide/Releases/Entries/InlineLeanElaboration.lean index da439740d..aa0699f42 100644 --- a/doc/UsersGuide/Releases/Entries/InlineLeanElaboration.lean +++ b/doc/UsersGuide/Releases/Entries/InlineLeanElaboration.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 36, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/InlineLeanInfoview.lean b/doc/UsersGuide/Releases/Entries/InlineLeanInfoview.lean index bf92f1abb..73f6a3fb9 100644 --- a/doc/UsersGuide/Releases/Entries/InlineLeanInfoview.lean +++ b/doc/UsersGuide/Releases/Entries/InlineLeanInfoview.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 28, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/LeanHtml.lean b/doc/UsersGuide/Releases/Entries/LeanHtml.lean index 02c941312..04e473254 100644 --- a/doc/UsersGuide/Releases/Entries/LeanHtml.lean +++ b/doc/UsersGuide/Releases/Entries/LeanHtml.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 36, 0⟩ breaking := true diff --git a/doc/UsersGuide/Releases/Entries/LegacyInlineRoles.lean b/doc/UsersGuide/Releases/Entries/LegacyInlineRoles.lean index 4d9e87165..66130560d 100644 --- a/doc/UsersGuide/Releases/Entries/LegacyInlineRoles.lean +++ b/doc/UsersGuide/Releases/Entries/LegacyInlineRoles.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 31, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/LinkFootnoteResolution.lean b/doc/UsersGuide/Releases/Entries/LinkFootnoteResolution.lean index 76f8bb78d..02ae39f28 100644 --- a/doc/UsersGuide/Releases/Entries/LinkFootnoteResolution.lean +++ b/doc/UsersGuide/Releases/Entries/LinkFootnoteResolution.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 35, 0⟩ breaking := true diff --git a/doc/UsersGuide/Releases/Entries/LiterateHtmlKatex.lean b/doc/UsersGuide/Releases/Entries/LiterateHtmlKatex.lean index 4573d8043..7e4ceb16e 100644 --- a/doc/UsersGuide/Releases/Entries/LiterateHtmlKatex.lean +++ b/doc/UsersGuide/Releases/Entries/LiterateHtmlKatex.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 32, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/LiterateProgramming.lean b/doc/UsersGuide/Releases/Entries/LiterateProgramming.lean index 5e9496c0b..1397d11c3 100644 --- a/doc/UsersGuide/Releases/Entries/LiterateProgramming.lean +++ b/doc/UsersGuide/Releases/Entries/LiterateProgramming.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 29, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/ManualMarginalia.lean b/doc/UsersGuide/Releases/Entries/ManualMarginalia.lean index ae259403e..d8035dfc0 100644 --- a/doc/UsersGuide/Releases/Entries/ManualMarginalia.lean +++ b/doc/UsersGuide/Releases/Entries/ManualMarginalia.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 35, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/MethodInMultiVerso.lean b/doc/UsersGuide/Releases/Entries/MethodInMultiVerso.lean index ae08b3f3f..eb700509d 100644 --- a/doc/UsersGuide/Releases/Entries/MethodInMultiVerso.lean +++ b/doc/UsersGuide/Releases/Entries/MethodInMultiVerso.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 32, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/ReleaseNotesChapter.lean b/doc/UsersGuide/Releases/Entries/ReleaseNotesChapter.lean index c1a36f02f..60cf518f5 100644 --- a/doc/UsersGuide/Releases/Entries/ReleaseNotesChapter.lean +++ b/doc/UsersGuide/Releases/Entries/ReleaseNotesChapter.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 28, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/RoleDiagnostics.lean b/doc/UsersGuide/Releases/Entries/RoleDiagnostics.lean index b507197c5..fe8304321 100644 --- a/doc/UsersGuide/Releases/Entries/RoleDiagnostics.lean +++ b/doc/UsersGuide/Releases/Entries/RoleDiagnostics.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 31, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/SearchPriority.lean b/doc/UsersGuide/Releases/Entries/SearchPriority.lean index 7cb8adba8..c2e5be053 100644 --- a/doc/UsersGuide/Releases/Entries/SearchPriority.lean +++ b/doc/UsersGuide/Releases/Entries/SearchPriority.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 30, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/SubprojectRefactor.lean b/doc/UsersGuide/Releases/Entries/SubprojectRefactor.lean index 6fd50f21a..610d4e0fc 100644 --- a/doc/UsersGuide/Releases/Entries/SubprojectRefactor.lean +++ b/doc/UsersGuide/Releases/Entries/SubprojectRefactor.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 36, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/TeXBlockParagraphs.lean b/doc/UsersGuide/Releases/Entries/TeXBlockParagraphs.lean index 5ef40fc50..1c435874b 100644 --- a/doc/UsersGuide/Releases/Entries/TeXBlockParagraphs.lean +++ b/doc/UsersGuide/Releases/Entries/TeXBlockParagraphs.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 36, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/TestFramework.lean b/doc/UsersGuide/Releases/Entries/TestFramework.lean index 92c744e7c..4050daede 100644 --- a/doc/UsersGuide/Releases/Entries/TestFramework.lean +++ b/doc/UsersGuide/Releases/Entries/TestFramework.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 34, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/TestWidget.lean b/doc/UsersGuide/Releases/Entries/TestWidget.lean index 84bed74b2..7fd80467f 100644 --- a/doc/UsersGuide/Releases/Entries/TestWidget.lean +++ b/doc/UsersGuide/Releases/Entries/TestWidget.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 35, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/UpstreamParser.lean b/doc/UsersGuide/Releases/Entries/UpstreamParser.lean index f8f73100e..7142f4146 100644 --- a/doc/UsersGuide/Releases/Entries/UpstreamParser.lean +++ b/doc/UsersGuide/Releases/Entries/UpstreamParser.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 36, 0⟩ breaking := true diff --git a/doc/UsersGuide/Releases/Entries/VersionedReleaseNotes.lean b/doc/UsersGuide/Releases/Entries/VersionedReleaseNotes.lean index 4ecbdbea2..670974d9a 100644 --- a/doc/UsersGuide/Releases/Entries/VersionedReleaseNotes.lean +++ b/doc/UsersGuide/Releases/Entries/VersionedReleaseNotes.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 34, 0⟩ breaking := false diff --git a/doc/UsersGuide/Releases/Entries/VersoMainInterpret.lean b/doc/UsersGuide/Releases/Entries/VersoMainInterpret.lean index 9584d4060..6b9bcca33 100644 --- a/doc/UsersGuide/Releases/Entries/VersoMainInterpret.lean +++ b/doc/UsersGuide/Releases/Entries/VersoMainInterpret.lean @@ -9,6 +9,8 @@ public import UsersGuide.Releases.Entry open Verso.Genre Manual InlineLean UsersGuide.Releases +set_option linter.verso.manual.headerTags false + release_note version := ⟨4, 36, 0⟩ breaking := false diff --git a/src/tests/VersoTests/Linters.lean b/src/tests/VersoTests/Linters.lean index 5bd1de950..63ef44aaa 100644 --- a/src/tests/VersoTests/Linters.lean +++ b/src/tests/VersoTests/Linters.lean @@ -289,6 +289,136 @@ set_option linter.verso.manual.headerTags true in #docs (Verso.Genre.Manual) headerTagsOn "Header tags on" := ::::::: +%%% +tag := "header-tags-on" +%%% + +# Untagged section + +Some text. + +::::::: + +/-! +A header that is followed by a metadata block without a `tag` field produces a warning whose hint +adds the field to that metadata block. +-/ +/-- +warning: Missing permalink tag + +Hint: Add a tag to the metadata block or explicitly indicate that no tag is desired: + • # Untagged section + %%% + t̲a̲g̲ ̲:̲=̲ ̲"̲u̲n̲t̲a̲g̲g̲e̲d̲-̲s̲e̲c̲t̲i̲o̲n̲"̲ + ̲number := false + %%% + • # Untagged section + %%% + t̲a̲g̲ ̲:̲=̲ ̲n̲o̲n̲e̲ + ̲number := false + %%% + +Note: The tag is used as a permanent name for the section or chapter. Writers of this or other documents may use it to link to the section, and it is used to share permanent links. In HTML content, they are used as IDs for headers. Section tags should remain unchanged over time. + +Note: This linter can be disabled with `set_option linter.verso.manual.headerTags false` +-/ +#test_msgs in +set_option linter.verso.manual.headerTags true in +#docs (Verso.Genre.Manual) headerTagsNoTagField "Header tags without a tag field" := +::::::: + +%%% +tag := "header-tags-without-a-tag-field" +%%% + +# Untagged section + +%%% +number := false +%%% + +Some text. + +::::::: + +/-! +A header that is the last block of a document produces a warning. +-/ +/-- +warning: Missing permalink tag + +Hint: Add a metadata block with a tag or explicitly indicate that no tag is desired: + • # Untagged section + ̲%̲%̲%̲ + ̲t̲a̲g̲ ̲:̲=̲ ̲"̲u̲n̲t̲a̲g̲g̲e̲d̲-̲s̲e̲c̲t̲i̲o̲n̲"̲ + ̲%̲%̲%̲ + • # Untagged section + ̲%̲%̲%̲ + ̲t̲a̲g̲ ̲:̲=̲ ̲n̲o̲n̲e̲ + ̲%̲%̲%̲ + +Note: The tag is used as a permanent name for the section or chapter. Writers of this or other documents may use it to link to the section, and it is used to share permanent links. In HTML content, they are used as IDs for headers. Section tags should remain unchanged over time. + +Note: This linter can be disabled with `set_option linter.verso.manual.headerTags false` +-/ +#test_msgs in +set_option linter.verso.manual.headerTags true in +#docs (Verso.Genre.Manual) headerTagsLast "Header tags last" := +::::::: + +%%% +tag := "header-tags-last" +%%% + +Some text. + +# Untagged section + +::::::: + +/-! +A document's title that is followed by a metadata block without a `tag` field produces a warning +whose hint adds the field to that metadata block. +-/ +/-- +warning: Missing permalink tag + +Hint: Add a tag to the metadata block or explicitly indicate that no tag is desired: + • %%% + ̲t̲a̲g̲ ̲:̲=̲ ̲"̲f̲a̲l̲l̲e̲n̲-̲l̲e̲a̲v̲e̲s̲"̲ + shortTitle := "Leaves" + %%% + • %%% + ̲t̲a̲g̲ ̲:̲=̲ ̲n̲o̲n̲e̲ + shortTitle := "Leaves" + %%% + +Note: The tag is used as a permanent name for the section or chapter. Writers of this or other documents may use it to link to the section, and it is used to share permanent links. In HTML content, they are used as IDs for headers. Section tags should remain unchanged over time. + +Note: This linter can be disabled with `set_option linter.verso.manual.headerTags false` +-/ +#test_msgs in +set_option linter.verso.manual.headerTags true in +#docs (Verso.Genre.Manual) headerTagsTitle "Fallen leaves" := +::::::: + +%%% +shortTitle := "Leaves" +%%% + +Leaves fall from the trees in autumn. + +::::::: + +/-! +In a genre other than `Manual`, an untagged header doesn't produce a warning, even when the option +is enabled. +-/ +#test_msgs in +set_option linter.verso.manual.headerTags true in +#docs (Verso.Doc.Genre.none) headerTagsOtherGenre "Header tags other genre" := +::::::: + # Untagged section Some text. diff --git a/src/tests/VersoTests/VersoManual/HeaderTags.lean b/src/tests/VersoTests/VersoManual/HeaderTags.lean new file mode 100644 index 000000000..6d6f59d2c --- /dev/null +++ b/src/tests/VersoTests/VersoManual/HeaderTags.lean @@ -0,0 +1,143 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +import Errata +public import VersoManual +meta import Lean.Elab.Frontend +meta import VersoManual + +/-! +These tests are for `linter.verso.manual.headerTags`. This linter warns about headers that don't +have a metadata block with an explicit `tag` field. A failure means that the linter doesn't warn on +a header that it should or that the editor's warnings after an edit differ from those of a build +from scratch. + +In prior versions of Verso, this linter parsed commands one at a time and could show stale warnings +when a metadata block was edited. +-/ + +namespace Verso.Tests.VersoManual.HeaderTags + +open Lean Elab Command Language + +/-- +Elaborates `input` as commands in the current environment, with the header tag linter enabled, +reusing the results of the commands of `old?` that are unchanged. +-/ +meta def elabInput (input : String) (old? : Option IncrementalState) : + CommandElabM IncrementalState := do + -- Lean's command-line driver sets `internal.cmdlineSnapshots`. With it set, snapshots don't keep + -- commands' syntax, so no command is reused. + let opts := (← getOptions).setBool `internal.cmdlineSnapshots false + |>.setBool `linter.verso.manual.headerTags true + IO.processCommandsIncrementally (Parser.mkInputContext input "Input.lean") {} + (Command.mkState (← getEnv) {} opts) old? + +/-- The messages of all commands of `st`, each with its position and its full text. -/ +meta def messages (st : IncrementalState) : IO (Array String) := + (toSnapshotTree st.initialSnap).getAll.flatMap (·.diagnostics.msgLog.toArray) |>.mapM fun m => + return s!"{m.pos.line}:{m.pos.column} {← m.data.toString}" + +meta def firstLines (msgs : Array String) : List String := + msgs.toList.map fun m => (m.takeWhile (· != '\n')).copy + +/- +The warning about a header disappears when a metadata block with a `tag` field is added after the +header and comes back when the block is removed. The messages of each version of the text equal +those of an elaboration from scratch. + +In prior versions of the Manual genre, the linter checked the text after the header while linting +the header's command. An edit of the next block doesn't elaborate that command again, so the warning +stayed after the tag was added. +-/ +/-- +info: without a tag: [7:0 Missing permalink tag]; as from scratch: true +with a tag: []; as from scratch: true +without a tag again: [7:0 Missing permalink tag]; as from scratch: true +-/ +#test_msgs in +run_cmd do + let header := "#doc (Verso.Genre.Manual) \"Trees\" =>\n\n%%%\ntag := \"trees\"\n%%%\n\n\ + # Leaves\n\n" + let untagged := header ++ "Leaves fall.\n" + let tagged := header ++ "%%%\ntag := \"leaves\"\n%%%\n\nLeaves fall.\n" + let mut old? := none + let mut out := #[] + for (name, text) in [("without a tag", untagged), ("with a tag", tagged), + ("without a tag again", untagged)] do + let edited ← elabInput text old? + let msgs ← messages edited + let fromScratch ← messages (← elabInput text none) + out := out.push s!"{name}: {firstLines msgs}; as from scratch: {msgs == fromScratch}" + old? := some edited + logInfo ("\n".intercalate out.toList) + +/- +The linter warns on a header that is the last block of a `#doc` document. +-/ +/-- info: [9:0 Missing permalink tag] -/ +#test_msgs in +run_cmd do + let input := "#doc (Verso.Genre.Manual) \"Trees\" =>\n\n%%%\ntag := \"trees\"\n%%%\n\n\ + Trees grow.\n\n# Leaves\n" + logInfo s!"{firstLines (← messages (← elabInput input none))}" + +/- +The linter warns on a header that is followed by a deeper header. The deeper header has a tag. +-/ +/-- info: [7:0 Missing permalink tag] -/ +#test_msgs in +run_cmd do + let input := "#doc (Verso.Genre.Manual) \"Trees\" =>\n\n%%%\ntag := \"trees\"\n%%%\n\n\ + # Leaves\n\n## Red\n\n%%%\ntag := \"red\"\n%%%\n\nMaple leaves turn red.\n" + logInfo s!"{firstLines (← messages (← elabInput input none))}" + +/- +The linter warns on a header that is followed by a header two levels higher. The other headers have +tags. +-/ +/-- info: [19:0 Missing permalink tag] -/ +#test_msgs in +run_cmd do + let input := "#doc (Verso.Genre.Manual) \"Trees\" =>\n\n%%%\ntag := \"trees\"\n%%%\n\n\ + # Leaves\n\n%%%\ntag := \"leaves\"\n%%%\n\n## Red\n\n%%%\ntag := \"red\"\n%%%\n\n\ + ### Maple\n\n# Bark\n\n%%%\ntag := \"bark\"\n%%%\n\nBark is rough.\n" + logInfo s!"{firstLines (← messages (← elabInput input none))}" + +/- +The warning about the document's title disappears when a metadata block with a `tag` field is added +as the document's first block and comes back when the block is removed. The messages of each version +of the text equal those of an elaboration from scratch. +-/ +/-- +info: without a tag: [1:26 Missing permalink tag]; as from scratch: true +with a tag: []; as from scratch: true +without a tag again: [1:26 Missing permalink tag]; as from scratch: true +-/ +#test_msgs in +run_cmd do + let title := "#doc (Verso.Genre.Manual) \"Trees\" =>\n\n" + let untagged := title ++ "Trees grow.\n\nLeaves fall.\n" + let tagged := title ++ "%%%\ntag := \"trees\"\n%%%\n\nTrees grow.\n\nLeaves fall.\n" + let mut old? := none + let mut out := #[] + for (name, text) in [("without a tag", untagged), ("with a tag", tagged), + ("without a tag again", untagged)] do + let edited ← elabInput text old? + let msgs ← messages edited + let fromScratch ← messages (← elabInput text none) + out := out.push s!"{name}: {firstLines msgs}; as from scratch: {msgs == fromScratch}" + old? := some edited + logInfo ("\n".intercalate out.toList) + +/- +The linter warns on the title of a `#doc` document without blocks. +-/ +/-- info: [1:26 Missing permalink tag] -/ +#test_msgs in +run_cmd do + let input := "#doc (Verso.Genre.Manual) \"Trees\" =>\n" + logInfo s!"{firstLines (← messages (← elabInput input none))}" diff --git a/src/tests/interactive/test-cases/header_tag_action.lean b/src/tests/interactive/test-cases/header_tag_action.lean new file mode 100644 index 000000000..9b498af80 --- /dev/null +++ b/src/tests/interactive/test-cases/header_tag_action.lean @@ -0,0 +1,17 @@ +import VersoManual +--^ collectDiagnostics + +/-! +Tests that the correct quick fix warnings are added for the missing tags linter. +-/ + +set_option linter.verso.manual.headerTags true + +#doc (Verso.Genre.Manual) "Trees" => + +%%% +tag := "trees" +%%% + +# Leaves +--^ codeAction diff --git a/src/tests/interactive/test-cases/header_tag_action.lean.expected.out b/src/tests/interactive/test-cases/header_tag_action.lean.expected.out new file mode 100644 index 000000000..df047ec4e --- /dev/null +++ b/src/tests/interactive/test-cases/header_tag_action.lean.expected.out @@ -0,0 +1,106 @@ +{"version": 1, + "uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean", + "isIncremental": false, + "diagnostics": + [{"source": "Lean 4", + "severity": 2, + "range": + {"start": {"line": 15, "character": 0}, "end": {"line": 15, "character": 8}}, + "message": + "Missing permalink tag\n\nHint: Add a metadata block with a tag or explicitly indicate that no tag is desired:\n • # Leaves\n ̲%̲%̲%̲\n ̲t̲a̲g̲ ̲:̲=̲ ̲\"̲l̲e̲a̲v̲e̲s̲\"̲\n ̲%̲%̲%̲\n • # Leaves\n ̲%̲%̲%̲\n ̲t̲a̲g̲ ̲:̲=̲ ̲n̲o̲n̲e̲\n ̲%̲%̲%̲\n\nNote: The tag is used as a permanent name for the section or chapter. Writers of this or other documents may use it to link to the section, and it is used to share permanent links. In HTML content, they are used as IDs for headers. Section tags should remain unchanged over time.\n\nNote: This linter can be disabled with `set_option linter.verso.manual.headerTags false`", + "fullRange": + {"start": {"line": 15, "character": 0}, + "end": {"line": 15, "character": 8}}}]} +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}} +[{"title": "Add `tag := \"leaves\"`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean"}, + "edits": + [{"range": + {"start": {"line": 15, "character": 0}, + "end": {"line": 15, "character": 8}}, + "newText": "# Leaves\n%%%\ntag := \"leaves\"\n%%%"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "Verso.Genre.Manual.headerTagActions", + "params": + {"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, + "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}}}}, + {"title": "Add `tag := none`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean"}, + "edits": + [{"range": + {"start": {"line": 15, "character": 0}, + "end": {"line": 15, "character": 8}}, + "newText": "# Leaves\n%%%\ntag := none\n%%%"}]}]}, + "data": + {"providerResultIndex": 1, + "providerName": "Verso.Genre.Manual.headerTagActions", + "params": + {"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, + "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add `tag := "leaves"`: +{"title": "Add `tag := \"leaves\"`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean"}, + "edits": + [{"range": + {"start": {"line": 15, "character": 0}, + "end": {"line": 15, "character": 8}}, + "newText": "# Leaves\n%%%\ntag := \"leaves\"\n%%%"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "Verso.Genre.Manual.headerTagActions", + "params": + {"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}}}} +Resolution of Add `tag := none`: +{"title": "Add `tag := none`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean"}, + "edits": + [{"range": + {"start": {"line": 15, "character": 0}, + "end": {"line": 15, "character": 8}}, + "newText": "# Leaves\n%%%\ntag := none\n%%%"}]}]}, + "data": + {"providerResultIndex": 1, + "providerName": "Verso.Genre.Manual.headerTagActions", + "params": + {"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/header_tag_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}}}} diff --git a/src/tests/interactive/test-cases/header_tag_action_other_line.lean b/src/tests/interactive/test-cases/header_tag_action_other_line.lean new file mode 100644 index 000000000..c60644f46 --- /dev/null +++ b/src/tests/interactive/test-cases/header_tag_action_other_line.lean @@ -0,0 +1,21 @@ +import VersoManual +--^ collectDiagnostics + +/-! +Tests that `headerTagActions` doesn't offer quick fixes for a request on a line other than the +header's, including the quick fixes of a hint about the requested line. The paragraph's command logs +the header tag linter's hint about the header and a hint about the paragraph. +-/ + +set_option linter.verso.manual.headerTags true + +#doc (Verso.Genre.Manual) "Trees" => + +%%% +tag := "trees" +%%% + +# Leaves + +__Maple__ leaves turn red in the fall. +--⬑ codeAction diff --git a/src/tests/interactive/test-cases/header_tag_action_other_line.lean.expected.out b/src/tests/interactive/test-cases/header_tag_action_other_line.lean.expected.out new file mode 100644 index 000000000..e7a79f490 --- /dev/null +++ b/src/tests/interactive/test-cases/header_tag_action_other_line.lean.expected.out @@ -0,0 +1,30 @@ +{"version": 1, + "uri": + "file:///src/tests/interactive/test-cases/header_tag_action_other_line.lean", + "isIncremental": false, + "diagnostics": + [{"source": "Lean 4", + "severity": 2, + "range": + {"start": {"line": 17, "character": 0}, "end": {"line": 17, "character": 8}}, + "message": + "Missing permalink tag\n\nHint: Add a metadata block with a tag or explicitly indicate that no tag is desired:\n • # Leaves\n ̲%̲%̲%̲\n ̲t̲a̲g̲ ̲:̲=̲ ̲\"̲l̲e̲a̲v̲e̲s̲\"̲\n ̲%̲%̲%̲\n • # Leaves\n ̲%̲%̲%̲\n ̲t̲a̲g̲ ̲:̲=̲ ̲n̲o̲n̲e̲\n ̲%̲%̲%̲\n\nNote: The tag is used as a permanent name for the section or chapter. Writers of this or other documents may use it to link to the section, and it is used to share permanent links. In HTML content, they are used as IDs for headers. Section tags should remain unchanged over time.\n\nNote: This linter can be disabled with `set_option linter.verso.manual.headerTags false`", + "fullRange": + {"start": {"line": 17, "character": 0}, + "end": {"line": 17, "character": 8}}}, + {"source": "Lean 4", + "severity": 2, + "range": + {"start": {"line": 19, "character": 0}, "end": {"line": 19, "character": 9}}, + "message": + "Unnecessary '_'\n\nHint: Use the minimal number of '_'s\n _̵_̵M̵a̵p̵l̵e̵_̵_̵_̲M̲a̲p̲l̲e̲_̲\n\nNote: This linter can be disabled with `set_option linter.verso.markup.emph false`", + "fullRange": + {"start": {"line": 19, "character": 0}, + "end": {"line": 19, "character": 9}}}]} +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_action_other_line.lean"}, + "range": + {"start": {"line": 19, "character": 0}, "end": {"line": 19, "character": 0}}, + "context": {"diagnostics": []}} +[] diff --git a/src/tests/interactive/test-cases/header_tag_metadata_action.lean b/src/tests/interactive/test-cases/header_tag_metadata_action.lean new file mode 100644 index 000000000..4cdea8d8c --- /dev/null +++ b/src/tests/interactive/test-cases/header_tag_metadata_action.lean @@ -0,0 +1,19 @@ +import VersoManual + +/-! +Tests that Lean's own code action provider offers the header tag linter's quick fixes with their +short titles in a metadata block without a `tag` field. +-/ + +set_option linter.verso.manual.headerTags true + +#doc (Verso.Genre.Manual) "Trees" => + +# Leaves + +%%% +shortTitle := "Leaves" +%%% +--^ codeAction + +Leaves fall from the trees in autumn. diff --git a/src/tests/interactive/test-cases/header_tag_metadata_action.lean.expected.out b/src/tests/interactive/test-cases/header_tag_metadata_action.lean.expected.out new file mode 100644 index 000000000..b6a29720a --- /dev/null +++ b/src/tests/interactive/test-cases/header_tag_metadata_action.lean.expected.out @@ -0,0 +1,110 @@ +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_metadata_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}} +[{"title": "Add `tag := \"leaves\"`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": + "file:///src/tests/interactive/test-cases/header_tag_metadata_action.lean"}, + "edits": + [{"range": + {"start": {"line": 11, "character": 0}, + "end": {"line": 15, "character": 3}}, + "newText": + "# Leaves\n%%%\ntag := \"leaves\"\nshortTitle := \"Leaves\"\n%%%"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_metadata_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, + "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}}}}, + {"title": "Add `tag := none`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": + "file:///src/tests/interactive/test-cases/header_tag_metadata_action.lean"}, + "edits": + [{"range": + {"start": {"line": 11, "character": 0}, + "end": {"line": 15, "character": 3}}, + "newText": + "# Leaves\n%%%\ntag := none\nshortTitle := \"Leaves\"\n%%%"}]}]}, + "data": + {"providerResultIndex": 1, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_metadata_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, + "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add `tag := "leaves"`: +{"title": "Add `tag := \"leaves\"`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": + "file:///src/tests/interactive/test-cases/header_tag_metadata_action.lean"}, + "edits": + [{"range": + {"start": {"line": 11, "character": 0}, + "end": {"line": 15, "character": 3}}, + "newText": + "# Leaves\n%%%\ntag := \"leaves\"\nshortTitle := \"Leaves\"\n%%%"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_metadata_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}}}} +Resolution of Add `tag := none`: +{"title": "Add `tag := none`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": + "file:///src/tests/interactive/test-cases/header_tag_metadata_action.lean"}, + "edits": + [{"range": + {"start": {"line": 11, "character": 0}, + "end": {"line": 15, "character": 3}}, + "newText": + "# Leaves\n%%%\ntag := none\nshortTitle := \"Leaves\"\n%%%"}]}]}, + "data": + {"providerResultIndex": 1, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_metadata_action.lean"}, + "range": + {"start": {"line": 15, "character": 2}, "end": {"line": 15, "character": 2}}, + "context": {"diagnostics": []}}}} diff --git a/src/tests/interactive/test-cases/header_tag_title_action.lean b/src/tests/interactive/test-cases/header_tag_title_action.lean new file mode 100644 index 000000000..b849f1bd0 --- /dev/null +++ b/src/tests/interactive/test-cases/header_tag_title_action.lean @@ -0,0 +1,15 @@ +import VersoManual +--^ sync + +/-! +Tests that `headerTagActions` offers the header tag linter's quick fixes for the document's title on +the title's line. The comment with the request is the document's first block, so the fixes insert a +metadata block before it. +-/ + +set_option linter.verso.manual.headerTags true + +#doc (Verso.Genre.Manual) "Fallen Leaves" => + --^ codeAction + +Leaves fall from the trees in autumn. diff --git a/src/tests/interactive/test-cases/header_tag_title_action.lean.expected.out b/src/tests/interactive/test-cases/header_tag_title_action.lean.expected.out new file mode 100644 index 000000000..32c437826 --- /dev/null +++ b/src/tests/interactive/test-cases/header_tag_title_action.lean.expected.out @@ -0,0 +1,104 @@ +{"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_title_action.lean"}, + "range": + {"start": {"line": 11, "character": 28}, "end": {"line": 11, "character": 28}}, + "context": {"diagnostics": []}} +[{"title": "Add `tag := \"fallen-leaves\"`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": + "file:///src/tests/interactive/test-cases/header_tag_title_action.lean"}, + "edits": + [{"range": + {"start": {"line": 12, "character": 0}, + "end": {"line": 12, "character": 0}}, + "newText": "%%%\ntag := \"fallen-leaves\"\n%%%\n\n"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "Verso.Genre.Manual.headerTagActions", + "params": + {"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_title_action.lean"}, + "range": + {"start": {"line": 11, "character": 28}, + "end": {"line": 11, "character": 28}}, + "context": {"diagnostics": []}}}}, + {"title": "Add `tag := none`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": + "file:///src/tests/interactive/test-cases/header_tag_title_action.lean"}, + "edits": + [{"range": + {"start": {"line": 12, "character": 0}, + "end": {"line": 12, "character": 0}}, + "newText": "%%%\ntag := none\n%%%\n\n"}]}]}, + "data": + {"providerResultIndex": 1, + "providerName": "Verso.Genre.Manual.headerTagActions", + "params": + {"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_title_action.lean"}, + "range": + {"start": {"line": 11, "character": 28}, + "end": {"line": 11, "character": 28}}, + "context": {"diagnostics": []}}}}] +Resolution of Add `tag := "fallen-leaves"`: +{"title": "Add `tag := \"fallen-leaves\"`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": + "file:///src/tests/interactive/test-cases/header_tag_title_action.lean"}, + "edits": + [{"range": + {"start": {"line": 12, "character": 0}, + "end": {"line": 12, "character": 0}}, + "newText": "%%%\ntag := \"fallen-leaves\"\n%%%\n\n"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "Verso.Genre.Manual.headerTagActions", + "params": + {"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_title_action.lean"}, + "range": + {"start": {"line": 11, "character": 28}, + "end": {"line": 11, "character": 28}}, + "context": {"diagnostics": []}}}} +Resolution of Add `tag := none`: +{"title": "Add `tag := none`", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, + "uri": + "file:///src/tests/interactive/test-cases/header_tag_title_action.lean"}, + "edits": + [{"range": + {"start": {"line": 12, "character": 0}, + "end": {"line": 12, "character": 0}}, + "newText": "%%%\ntag := none\n%%%\n\n"}]}]}, + "data": + {"providerResultIndex": 1, + "providerName": "Verso.Genre.Manual.headerTagActions", + "params": + {"textDocument": + {"uri": + "file:///src/tests/interactive/test-cases/header_tag_title_action.lean"}, + "range": + {"start": {"line": 11, "character": 28}, + "end": {"line": 11, "character": 28}}, + "context": {"diagnostics": []}}}} diff --git a/src/verso-manual/VersoManual/Linters.lean b/src/verso-manual/VersoManual/Linters.lean index 10e787faa..250154428 100644 --- a/src/verso-manual/VersoManual/Linters.lean +++ b/src/verso-manual/VersoManual/Linters.lean @@ -6,143 +6,281 @@ Author: David Thrane Christiansen module public meta import Lean.Linter.Basic public meta import Lean.Meta.Hint +public meta import Lean.Server.CodeActions.Basic public meta import Verso.Doc.Concrete public meta import MultiVerso.Slug public meta import VersoManual.Linters.Options - -public section +import VersoManual.Basic set_option linter.missingDocs true open Lean Linter Elab Command open Lean.Doc (HeaderView MetadataView VersoInline) -open Lean.Doc.Parser +namespace Verso.Genre.Manual + +/-- Checks whether `field`'s name is `tag`. -/ +private meta def isTagField (field : TSyntax ``Lean.Parser.Term.structInstField) : Bool := + match field with + | `(Lean.Parser.Term.structInstField| + $x:ident $[$_* $[$_:typeSpec]? $_:structInstFieldDecl]?) => x.getId == `tag + | _ => false + +private meta partial def suggestId' (name : Array VersoInline) : String := Id.run do + let mut strTitle := "" + for inl in name do + match inl.view with + | .text s => strTitle := strTitle ++ s.getVersoText.toLower + | .code c => strTitle := strTitle ++ c.getVersoCode + | .emph e => strTitle := strTitle ++ suggestId' e.content + | .bold b => strTitle := strTitle ++ suggestId' b.content + | .link l => strTitle := strTitle ++ suggestId' l.content + | .role r => strTitle := strTitle ++ suggestId' r.content + | _ => pure () + return strTitle + +private meta def suggestId (name : Array VersoInline) : String := + suggestId' name |>.sluggify |>.toString + +/-- +A recorded fix that adds a tag to a header that's missing one. +-/ +private meta structure HeaderTagFix where + /-- The title and the text edit of each quick fix. -/ + fixes : Array (String × Lsp.TextEdit) +deriving TypeName + +/-- +A marker placed in the info tree of a header that indicates that the header tag linter applies to +it. +-/ +private meta structure HeaderTagCheck where +deriving TypeName + +/-- +Builds `hint` with `MessageData.hint` and pushes a `HeaderTagFix` leaf for `stx` with the titles +and edits of the hint's code actions. + +The `MessageData` is used to provide a clickable InfoView hint, while the info leaf is used for code +actions that need to trigger on a multi-command range. The hint's code actions are at `ref`, and +its preview shows the text in `preview?` with the edit. +-/ +private meta def headerHint (stx ref : Syntax) (hint : MessageData) + (suggestions : Array (String × String)) (range : Syntax.Range) + (preview? : Option Syntax.Range := none) : CoreM MessageData := do + let msg ← MessageData.hint hint (ref? := some ref) <| + suggestions.map fun (title, text) => { + suggestion := .string text, toCodeActionTitle? := some fun _ => title, + span? := some (Syntax.ofRange range), previewSpan? := preview?.map Syntax.ofRange + } + let lspRange := (← getFileMap).utf8RangeToLspRange range + let fixes := suggestions.map fun (title, newText) => (title, { range := lspRange, newText }) + pushInfoLeaf <| .ofCustomInfo { stx, value := .mk { fixes : HeaderTagFix } } + return msg + +private meta def tagNote : MessageData := + MessageData.note <| + "The tag is used as a permanent name for the section or chapter. Writers " ++ + "of this or other documents may use it to link to the section, and it is " ++ + "used to share permanent links. In HTML content, they are used as IDs for " ++ + "headers. Section tags should remain unchanged over time." + +/-- +Warns about `header` unless `next?` is a metadata block with a `tag` field. + +`next?` should be the block after the header, or `none` when the header is the last block in the +document. +-/ +private meta def checkHeader (header : HeaderView) (next? : Option Syntax) : + CommandElabM Unit := do + let metadata? := next?.bind (MetadataView.of ⟨·⟩) + -- Abort if the next field is metadata with a tag field. Otherwise continue. + if metadata?.any (·.fields.any isTagField) then return + let text ← getFileMap + let some ⟨start, stop⟩ := header.stx.raw.getRange? | return + let name := suggestId header.content + let blockStr := start.extract text.source stop + let log (hint : MessageData) := + logLint linter.verso.manual.headerTags header.stx m!"Missing permalink tag{hint}{tagNote}" + let tagField := s!"tag := \"{name}\"" + match metadata? with + | none => + let suggestions := #[ + (s!"Add `{tagField}`", s!"{blockStr}\n%%%\n{tagField}\n%%%"), + ("Add `tag := none`", s!"{blockStr}\n%%%\ntag := none\n%%%") + ] + log <| ← runTermElabM fun _ => + headerHint header.stx (Syntax.ofRange ⟨start, stop⟩) + "Add a metadata block with a tag or explicitly indicate that no tag is desired:" + suggestions ⟨start, stop⟩ + | some metadata => + let some ⟨_, stop1⟩ := metadata.opener.getRange? | return + let some ⟨_, stop2⟩ := metadata.closer.getRange? | return + let some range := (mkNullNode #[header.stx, metadata.stx]).getRange? | return + let afterOpener := stop1.extract text.source stop2 + let suggestions := #[ + (s!"Add `{tagField}`", s!"{blockStr}\n%%%\n{tagField}{afterOpener}"), + ("Add `tag := none`", s!"{blockStr}\n%%%\ntag := none{afterOpener}") + ] + log <| ← runTermElabM fun _ => + headerHint header.stx (Syntax.ofRange range) + "Add a tag to the metadata block or explicitly indicate that no tag is desired:" + suggestions range + +/-- +Warns about the document's title `title` unless `next?` is a metadata block with a `tag` field. + +`next?` should be the document's first block, or `none` when the document has no blocks. `stop` is +the end of the token before the document's blocks. The hints insert the metadata block at the first +block or at `stop`, and the field after the metadata block's opener. +-/ +private meta def checkTitle (title : StrLit) (next? : Option Syntax) (stop : String.Pos.Raw) : + CommandElabM Unit := do + let metadata? := next?.bind (MetadataView.of ⟨·⟩) + if metadata?.any (·.fields.any isTagField) then return + let some content ← try some <$> Verso.Doc.Concrete.stringToInlines title catch _ => pure none + | return + let tagField := s!"tag := \"{suggestId (content.map (⟨·⟩))}\"" + let newMetadata := + "Add a metadata block with a tag or explicitly indicate that no tag is desired:" + let (hint, edit, pos, preview?) : MessageData × (String → String) × _ × _ ← + match metadata?, next? with + | none, some next => + let some pos := next.getPos? | return + -- The metadata block goes before the indentation of the first block. + let text ← getFileMap + let lineStart := text.ofPosition ⟨(text.toPosition pos).line, 0⟩ + let pos := if (lineStart.extract text.source pos).all (· == ' ') then lineStart else pos + pure (newMetadata, (s!"%%%\n{·}\n%%%\n\n"), pos, none) + | none, none => pure (newMetadata, (s!"\n\n%%%\n{·}\n%%%"), stop, none) + | some metadata, _ => + let some pos := metadata.opener.getTailPos? | return + pure ("Add a tag to the metadata block or explicitly indicate that no tag is desired:", + (s!"\n{·}"), pos, metadata.stx.raw.getRange?) + let suggestions := + #[(s!"Add `{tagField}`", edit tagField), ("Add `tag := none`", edit "tag := none")] + let hint ← runTermElabM fun _ => + headerHint title title hint suggestions ⟨pos, pos⟩ preview? + logLint linter.verso.manual.headerTags title m!"Missing permalink tag{hint}{tagNote}" + +open Verso.Doc.Elab (FinishedPart) in /-- -Lints for tagless headers. +Appends the headers of `part` and of its subparts to `headers`, except those of parts that end +before `start`. -/ -meta partial def headerTagLinter : Linter where +private meta partial def closedHeaders (start : String.Pos.Raw) (headers : Array Syntax) + (part : FinishedPart) : Array Syntax := + match part with + | .mk (rangeSyntax := header) (subParts := subParts) (endPos := endPos) .. => + if endPos < start then headers else subParts.foldl (closedHeaders start) (headers.push header) + | .included _ => headers + +open Verso.Doc.Elab (PartContext) in +/-- +Finds the header or the `#doc` command right before the top-level block at `start`, in the part +state `ctx` after the block's command. + +A header or the `#doc` command is right before the block when its syntax, with its trailing +whitespace, ends at `start`. Such a header belongs to an open part or to a part that was closed by +the block's command. Parts that were closed by an earlier command end before `start`. +`headerBefore` skips headers with a parse error. +-/ +private meta def headerBefore (ctx : PartContext) (start : String.Pos.Raw) : Option Syntax := + let frames := ctx.parents.push ctx.toPartFrame + let headers := frames.foldl (init := #[]) fun headers frame => + frame.priorParts.foldl (closedHeaders start) (headers.push frame.rangeSyntax) + headers.find? fun stx => !stx.hasMissing && stx.getTrailingTailPos? == some start + +/-- Gives the title, the arrow and whether the document is empty for a `#doc` command. -/ +private meta def docCommand? : Syntax → Option (StrLit × Syntax × Bool) + | `(command|#doc ( $_ ) $title:str =>%$arrow $[$empty]?) => some (title, arrow, empty.isSome) + | _ => none + +/-- +Warns about headers in documents in the `Manual` genre that aren't followed by a metadata block with +a `tag` field. +-/ +public meta def headerTagLinter : Linter where run := withSetOptionIn fun stx => do + if stx.hasMissing then return unless (`Verso.Doc.Concrete).isPrefixOf stx.getKind do return unless getLinterValue linter.verso.manual.headerTags (← getLinterOptions) do return - -- Identify the command form and extract its genre term. `#docs (...) ...` and the opening - -- `#doc (...) ... =>` both place the genre as their third syntax child. Individual blocks - -- in an incremental `#doc` document are parsed as `addBlockCmd`/`addLastBlockCmd` commands, - -- which don't carry the genre syntactically, so we read it from the environment extension - -- that `startDoc` populates when it processes the opening `#doc (...) =>` line. - let genreStx? : Option Syntax ← - match stx[0] with - | .atom _ "#docs" | .atom _ "#doc" => pure (some stx[2]) - | _ => - if stx.isOfKind ``Verso.Doc.Concrete.addBlockCmd - || stx.isOfKind ``Verso.Doc.Concrete.addLastBlockCmd then - pure (some (Verso.Doc.Concrete.docEnvironmentExt.getState (← getEnv)).genreSyntax) - else pure none - - let some genreStx := genreStx? | return + -- The genre of `#docs (...) ...` is its third syntax child, and its blocks are the children of + -- its `document` node. Top-level blocks of a `#doc` document are parsed as `addBlockCmd` and + -- `addLastBlockCmd` commands, whose only child is the block. The genre and the part state are + -- read from Verso's document environment extension. + let docEnv := Verso.Doc.Concrete.docEnvironmentExt.getState (← getEnv) + let some (genreStx, docsBlocks?) := + if stx[0] matches .atom _ "#docs" then some (stx[2], some stx[8].getArgs) + else if stx.isOfKind ``Verso.Doc.Concrete.addBlockCmd + || stx.isOfKind ``Verso.Doc.Concrete.addLastBlockCmd + || stx.isOfKind ``Verso.Doc.Concrete.replaceDoc then + some (docEnv.genreSyntax, none) + else none + | return let genreName ← try runTermElabM <| fun _ => realizeGlobalConstNoOverload genreStx catch | _ => return - unless genreName == `Verso.Genre.Manual do return - - let text ← getFileMap - - discard <| stx.replaceM fun block => do - if let some hdr := HeaderView.of ⟨block⟩ then - let inls := hdr.content - let some ⟨start, stop⟩ := block.getRange? - | return none - let mut nextLine : String.Legacy.Iterator := {s := text.source, i := stop} - while h : nextLine.hasNext do - if (nextLine.curr' h).isWhitespace then nextLine := nextLine.next' h - else break - -- Attempt to parse the next command as a metadata block. - let ictx := { - inputString := text.source, - fileName := ← getFileName, - fileMap := text - } - let pmctx := { - env := ← getEnv, - options := ← getOptions - } - let toks := Parser.getTokenTable (← getEnv) - let s := { cache := { tokenCache := {}, parserCache := {} }, pos := nextLine.i } - let s := metadataBlockFn.run ictx pmctx toks s - let tagNote := - MessageData.note <| - "The tag is used as a permanent name for the section or chapter. Writers "++ - "of this or other documents may use it to link to the section, and it is " ++ - "used to share permanent links. In HTML content, they are used as IDs for " ++ - "headers. Section tags should remain unchanged over time." - if s.hasError || !s.recoveredErrors.isEmpty then - -- Next block is not metadata, so suggest inserting one - let name := suggestId inls - let blockStr := start.extract text.source stop - let suggestions : Array Meta.Hint.Suggestion := #[ - s!"{blockStr}\n%%%\ntag := \"{name}\"\n%%%", - s!"{blockStr}\n%%%\ntag := none\n%%%" - ] - let h ← runTermElabM fun _ => MessageData.hint "Add a metadata block with a tag or explicitly indicate that no tag is desired:" suggestions (ref? := some block) - logLint linter.verso.manual.headerTags block m!"Missing permalink tag{h}{tagNote}" - return none - let nextStx ← - if s.stxStack.size = 1 then - pure (s.stxStack.get! 0) - else return none - if let some metaView := MetadataView.of ⟨nextStx⟩ then - let fieldOrAbbrev := metaView.fields - let metadataStx : Term := - ⟨(← `(Lean.Parser.Term.structInst| { $[$fieldOrAbbrev],* })).raw⟩ - let isMissing ← runTermElabM fun _ => do - let type := .const `Verso.Genre.Manual.PartMetadata [] - let metadataTerm ← Term.elabTerm metadataStx (some type) - let tagExpr ← Meta.whnf (← Meta.mkProjection metadataTerm `tag) - match_expr tagExpr with - | Option.none _ => pure true - | _ => pure false - -- The syntactic check is to disable the linter when an explicit `none` is used - if isMissing && noFieldIsTag fieldOrAbbrev then - let name := suggestId inls - -- Find the beginning of the line after the token - let some ⟨start1, stop1⟩ := metaView.opener.getRange? - | return none - let some ⟨start2, stop2⟩ := metaView.closer.getRange? - | return none - let blockStr := start.extract text.source stop - let suggestions : Array Meta.Hint.Suggestion := #[ - s!"{blockStr}\n%%%\ntag := \"{name}\"" ++ stop1.extract text.source stop2, - s!"{blockStr}\n%%%\ntag := none" ++ stop1.extract text.source stop2 - ] - - let h ← runTermElabM fun _ => MessageData.hint "Add a tag to the metadata block or explicitly indicate that no tag is desired:" suggestions (ref? := some <| mkNullNode #[block, nextStx]) - logLint linter.verso.manual.headerTags block m!"Missing permalink tag{h}{tagNote}" - pure () - return none - pure none - -where - noFieldIsTag (xs : Array (TSyntax `Lean.Parser.Term.structInstField)) : Bool := - xs.all fun - | `(Lean.Parser.Term.structInstField|$x:ident) - | `(Lean.Parser.Term.structInstField|$x:ident := $_ ) => x.getId ≠ `tag - | _ => true - - suggestId (name : Array VersoInline) : String := - suggestId' name |>.sluggify |>.toString - - suggestId' (name : Array VersoInline) : String := Id.run do - let mut strTitle := "" - for inl in name do - match inl.view with - | .text s => strTitle := strTitle ++ s.getVersoText.toLower - | .code c => strTitle := strTitle ++ c.getVersoCode - | .emph e => strTitle := strTitle ++ suggestId' e.content - | .bold b => strTitle := strTitle ++ suggestId' b.content - | .link l => strTitle := strTitle ++ suggestId' l.content - | .role r => strTitle := strTitle ++ suggestId' r.content - | _ => pure () - return strTitle + unless genreName == ``Verso.Genre.Manual do return + + if let some blocks := docsBlocks? then + if let some stop := stx[7].getTailPos? then checkTitle ⟨stx[5]⟩ blocks[0]? stop + for h : i in [0:blocks.size] do + let some header := HeaderView.of ⟨blocks[i]⟩ | continue + checkHeader header blocks[i + 1]? + return + + -- The title of `#doc` is checked with the first block's command. The syntax of a `#doc` command + -- without blocks ends with `emptyDocument`. + if let some (title, arrow, empty) := docCommand? stx then + if !empty then + pushInfoLeaf <| .ofCustomInfo { stx := title, value := .mk ({} : HeaderTagCheck) } + else if let some stop := arrow.getTailPos? then checkTitle title none stop + return + + let block := stx[0] + if let some before := block.getPos?.bind (headerBefore docEnv.partState.partContext) then + if let some header := HeaderView.of ⟨before⟩ then checkHeader header (some block) + else if let some (title, arrow, _) := docCommand? before then + if let some stop := arrow.getTailPos? then checkTitle title (some block) stop + let some header := HeaderView.of ⟨block⟩ | return + -- In an `addBlockCmd`, the block's header is checked with the next command. + if stx.isOfKind ``Verso.Doc.Concrete.addBlockCmd then + pushInfoLeaf <| .ofCustomInfo { stx := header.stx, value := .mk ({} : HeaderTagCheck) } + else checkHeader header none meta initialize addLinter headerTagLinter + +open Lean Server Lsp RequestM in +/-- +Offers the header tag linter's quick fixes for the headers in the requested lines of a `#doc` +document. +-/ +@[code_action_provider] +public meta def headerTagActions : CodeActionProvider := fun params snap => do + let doc ← readDoc + let (finished, _, _) ← (doc.cmdSnaps.getFinishedPrefix : BaseIO _) + let some next := (finished.dropWhile (·.endPos < snap.endPos))[1]? | return #[] + -- The parts of the info trees that are filled in later, such as the linters', are tasks. + for infoState in [snap.cmdState.infoState, next.cmdState.infoState] do + for (_, part) in infoState.lazyAssignment do + unless ← IO.hasFinished part do return #[] + let checksHeader := snap.infoTree.foldInfo (init := false) fun _ info found => + found || match info with + | .ofCustomInfo { value, .. } => (value.get? HeaderTagCheck).isSome + | _ => false + unless checksHeader do return #[] + let text := doc.meta.text + return next.infoTree.foldInfo (init := #[]) fun _ info actions => Id.run do + let .ofCustomInfo { stx, value } := info | actions + let some { fixes } := value.get? HeaderTagFix | actions + let some range := stx.getRange? | actions + let lspRange := text.utf8RangeToLspRange range + unless lspRange.start.line ≤ params.range.end.line do return actions + unless params.range.start.line ≤ lspRange.end.line do return actions + actions ++ fixes.map fun (title, edit) => { + eager.title := title + eager.kind? := "quickfix" + eager.edit? := some <| .ofTextEdit doc.versionedIdentifier edit + }