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.
192 lines
8.7 KiB
Text
192 lines
8.7 KiB
Text
"Foo structure is just a test "
|
||
"main name "
|
||
"documentation for the second field "
|
||
"documenting test axiom "
|
||
doc string for 'Boo' is not available
|
||
"Boo constructor has a custom name "
|
||
"Boo.x docString "
|
||
doc string for 'Boo.y' is not available
|
||
"inductive datatype Tree documentation "
|
||
"Tree.node documentation "
|
||
"Tree.leaf stores the values "
|
||
"documenting definition in namespace "
|
||
"We can document 'where' functions too\n\n... and indentation is stripped, even after an empty line. "
|
||
doc string for 'f' is not available
|
||
"let rec documentation at f "
|
||
doc string for 'g' is not available
|
||
"let rec documentation at g "
|
||
"Gadget for optional parameter support.\n\nA binder like `(x : α := default)` in a declaration is syntax sugar for\n`x : optParam α default`, and triggers the elaborator to attempt to use\n`default` to supply the argument if it is not supplied.\n"
|
||
"Auxiliary declaration used to implement named patterns like `x@h:p`. "
|
||
"Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues building the telescope if it is a `forall`.\n\nIf `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.\n\nIf `whnfType` is `true`, we give `k` the `whnf` of the resulting type. This is a free operation.\n"
|
||
Foo :=
|
||
{ range := { pos := { line := 3, column := 0 },
|
||
charUtf16 := 0,
|
||
endPos := { line := 6, column := 58 },
|
||
endCharUtf16 := 58 },
|
||
selectionRange := { pos := { line := 4, column := 10 },
|
||
charUtf16 := 10,
|
||
endPos := { line := 4, column := 13 },
|
||
endCharUtf16 := 13 } }
|
||
Foo.name :=
|
||
{ range := { pos := { line := 5, column := 19 },
|
||
charUtf16 := 19,
|
||
endPos := { line := 5, column := 23 },
|
||
endCharUtf16 := 23 },
|
||
selectionRange := { pos := { line := 5, column := 19 },
|
||
charUtf16 := 19,
|
||
endPos := { line := 5, column := 23 },
|
||
endCharUtf16 := 23 } }
|
||
Foo.val :=
|
||
{ range := { pos := { line := 6, column := 44 },
|
||
charUtf16 := 44,
|
||
endPos := { line := 6, column := 47 },
|
||
endCharUtf16 := 47 },
|
||
selectionRange := { pos := { line := 6, column := 44 },
|
||
charUtf16 := 44,
|
||
endPos := { line := 6, column := 47 },
|
||
endCharUtf16 := 47 } }
|
||
myAxiom :=
|
||
{ range := { pos := { line := 8, column := 0 },
|
||
charUtf16 := 0,
|
||
endPos := { line := 9, column := 19 },
|
||
endCharUtf16 := 19 },
|
||
selectionRange := { pos := { line := 9, column := 6 },
|
||
charUtf16 := 6,
|
||
endPos := { line := 9, column := 13 },
|
||
endCharUtf16 := 13 } }
|
||
Boo :=
|
||
{ range := { pos := { line := 11, column := 0 },
|
||
charUtf16 := 0,
|
||
endPos := { line := 15, column := 12 },
|
||
endCharUtf16 := 12 },
|
||
selectionRange := { pos := { line := 11, column := 10 },
|
||
charUtf16 := 10,
|
||
endPos := { line := 11, column := 13 },
|
||
endCharUtf16 := 13 } }
|
||
Boo.makeBoo :=
|
||
{ range := { pos := { line := 13, column := 2 },
|
||
charUtf16 := 2,
|
||
endPos := { line := 13, column := 9 },
|
||
endCharUtf16 := 9 },
|
||
selectionRange := { pos := { line := 13, column := 2 },
|
||
charUtf16 := 2,
|
||
endPos := { line := 13, column := 9 },
|
||
endCharUtf16 := 9 } }
|
||
Boo.x :=
|
||
{ range := { pos := { line := 14, column := 27 },
|
||
charUtf16 := 27,
|
||
endPos := { line := 14, column := 28 },
|
||
endCharUtf16 := 28 },
|
||
selectionRange := { pos := { line := 14, column := 27 },
|
||
charUtf16 := 27,
|
||
endPos := { line := 14, column := 28 },
|
||
endCharUtf16 := 28 } }
|
||
Boo.y :=
|
||
{ range := { pos := { line := 15, column := 4 },
|
||
charUtf16 := 4,
|
||
endPos := { line := 15, column := 5 },
|
||
endCharUtf16 := 5 },
|
||
selectionRange := { pos := { line := 15, column := 4 },
|
||
charUtf16 := 4,
|
||
endPos := { line := 15, column := 5 },
|
||
endCharUtf16 := 5 } }
|
||
Tree :=
|
||
{ range := { pos := { line := 17, column := 0 },
|
||
charUtf16 := 0,
|
||
endPos := { line := 20, column := 56 },
|
||
endCharUtf16 := 56 },
|
||
selectionRange := { pos := { line := 18, column := 10 },
|
||
charUtf16 := 10,
|
||
endPos := { line := 18, column := 14 },
|
||
endCharUtf16 := 14 } }
|
||
Tree.rec :=
|
||
{ range := { pos := { line := 17, column := 0 },
|
||
charUtf16 := 0,
|
||
endPos := { line := 20, column := 56 },
|
||
endCharUtf16 := 56 },
|
||
selectionRange := { pos := { line := 18, column := 10 },
|
||
charUtf16 := 10,
|
||
endPos := { line := 18, column := 14 },
|
||
endCharUtf16 := 14 } }
|
||
Tree.casesOn :=
|
||
{ range := { pos := { line := 17, column := 0 },
|
||
charUtf16 := 0,
|
||
endPos := { line := 20, column := 56 },
|
||
endCharUtf16 := 56 },
|
||
selectionRange := { pos := { line := 18, column := 10 },
|
||
charUtf16 := 10,
|
||
endPos := { line := 18, column := 14 },
|
||
endCharUtf16 := 14 } }
|
||
Tree.node :=
|
||
{ range := { pos := { line := 19, column := 2 },
|
||
charUtf16 := 2,
|
||
endPos := { line := 19, column := 64 },
|
||
endCharUtf16 := 64 },
|
||
selectionRange := { pos := { line := 19, column := 35 },
|
||
charUtf16 := 35,
|
||
endPos := { line := 19, column := 39 },
|
||
endCharUtf16 := 39 } }
|
||
Tree.leaf :=
|
||
{ range := { pos := { line := 20, column := 2 },
|
||
charUtf16 := 2,
|
||
endPos := { line := 20, column := 56 },
|
||
endCharUtf16 := 56 },
|
||
selectionRange := { pos := { line := 20, column := 39 },
|
||
charUtf16 := 39,
|
||
endPos := { line := 20, column := 43 },
|
||
endCharUtf16 := 43 } }
|
||
Bla.test :=
|
||
{ range := { pos := { line := 24, column := 0 },
|
||
charUtf16 := 0,
|
||
endPos := { line := 31, column := 16 },
|
||
endCharUtf16 := 16 },
|
||
selectionRange := { pos := { line := 25, column := 4 },
|
||
charUtf16 := 4,
|
||
endPos := { line := 25, column := 8 },
|
||
endCharUtf16 := 8 } }
|
||
Bla.test.aux :=
|
||
{ range := { pos := { line := 31, column := 2 },
|
||
charUtf16 := 2,
|
||
endPos := { line := 31, column := 16 },
|
||
endCharUtf16 := 16 },
|
||
selectionRange := { pos := { line := 31, column := 2 },
|
||
charUtf16 := 2,
|
||
endPos := { line := 31, column := 5 },
|
||
endCharUtf16 := 5 } }
|
||
f :=
|
||
{ range := { pos := { line := 35, column := 0 },
|
||
charUtf16 := 0,
|
||
endPos := { line := 39, column := 14 },
|
||
endCharUtf16 := 14 },
|
||
selectionRange := { pos := { line := 35, column := 4 },
|
||
charUtf16 := 4,
|
||
endPos := { line := 35, column := 5 },
|
||
endCharUtf16 := 5 } }
|
||
f.foo :=
|
||
{ range := { pos := { line := 36, column := 44 },
|
||
charUtf16 := 44,
|
||
endPos := { line := 38, column := 22 },
|
||
endCharUtf16 := 22 },
|
||
selectionRange := { pos := { line := 36, column := 44 },
|
||
charUtf16 := 44,
|
||
endPos := { line := 36, column := 47 },
|
||
endCharUtf16 := 47 } }
|
||
g :=
|
||
{ range := { pos := { line := 41, column := 0 },
|
||
charUtf16 := 0,
|
||
endPos := { line := 45, column := 7 },
|
||
endCharUtf16 := 7 },
|
||
selectionRange := { pos := { line := 41, column := 4 },
|
||
charUtf16 := 4,
|
||
endPos := { line := 41, column := 5 },
|
||
endCharUtf16 := 5 } }
|
||
g.foo :=
|
||
{ range := { pos := { line := 42, column := 44 },
|
||
charUtf16 := 44,
|
||
endPos := { line := 44, column := 22 },
|
||
endCharUtf16 := 22 },
|
||
selectionRange := { pos := { line := 42, column := 44 },
|
||
charUtf16 := 44,
|
||
endPos := { line := 42, column := 47 },
|
||
endCharUtf16 := 47 } }
|
||
docStr.lean:106:0-107:20: error: invalid 'add_decl_doc', declaration is in an imported module
|