add docstring

Mdgen.lean

@@ -1,5 +1,6 @@
 import Mdgen.Cli
 
+set_option linter.missingDocs false
 
 def main (args : List String) : IO UInt32 :=
   mkMdgenCmd.validate args

Mdgen/Cli.lean

@@ -4,6 +4,7 @@ import Cli
 
 open Cli System FilePath
 
+/-- what `mdgen` does -/
 def runMdgenCmd (p : Parsed) : IO UInt32 := do
   let inputDir : FilePath := p.positionalArg! "input_dir" |>.as! String
   let outputDir : FilePath := p.positionalArg! "output_dir" |>.as! String
@@ -22,6 +23,7 @@ def runMdgenCmd (p : Parsed) : IO UInt32 := do
     createFile (path := outputFilePath) (content := newContent)
   return 0
 
+/-- API definition of `mdgen` command -/
 def mkMdgenCmd : Cmd := `[Cli|
   mdgen VIA runMdgenCmd; ["1.5.0"]
   "mdgen is a tool to generate .md files from .lean files."

Mdgen/ConvertToMd.lean

@@ -2,6 +2,7 @@ import Mdgen.File
 
 open System FilePath
 
+/-- intermediate data structure -/
 structure RichLine where
   /-- text content -/
   content : String
@@ -48,7 +49,10 @@ def analysis (lines : List String) : List RichLine := Id.run do
 
 /-- A chunk of grouped code for conversion to markdown. -/
 structure Block where
+  /-- content of block -/
   content : String
+
+  /-- whether the `content` is converted into code section in markdown -/
   toCodeBlock : Bool
   deriving Repr
 
@@ -64,6 +68,7 @@ def List.spanWithEdge {α : Type} (p : α → Bool) (as : List α) : List α ×
   | [] => (l, [])
   | y :: ys => (l ++ [y], ys)
 
+/-- build a `Block` from a `RichLine` -/
 partial def buildBlocks (lines : List RichLine) : List Block :=
   match lines with
   | [] => []
@@ -88,6 +93,7 @@ partial def buildBlocks (lines : List RichLine) : List Block :=
 /-- markdown text -/
 abbrev Md := String
 
+/-- convert a `Block` intro a markdown snippet -/
 def Block.toMd (b : Block) : Md :=
   if b.content == "" then
     ""
@@ -105,6 +111,7 @@ instance : ToString Block where
   toString := fun b =>
     s!"content: \n{b.content}\n toCodeBlock: {b.toCodeBlock}\n\n"
 
+/-- merge blocks and build a markdown content -/
 def mergeBlocks (blocks : List Block) : Md :=
   let res := blocks
     |>.map Block.toMd

Mdgen/Test/ConvertToMd.lean

@@ -2,6 +2,7 @@ import Mdgen.ConvertToMd
 
 namespace analysis
 
+/-- test for `analysis` function -/
 def runTest (input : List String) (expected : List (Nat × Bool)) (title := "") : IO Unit :=
   let output := analysis input |>.map (fun x => (x.level, x.close))
   if output = expected then
@@ -77,9 +78,11 @@ end analysis
 
 namespace ConvertToMd
 
+/-- add breakline for each element in a list -/
 def _root_.List.withBreakLine (as : List String) : String :=
   as.map (· ++ "\n") |>.foldl (· ++ ·) ""
 
+/-- test for `convertToMd` -/
 def runTest (input : List String) (expected : List String) (title := "") : IO Unit :=
   let output := convertToMd (lines := input)
   if output = expected.withBreakLine then

lakefile.lean

@@ -9,7 +9,8 @@ package «mdgen» where
   -- add package configuration options here
   leanOptions := #[
     ⟨`autoImplicit, false⟩,
-    ⟨`relaxedAutoImplicit, false⟩
+    ⟨`relaxedAutoImplicit, false⟩,
+    ⟨`linter.missingDocs, true⟩
   ]
 
 @[default_target]