Lean.DocString.Links

Computes the root of the Lean reference manual that should be used for targets.

If the environment variable LEAN_MANUAL_ROOT is set, it is used as the root. If not, but a manual root is pre-configured for the current Lean executable (typically true for releases), then it is used. If neither are true, then https://lean-lang.org/doc/reference/latest/ is used.

Equations

One or more equations did not get rendered due to their size.

source

def Lean.rewriteManualLinksCore (s : String) :

BaseIO (Array (String.Range × String) × String)

Rewrites links from the internal Lean manual syntax to the correct URL. This rewriting is an overapproximation: any parentheses containing the internal syntax of a Lean manual URL is rewritten.

The internal syntax is the URL scheme lean-manual followed by the path /KIND/MORE..., where KIND is a kind of content being linked to. Presently, the only valid kind is section, and it requires that the remainder of the path consists of one element, which is a section or part identifier.

The correct URL is based on a manual root URL, which is determined by the LEAN_MANUAL_ROOT environment variable. If this environment variable is not set, a manual root provided when Lean was built is used (typically this is the version corresponding to the current release). If no such root is available, the latest version of the manual is used.

Equations

One or more equations did not get rendered due to their size.

source

def Lean.rewriteManualLinksCore.urlChar (c : Char) :

Bool

Returns true if the character is one of those allowed in RFC 3986 sections 2.2 and 2.3. other than '(' or')'.

Equations

One or more equations did not get rendered due to their size.

source

def Lean.rewriteManualLinksCore.lookingAt (goal : String) (iter : String.Iterator) :

Bool

Returns true if goal is a prefix of the string at the position pointed to by iter.

Equations

Lean.rewriteManualLinksCore.lookingAt goal iter = iter.s.substrEq iter.i goal 0 goal.endPos.byteIdx

source

def Lean.rewriteManualLinksCore.rw (path : String) :

Except String String

Equations

One or more equations did not get rendered due to their size.

source

def Lean.rewriteManualLinks (docString : String) :

BaseIO String

Rewrites Lean reference manual links in docstring to point at the reference manual.

This assumes that all such links have already been validated by validateDocComment.

Equations

One or more equations did not get rendered due to their size.

source

def Lean.validateBuiltinDocString (docString : String) :

IO Unit

Validates all links to the Lean reference manual in docstring, printing an error message if any are invalid. Returns true if all links are valid.

This is intended to be used before saving a docstring that is later subject to rewriting with rewriteManualLinks, in contexts where the imports needed to produce better error messages in validateDocComment are not yet available.

Equations

One or more equations did not get rendered due to their size.