eb58f46ce7
This PR adds a canonical syntax for linking to sections in the language reference along with formatting of examples in docstrings according to the docstring style guide. Docstrings are now pre-processed as follows: * Output included as part of examples is shown with leading line comment indicators in hovers * URLs of the form `lean-manual://section/section-id` are rewritten to links that point at the corresponding section in the Lean reference manual. The reference manual's base URL is configured when Lean is built and can be overridden with the `LEAN_MANUAL_ROOT` environment variable. This way, releases can point documentation links to the correct snapshot, and users can use their own, e.g. for offline reading. Manual URLs in docstrings are validated when the docstring is added. The presence of a URL starting with `lean-manual://` that is not a syntactically valid section link causes the docstring to be rejected. This allows for future extensibility to the set of allowed links. There is no validation that the linked-to section actually exists. To provide the best possible error messages in case of validation failures, `Lean.addDocString` now takes a `TSyntax ``docComment` instead of a string; clients should adapt by removing the step that extracts the string, or by calling the lower-level `addDocStringCore` in cases where the docstring in question is obtained from the environment and has thus already had its links validated. A stage0 update is required to make the documentation site configurable at build time and for releases. A local commit on top of a stage0 update that will be sent in a followup PR includes the configurable reference manual root and updates to the release checklist. --------- Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
61 lines
2.1 KiB
Text
61 lines
2.1 KiB
Text
/-
|
|
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: David Thrane Christiansen
|
|
-/
|
|
|
|
prelude
|
|
import Lean.Environment
|
|
import Lean.Exception
|
|
import Lean.Log
|
|
import Lean.DocString.Extension
|
|
import Lean.DocString.Links
|
|
|
|
set_option linter.missingDocs true
|
|
|
|
namespace Lean
|
|
|
|
/--
|
|
Validates all links to the Lean reference manual in `docstring`.
|
|
|
|
This is intended to be used before saving a docstring that is later subject to rewriting with
|
|
`rewriteManualLinks`.
|
|
-/
|
|
def validateDocComment
|
|
[Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
|
|
(docstring : TSyntax `Lean.Parser.Command.docComment) :
|
|
m Unit := do
|
|
let str := docstring.getDocString
|
|
let pos? := docstring.raw[1].getHeadInfo? >>= (·.getPos?)
|
|
|
|
let (errs, out) ← (rewriteManualLinksCore str : IO _)
|
|
|
|
for (⟨start, stop⟩, err) in errs do
|
|
-- Report errors at their actual location if possible
|
|
if let some pos := pos? then
|
|
let urlStx : Syntax := .atom (.synthetic (pos + start) (pos + stop)) (str.extract start stop)
|
|
logErrorAt urlStx err
|
|
else
|
|
logError err
|
|
|
|
/--
|
|
Adds a docstring to the environment, validating documentation links.
|
|
-/
|
|
def addDocString
|
|
[Monad m] [MonadError m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
|
|
(declName : Name) (docComment : TSyntax `Lean.Parser.Command.docComment) : m Unit := do
|
|
unless (← getEnv).getModuleIdxFor? declName |>.isNone do
|
|
throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
|
|
validateDocComment docComment
|
|
let docString : String ← getDocStringText docComment
|
|
modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
|
|
|
|
/--
|
|
Adds a docstring to the environment, validating documentation links.
|
|
-/
|
|
def addDocString'
|
|
[Monad m] [MonadError m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
|
|
(declName : Name) (docString? : Option (TSyntax `Lean.Parser.Command.docComment)) : m Unit :=
|
|
match docString? with
|
|
| some docString => addDocString declName docString
|
|
| none => return ()
|