Skip to content

fix: fix a collection of docstring errors#12959

Merged
TwoFX merged 13 commits intoleanprover:masterfrom
dfpetrin:docstring-fix
Mar 19, 2026
Merged

fix: fix a collection of docstring errors#12959
TwoFX merged 13 commits intoleanprover:masterfrom
dfpetrin:docstring-fix

Conversation

@dfpetrin
Copy link
Copy Markdown
Contributor

@dfpetrin dfpetrin commented Mar 18, 2026 •
edited by TwoFX
Loading

This PR fixes a series of errors in docstrings.

This includes:

  • incorrect gramar
  • errant reference to "dependent" in the non-dependent HashMap files
  • reference to expression metavariables as universe level metavariables
  • outdated reference to usizeSz instead of USize.size
  • syntax errors in code examples
  • a broken link to a paper

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 18, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 18, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 61a3443a9569d548a235f785b9a33984bb7ff622 --onto 6714601ee4a123fef0f6ff3e44f01086ba78dfce. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-18 06:54:20)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b7380758ae54ef60b109b7e5325075912e437958 --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-19 01:38:30)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 18, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 61a3443a9569d548a235f785b9a33984bb7ff622 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-18 06:54:22)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b7380758ae54ef60b109b7e5325075912e437958 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-19 01:38:32)

Derrik Petrin added 8 commits March 18, 2026 17:48
doc: fix small error in run_meta docstring
e84716b 
Examples:
```lean4
import Lean
open Lean Meta

  let mvar1 ← mkFreshExprMVar (mkConst `Nat)
  let e := (mkConst `Nat.succ).app mvar1
  -- e is `Nat.succ ?m.773`, `?m.773` is unassigned
  mvar1.mvarId!.assign (mkNatLit 42)
  -- e is `Nat.succ ?m.773`, `?m.773` is assigned to `42`
  let e' ← instantiateMVars e
  -- e' is `Nat.succ 42`, `?m.773` is assigned to `42`
  pure 4

def getFinBound (e : Expr) : MetaM (Option Expr) := do
  let type ← whnf (← inferType e)
  let_expr Fin bound := type | return none
  return bound

def a : Fin 100 := 42

  match ← getFinBound (.const ``a []) with
  | some limit => IO.println (← ppExpr limit)
  | none => IO.println "no limit found"
```
style
a52e964
grammar error
1cf24c1
incorrect reference
c68a777
broken link
5049e19
minor error
3ac539d
grammar error
10c992d
incorrect constant
e0ebf61
@dfpetrin
Copy link
Copy Markdown
Contributor Author

dfpetrin commented Mar 19, 2026

Alright I understand which test is failing/why, fixing!

@dfpetrin
Copy link
Copy Markdown
Contributor Author

dfpetrin commented Mar 19, 2026

Since these are all docstring changes, and I am assuming the manual is in part generated from docstrings, should I also kick off reference manual CI?

@dfpetrin dfpetrin marked this pull request as ready for review March 19, 2026 02:43
TwoFX
TwoFX approved these changes Mar 19, 2026
View reviewed changes
Copy link
Copy Markdown
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@TwoFX TwoFX added this pull request to the merge queue Mar 19, 2026
@TwoFX TwoFX removed this pull request from the merge queue due to a manual request Mar 19, 2026
@TwoFX TwoFX added the changelog-doc Documentation label Mar 19, 2026
@TwoFX TwoFX changed the title doc: fix a collection of docstring errors fix: fix a collection of docstring errors Mar 19, 2026
@TwoFX TwoFX enabled auto-merge March 19, 2026 06:42
@TwoFX TwoFX added this pull request to the merge queue Mar 19, 2026
Merged via the queue into leanprover:master with commit 87180a0 Mar 19, 2026
28 checks passed
@dfpetrin dfpetrin deleted the docstring-fix branch March 19, 2026 18:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees

No one assigned

Labels

changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@dfpetrin @leanprover-bot @TwoFX