use docComment for statement description
This commit is contained in:
Jon Eugster
+43
-10
@@ -27,8 +27,9 @@ and `World` strings can be anything.
|
||||
The core of a level is the `Statement`, which is the exercise that should be proven:
|
||||
|
||||
```lean
|
||||
/-- For all natural numbers $n$, we have $0 + n = n$. -/
|
||||
@[simp]
|
||||
Statement MyNat.zero_add
|
||||
"For all natural numbers $n$, we have $0 + n = n$."
|
||||
(n : ℕ) : 0 + n = n := by
|
||||
Hint "You can start a proof by `induction n`."
|
||||
induction n with n hn
|
||||
@@ -44,17 +45,47 @@ Statement MyNat.zero_add
|
||||
rfl
|
||||
```
|
||||
|
||||
The first two arguments (name, attributes, and description) are optional. Thereafter you have a statement and a proof.
|
||||
##### Proof
|
||||
|
||||
- The proof should always be a tactic proof, i.e. the `:= by` is mandatory.
|
||||
- In the proof you can use `Hint "text"` to display text if the goal state in-game matches the one where `Hint` is placed. For more options about hints, see below.
|
||||
- In the proof you can add a `Branch` that runs an alternativ tactic sequence, which helps setting `Hints` in different places. The `Branch` does not affect the main proof and does not need to finish any goals.
|
||||
- If you specify a name (`MyNat.zero_add`), this lemma will be available in future levels. (Note that a future level must also import this level, so that Lean knows about the added statement). The name must be *fully qualified*.
|
||||
- If you add a description (i.e. non-Lean exercise statement), it will be shown above the exercise. It supports Markdown (including katex).
|
||||
The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
|
||||
|
||||
There are a few extra tactics that help you structuring the proof:
|
||||
|
||||
- `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
|
||||
the one where `Hint` is placed. For more options about hints, see below.
|
||||
- `Branch`: In the proof you can add a `Branch` that runs an alternativ tactic sequence, which
|
||||
helps setting `Hints` in different places. The `Branch` does not affect the main
|
||||
proof and does not need to finish any goals.
|
||||
- `Template`/`Hole`: not implemented yet, but used to provide a sample proof template.
|
||||
|
||||
##### Statement Name (optional)
|
||||
|
||||
If you specify a name (`MyNat.zero_add`), this lemma will be available in future levels.
|
||||
(Note that a future level must also import this level,
|
||||
so that Lean knows about the added statement).
|
||||
|
||||
The name must be *fully qualified*. (TODO: is that still true? Did we implement namespaces?)
|
||||
|
||||
##### Doc Comment (optional)
|
||||
|
||||
There are three places where the documentation comment appears:
|
||||
|
||||
1. as doc comment when hovering over the theorem
|
||||
2. as exercise description at the top of the level: ``Theorem `zero_add`: yada yada.``
|
||||
3. in the inventory. This can be overwritten by using
|
||||
`LemmaDoc MyNat.zero_add "different yada yada"` as one might want to add a more detailed
|
||||
description there including examples etc.
|
||||
|
||||
Both latter points support Markdown (including katex).
|
||||
##### Attributes (optional)
|
||||
|
||||
the `@[ attributes ]` prefix should work just like you know it from the `theorem` keyword.
|
||||
|
||||
#### Introduction/Conclusion
|
||||
|
||||
Optionally, you can add a `Introduction "some text"` and `Conclusion "some text"` to your level. the introduction will always be visible on top, the conclusion is displayed once the level is solved.
|
||||
Optionally, you can add a `Introduction "some text"` and `Conclusion "some text"` to your level.
|
||||
The introduction will be shown at the beginning, the conclusion is displayed once the level
|
||||
is solved.
|
||||
|
||||
#### Lemmas/Tactics/Definitions
|
||||
|
||||
@@ -68,7 +99,8 @@ NewLemma MyNat.add_zero
|
||||
NewDefinition Nat
|
||||
```
|
||||
|
||||
Once added, items will be available in all future levels/worlds, unless you disable them for a particular level with
|
||||
Once added, items will be available in all future levels/worlds,
|
||||
unless you disable them for a particular level with
|
||||
|
||||
```lean
|
||||
DisabledTactic tauto
|
||||
@@ -82,7 +114,8 @@ OnlyTactic rw rfl apply
|
||||
OnlyLemma MyNat.add_zero
|
||||
```
|
||||
|
||||
Lastly, all items need documentation entries (which are imported in the level), see more about that below. There is also explains the `LemmaTab`
|
||||
Lastly, all items need documentation entries (which are imported in the level),
|
||||
see more about that below. There is also explains the `LemmaTab` keyword.
|
||||
|
||||
### World
|
||||
|
||||
|
||||
@@ -100,8 +100,8 @@ def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.g
|
||||
name := name
|
||||
category := if type == .Lemma then s!"{n.getPrefix}" else ""
|
||||
content := s })
|
||||
logInfoAt ref (m!"Missing {type} Documentation: {name}, used provided default (e.g. " ++
|
||||
m!"statement description) instead. If you want to write your own description, add " ++
|
||||
logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
|
||||
m!"docstring) instead. If you want to write a different description, add " ++
|
||||
m!"`{type}Doc {name}` somewhere above this statement.")
|
||||
|
||||
/-- Documentation entry of a tactic. Example:
|
||||
@@ -305,13 +305,18 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
|
||||
return {acc with definitions := acc.definitions.insertMany ns}
|
||||
) acc
|
||||
|
||||
#check expandOptDocComment?
|
||||
|
||||
/-- Define the statement of the current level. -/
|
||||
elab attrs:Lean.Parser.Term.attributes ? "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
|
||||
elab doc:docComment ? attrs:Parser.Term.attributes ?
|
||||
"Statement" statementName:ident ? sig:declSig val:declVal : command => do
|
||||
let lvlIdx ← getCurLevelIdx
|
||||
|
||||
let descr := match descr with
|
||||
| none => none
|
||||
| some s => s.getString
|
||||
let docContent : Option String := match doc with
|
||||
| none => none
|
||||
| some s => match s.raw[1] with
|
||||
| .atom _ val => val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
|
||||
| _ => none --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
|
||||
|
||||
-- Save the messages before evaluation of the proof.
|
||||
let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
|
||||
@@ -340,19 +345,19 @@ elab attrs:Lean.Parser.Term.attributes ? "Statement" statementName:ident ? descr
|
||||
-- in that case.
|
||||
logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
|
||||
m!"statement will be available in later levels:\n\n{origType}")
|
||||
let thmStatement ← `(command| $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
|
||||
let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
|
||||
elabCommand thmStatement
|
||||
-- Check that statement has a docs entry.
|
||||
checkInventoryDoc .Lemma name (name := fullName) (template := descr)
|
||||
checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
|
||||
|
||||
else
|
||||
let thmStatement ← `(command| $[$attrs:attributes]? theorem $name $sig $val)
|
||||
let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig $val)
|
||||
elabCommand thmStatement
|
||||
-- Check that statement has a docs entry.
|
||||
checkInventoryDoc .Lemma name (name := fullName) (template := descr)
|
||||
checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
|
||||
|
||||
| none =>
|
||||
let thmStatement ← `(command| $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
|
||||
let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
|
||||
elabCommand thmStatement
|
||||
|
||||
let msgs := (← get).messages
|
||||
@@ -402,7 +407,7 @@ elab attrs:Lean.Parser.Term.attributes ? "Statement" statementName:ident ? descr
|
||||
module := env.header.mainModule
|
||||
goal := sig,
|
||||
scope := scope,
|
||||
descrText := descr
|
||||
descrText := docContent
|
||||
statementName := match statementName with
|
||||
| none => default
|
||||
| some name => currNamespace ++ name.getId
|
||||
|
||||
@@ -7,10 +7,18 @@ Level 1
|
||||
|
||||
/- Missing doc -/
|
||||
|
||||
-- Shows warning on `foo.bar`:
|
||||
Statement foo.bar "some text" : 5 ≤ 7 := by
|
||||
-- Shows info on `foo.bar`:
|
||||
|
||||
/-- some text -/
|
||||
Statement foo.bar : 5 ≤ 7 := by
|
||||
simp
|
||||
|
||||
-- Shows warning on `foo.bar₂`:
|
||||
|
||||
Statement foo.bar2 : 3 ≤ 7 := by
|
||||
simp
|
||||
|
||||
|
||||
NewLemma foo.baz
|
||||
DisabledTactic tauto
|
||||
|
||||
@@ -20,7 +28,8 @@ DisabledTactic tauto
|
||||
-- test that the command also works inside a namespace
|
||||
namespace myNamespace
|
||||
|
||||
Statement anotherStatement "test" (n : Nat) : n + 0 = n := by
|
||||
/-- test -/
|
||||
Statement anotherStatement (n : Nat) : n + 0 = n := by
|
||||
rfl
|
||||
|
||||
end myNamespace
|
||||
@@ -29,7 +38,8 @@ end myNamespace
|
||||
|
||||
LemmaDoc add_zero as "add_zero" in "Nat" "(nothing)"
|
||||
|
||||
Statement add_zero "test" (n : Nat) : n + 0 = n := by
|
||||
/-- test -/
|
||||
Statement add_zero (n : Nat) : n + 0 = n := by
|
||||
rfl
|
||||
|
||||
Statement (n : Nat) : 0 + n = n := by
|
||||
@@ -47,3 +57,17 @@ NewLemma add_zero
|
||||
|
||||
theorem xy (n : Nat) : n + 0 = n := by
|
||||
simp
|
||||
|
||||
|
||||
|
||||
/-! Test that it is possible to add `simp` attribute. -/
|
||||
|
||||
/-- Doc comment -/
|
||||
@[simp]
|
||||
Statement My.add_comm (n m : Nat) : n + m = m + n := by
|
||||
rw [Nat.add_comm]
|
||||
|
||||
example (n m : Nat) : n + m = m + n := by
|
||||
simp
|
||||
|
||||
#check My.add_comm
|
||||
|
||||
Reference in New Issue
Block a user