feat: lake: `require` doc comments

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

Closed tydeu closed 2 weeks ago

tydeu commented 2 weeks ago

Lake now supports docstrings on require commands:

/-- This is a docstring for a require statement. -/
require std from ...

Closes #2898.

tydeu commented 2 weeks ago

Split from #3174.

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-4057 build this PR didn't complete normally. (2024-05-02 22:34:39) View Log