mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
56 lines
1.8 KiB
Lean4
56 lines
1.8 KiB
Lean4
/-
|
|
Tests that when `doc.verso.module` is not explicitly set,
|
|
module docs fall back to the value of `doc.verso`.
|
|
-/
|
|
import Lean
|
|
|
|
-- Only set doc.verso, do not set doc.verso.module
|
|
set_option doc.verso true
|
|
|
|
/-!
|
|
Module docs should parse as Verso here (fallback from {option}`doc.verso`).
|
|
|
|
*Bold* and _italic_ and [link](example.com)
|
|
-/
|
|
|
|
open Lean Elab Term in
|
|
/--
|
|
info: Markdown:
|
|
Verso:
|
|
{ text := #[Lean.Doc.Block.para
|
|
#[Lean.Doc.Inline.text "Module docs should parse as Verso here (fallback from ",
|
|
Lean.Doc.Inline.other
|
|
{ name := `Lean.Doc.Data.Option val := Dynamic.mk `Lean.Doc.Data.Option _ }
|
|
#[Lean.Doc.Inline.code "doc.verso"],
|
|
Lean.Doc.Inline.text ")."],
|
|
Lean.Doc.Block.para
|
|
#[Lean.Doc.Inline.bold #[Lean.Doc.Inline.text "Bold"], Lean.Doc.Inline.text " and ",
|
|
Lean.Doc.Inline.emph #[Lean.Doc.Inline.text "italic"], Lean.Doc.Inline.text " and ",
|
|
Lean.Doc.Inline.link #[Lean.Doc.Inline.text "link"] "example.com", Lean.Doc.Inline.linebreak "\n"]],
|
|
sections := #[],
|
|
declarationRange := { pos := { line := 10, column := 0 },
|
|
charUtf16 := 0,
|
|
endPos := { line := 14, column := 2 },
|
|
endCharUtf16 := 2 } }
|
|
-/
|
|
#guard_msgs in
|
|
#eval show TermElabM Unit from do
|
|
IO.println "Markdown:"
|
|
for modDoc in (Lean.getMainModuleDoc (← getEnv)).toArray do
|
|
IO.println modDoc.doc
|
|
IO.println "Verso:"
|
|
for modDoc in (Lean.getMainVersoModuleDocs (← getEnv)).snippets do
|
|
IO.println <| repr modDoc
|
|
|
|
|
|
/--
|
|
{name}`fallbackDecl`
|
|
-/
|
|
def fallbackDecl := "hello"
|
|
|
|
open Lean Elab Command Term in
|
|
/-- info: `fallbackDecl` -/
|
|
#guard_msgs in
|
|
#eval show TermElabM Unit from do
|
|
(← findDocString? (← getEnv) ``fallbackDecl).forM (IO.println ·)
|