diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 486561d..7c3399e 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -21,4 +21,4 @@ jobs: - name: lean action uses: leanprover/lean-action@v1 with: - build-args: "--fail-level=warning" + build-args: "--fail-level=warning --log-level=warning" diff --git a/Mdgen/Analysis.lean b/Mdgen/Analysis.lean new file mode 100644 index 0000000..926a2f1 --- /dev/null +++ b/Mdgen/Analysis.lean @@ -0,0 +1,128 @@ +import Mdgen.File + +open System FilePath + +/-- intermediate data structure which is annotated syntax infomation -/ +structure RichLine where + /-- text content -/ + content : String + + /-- nest level -/ + level : Nat + + /-- whether the line ends with the closing symbol or not. -/ + close : Bool +deriving Repr, BEq, Inhabited + +instance : ToString RichLine where + toString := RichLine.content + +/-- handle ignore pattern -/ +def filterIgnored (lines : List String) : List String := Id.run do + let mut res := [] + let mut ignore := false + for line in lines do + if line.endsWith "--#" then + continue + if line.endsWith "--#--" then + ignore := ! ignore + continue + if ignore then + continue + res := line :: res + return res.reverse + +/-- Receive a list of codes and count the nesting of block and sectioning comments. +* The corresponding opening and closing brackets should have the same level. +* Also handles the exclusion of ignored targets. +-/ +def analysis (lines : List String) : List RichLine := Id.run do + let mut res : List RichLine := [] + let mut level := 0 + let mut doc := false + for line in (filterIgnored lines) do + if line.startsWith "/--" then + doc := true + if line.startsWith "/-" && ! line.startsWith "/--" && ! doc then + level := level + 1 + res := {content := line, level := level, close := line.endsWith "-/" && ! doc} :: res + if line.endsWith "-/" then + if ! doc then + level := level - 1 + doc := false + return res.reverse + +namespace Analysis + +set_option linter.unusedVariables false in + +/-- test for `analysis` function -/ +def runTest (title := "") (input : List String) (expected : List (Nat × Bool)) : IO Unit := do + let output := analysis input |>.map (fun x => (x.level, x.close)) + if output ≠ expected then + throw <| .userError s!"Test failed: \n{output}" + +#eval runTest + (title := "nested block comment") + [ + "/-", + "/- inline -/", + "/- multi", + "line -/", + "hoge", + "-/", + "foo" + ] + [(1, false), (2, true), (2, false), (2, true), (1, false), (1, true), (0, false)] + +#eval runTest + (title := "sectioning comment and nested block comment") + [ + "/-! hoge fuga", + "/- foo! -/", + "-/", + "def foo := 1", + ] + [(1, false), (2, true), (1, true), (0, false)] + +#eval runTest + (title := "one line doc comment") + [ + "/-- hoge -/", + "def hoge := \"hoge\"", + ] + [(0, false), (0, false)] + +#eval runTest + (title := "multi line doc comment") + [ + "/-- hoge", + "fuga -/", + "def hoge := 42", + ] + [(0, false), (0, false), (0, false)] + +#eval runTest + (title := "raw code block") + [ + "/-", + "```lean", + "/-- greeting -/", + "def foo := \"Hello World!\"", + "```", + "-/", + ] + [(1, false), (1, false), (1, false), (1, false), (1, false), (1, true)] + +#eval runTest + (title := "multi line ignoring") + [ + "--#--", + "this is ignored", + "this is also ignored", + "--#--", + "hoge", + ] + [(0, false)] + +end Analysis diff --git a/Mdgen/Cli.lean b/Mdgen/Cli.lean index ebb1489..c7e7b41 100644 --- a/Mdgen/Cli.lean +++ b/Mdgen/Cli.lean @@ -33,7 +33,7 @@ def runMdgenCmd (p : Parsed) : IO UInt32 := do /-- API definition of `mdgen` command -/ def mkMdgenCmd : Cmd := `[Cli| - mdgen VIA runMdgenCmd; ["1.6.0"] + mdgen VIA runMdgenCmd; ["1.7.0"] "mdgen is a tool to generate .md files from .lean files." FLAGS: diff --git a/Mdgen/ConvertToMd.lean b/Mdgen/ConvertToMd.lean index e9cfe2c..ca26fa2 100644 --- a/Mdgen/ConvertToMd.lean +++ b/Mdgen/ConvertToMd.lean @@ -1,51 +1,4 @@ -import Mdgen.File - -open System FilePath - -/-- intermediate data structure -/ -structure RichLine where - /-- text content -/ - content : String - - /-- nest level -/ - level : Nat - - /-- whether the line ends with the closing symbol or not. -/ - close : Bool - deriving Repr, BEq, Inhabited - -instance : ToString RichLine where - toString := fun l => l.content - -/-- Receive a list of codes and count the nesting of block and sectioning comments. -* The corresponding opening and closing brackets should have the same level. -* Also handles the exclusion of ignored targets. --/ -def analysis (lines : List String) : List RichLine := Id.run do - let mut res : List RichLine := [] - let mut level := 0 - let mut doc := false - let mut ignore := false - for line in lines do - -- ignore pattern - if line.endsWith "--#" then - continue - if line.endsWith "--#--" then - ignore := ! ignore - continue - if ignore then - continue - - if line.startsWith "/--" then - doc := true - if line.startsWith "/-" && ! line.startsWith "/--" then - level := level + 1 - res := {content := line, level := level, close := line.endsWith "-/" && ! doc} :: res - if line.endsWith "-/" then - if ! doc then - level := level - 1 - doc := false - return res.reverse +import Mdgen.Analysis /-- A chunk of grouped code for conversion to markdown. -/ structure Block where @@ -118,7 +71,10 @@ def mergeBlocks (blocks : List Block) : Md := |>.foldl (· ++ ·) "" res.trim ++ "\n" -/-- convert `#{root}` in internal link to repeated `../` string -/ +open System FilePath + +/-- Handle uniform internal link syntax. +This converts `#{root}` in internal link to repeated `../` string -/ def Block.postProcess (outputFilePath outputDir : FilePath) (b : Block) : Block := Id.run do if b.toCodeBlock then return b @@ -142,3 +98,251 @@ def convertToMd (outputFilePath outputDir : Option FilePath := none) (lines : Li | _, _ => blocks mergeBlocks postProcessedBlocks + +namespace ConvertToMd + +/-- add breakline for each element in a list -/ +def _root_.List.withBreakLine (as : List String) : String := + as.map (· ++ "\n") |>.foldl (· ++ ·) "" + +set_option linter.unusedVariables false in + +/-- test for `convertToMd` -/ +def runTest (input : List String) (expected : List String) (title := "") : IO Unit := do + let output := convertToMd (lines := input) + if output ≠ expected.withBreakLine then + throw <| .userError s!"Test failed: \n{output}" + +#eval runTest + (title := "inline comment") + ["-- this is a test"] + [ + "```lean", + "-- this is a test", + "```" + ] + +#eval runTest + (title := "module document") + ["/-! # This is a test -/"] + ["# This is a test"] + +#eval runTest + (title := "multi line sectioning comment") + [ + "/-! # This is a test", + "of multiline section comment -/" + ] + [ + "# This is a test", + "of multiline section comment" + ] + +#eval runTest + (title := "empty lines") + ["/-! test -/", "", "", ""] + ["test"] + +#eval runTest + (title := "ignored lines") + ["this is ignored --#", "this is also ignored --#"] + [""] + +#eval runTest + (title := "doc comment") + [ + "/-- This is a test -/", + "def foo := 0" + ] + [ + "```lean", + "/-- This is a test -/", + "def foo := 0", + "```" + ] + +#eval runTest + (title := "multi line doc comment") + [ + "/-- This is a test", + "of multiline doc comment -/", + "def foo := 0" + ] + [ + "```lean", + "/-- This is a test", + "of multiline doc comment -/", + "def foo := 0", + "```" + ] + +#eval runTest + (title := "block comment in doc comment") + [ + "/-- foo", + "bar /- hoge -/", + "baz -/", + ] + [ + "```lean", + "/-- foo", + "bar /- hoge -/", + "baz -/", + "```" + ] + +#eval runTest + (title := "leading block comment in doc comment") + [ + "/-- foo", + "/- hoge bar -/", + "baz -/", + ] + [ + "```lean", + "/-- foo", + "/- hoge bar -/", + "baz -/", + "```" + ] + +#eval runTest + (title := "block comment") + ["/- this is a test -/"] + ["this is a test"] + +#eval runTest + (title := "multi line block comment") + [ + "/-", + "this is a test", + "of multiline block comment -/", + ] + [ + "this is a test", + "of multiline block comment" + ] + +#eval runTest + (title := "respect indent") + [ + "hoge", + " fuga", + " monyo", + ] + [ + "```lean", + "hoge", + " fuga", + " monyo", + "```" + ] + +#eval runTest + (title := "consecutive single-line block comments.") + [ + "/- hoge -/", + "/- fuga -/", + ] + [ + "hoge", + "", + "fuga" + ] + +#eval runTest + (title := "nested block comment") + [ + "/-", + "this is a test", + "/- nested comment -/", + "of nested block comment -/" + ] + [ + "this is a test", + "/- nested comment -/", + "of nested block comment" + ] + +#eval runTest + (title := "raw code block") + [ + "/-", + "```lean", + "/- this is test -/", + "```", + "fuga", + "-/", + "/- hoge -/", + ] + [ + "```lean", + "/- this is test -/", + "```", + "fuga", + "", + "hoge" + ] + +#eval runTest + (title := "indent in raw code block") + [ + "/-", + "```lean", + " hoge", + "```", + "-/" + ] + [ + "```lean", + " hoge", + "```" + ] + +#eval runTest + (title := "doc comment in raw code block") + [ + "/-", + "```lean", + "/-- foo -/", + "def zero := 0", + "```", + "-/", + ] + [ + "```lean", + "/-- foo -/", + "def zero := 0", + "```" + ] + +#eval runTest + (title := "multiple raw code blocks") + [ + "/-", + "```lean", + "/-- greeting -/", + "def foo := \"Hello World!\"", + "```", + "", + "```lean", + "/-! ### second code block -/", + "", + "def one := 1", + "```", + "-/", + ] + [ + "```lean", + "/-- greeting -/", + "def foo := \"Hello World!\"", + "```", + "", + "```lean", + "/-! ### second code block -/", + "", + "def one := 1", + "```", + ] + +end ConvertToMd diff --git a/Mdgen/File.lean b/Mdgen/File.lean index e6b2507..3971638 100644 --- a/Mdgen/File.lean +++ b/Mdgen/File.lean @@ -1,4 +1,4 @@ -open System +open System FilePath /-- A new list created by removing the matching parts of two lists from the beginning. -/ def List.diff (as : List String) (bs : List String) : List String := @@ -8,6 +8,10 @@ def List.diff (as : List String) (bs : List String) : List String := | [], _ => [] | a :: as, b :: bs => if a == b then List.diff as bs else a :: as +#guard List.diff ["test", "src", "first"] ["test", "src"] = ["first"] + +#guard List.diff ["test", "src", "first"] ["test", "out"] = ["src", "first"] + namespace System.FilePath /-- generate a filepath from path components -/ @@ -26,6 +30,16 @@ def outputFilePath (inputDir : List String) (outputDir : List String) |> List.filter (· ≠ ".") |> ofComponents +#guard outputFilePath ["."] ["out"] ["foo.lean"] = ofComponents ["out", "foo.md"] + +#guard outputFilePath ["src"] ["."] ["src", "foo.lean"] = ofComponents ["foo.md"] + +#guard outputFilePath ["src"] ["out"] ["src", "foo.lean"] = ofComponents ["out", "foo.md"] + +#guard outputFilePath ["test", "src"] ["test", "out"] ["test", "src", "foo.lean"] = ofComponents ["test", "out", "foo.md"] + +#guard outputFilePath ["src"] ["out", "dist"] ["src", "foo", "bar.lean"] = ofComponents ["out", "dist", "foo", "bar.md"] + /-- Recursively outputs a list of the paths of lean files contained in a directory whose path is `fp`. -/ partial def getLeanFilePaths (fp : FilePath) (acc : Array FilePath := #[]) : diff --git a/Mdgen/Test.lean b/Mdgen/Test.lean deleted file mode 100644 index 3c8283f..0000000 --- a/Mdgen/Test.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Mdgen.Test.File -import Mdgen.Test.ConvertToMd diff --git a/Mdgen/Test/ConvertToMd.lean b/Mdgen/Test/ConvertToMd.lean deleted file mode 100644 index 378bccc..0000000 --- a/Mdgen/Test/ConvertToMd.lean +++ /dev/null @@ -1,295 +0,0 @@ -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 - IO.println s!"{title} test passed!" - else - throw <| .userError s!"Test failed: \n{output}" - -#eval runTest - (title := "nested block comment") - [ - "/-", - "/- inline -/", - "/- multi", - "line -/", - "hoge", - "-/", - "foo" - ] - [(1, false), (2, true), (2, false), (2, true), (1, false), (1, true), (0, false)] - -#eval runTest - (title := "sectioning comment and nested block comment") - [ - "/-! hoge fuga", - "/- foo! -/", - "-/", - "def foo := 1", - ] - [(1, false), (2, true), (1, true), (0, false)] - -#eval runTest - (title := "one line doc comment") - [ - "/-- hoge -/", - "def hoge := \"hoge\"", - ] - [(0, false), (0, false)] - -#eval runTest - (title := "multi line doc comment") - [ - "/-- hoge", - "fuga -/", - "def hoge := 42", - ] - [(0, false), (0, false), (0, false)] - -#eval runTest - (title := "raw code block") - [ - "/-", - "```lean", - "/-- greeting -/", - "def foo := \"Hello World!\"", - "```", - "-/", - ] - [(1, false), (1, false), (1, false), (1, false), (1, false), (1, true)] - -#eval runTest - (title := "multi line ignoring") - [ - "--#--", - "this is ignored", - "this is also ignored", - "--#--", - "hoge", - ] - [(0, false)] - -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 - IO.println s!"{title} test passed!" - else - throw <| .userError s!"Test failed: \n{output}" - -#eval runTest - (title := "inline comment") - ["-- this is a test"] - [ - "```lean", - "-- this is a test", - "```" - ] - -#eval runTest - (title := "module document") - ["/-! # This is a test -/"] - ["# This is a test"] - -#eval runTest - (title := "multi line sectioning comment") - [ - "/-! # This is a test", - "of multiline section comment -/" - ] - [ - "# This is a test", - "of multiline section comment" - ] - -#eval runTest - (title := "empty lines") - ["/-! test -/", "", "", ""] - ["test"] - -#eval runTest - (title := "ignored lines") - ["this is ignored --#", "this is also ignored --#"] - [""] - -#eval runTest - (title := "doc comment") - [ - "/-- This is a test -/", - "def foo := 0" - ] - [ - "```lean", - "/-- This is a test -/", - "def foo := 0", - "```" - ] - -#eval runTest - (title := "multi line doc comment") - [ - "/-- This is a test", - "of multiline doc comment -/", - "def foo := 0" - ] - [ - "```lean", - "/-- This is a test", - "of multiline doc comment -/", - "def foo := 0", - "```" - ] - -#eval runTest - (title := "block comment") - ["/- this is a test -/"] - ["this is a test"] - -#eval runTest - (title := "multi line block comment") - [ - "/-", - "this is a test", - "of multiline block comment -/", - ] - [ - "this is a test", - "of multiline block comment" - ] - -#eval runTest - (title := "respect indent") - [ - "hoge", - " fuga", - " monyo", - ] - [ - "```lean", - "hoge", - " fuga", - " monyo", - "```" - ] - -#eval runTest - (title := " consecutive single-line block comments.") - [ - "/- hoge -/", - "/- fuga -/", - ] - [ - "hoge", - "", - "fuga" - ] - -#eval runTest - (title := "nested block comment") - [ - "/-", - "this is a test", - "/- nested comment -/", - "of nested block comment -/" - ] - [ - "this is a test", - "/- nested comment -/", - "of nested block comment" - ] - -#eval runTest - (title := "raw code block") - [ - "/-", - "```lean", - "/- this is test -/", - "```", - "fuga", - "-/", - "/- hoge -/", - ] - [ - "```lean", - "/- this is test -/", - "```", - "fuga", - "", - "hoge" - ] - -#eval runTest - (title := "indent in raw code block") - [ - "/-", - "```lean", - " hoge", - "```", - "-/" - ] - [ - "```lean", - " hoge", - "```" - ] - -#eval runTest - (title := "doc comment in raw code block") - [ - "/-", - "```lean", - "/-- foo -/", - "def zero := 0", - "```", - "-/", - ] - [ - "```lean", - "/-- foo -/", - "def zero := 0", - "```" - ] - -#eval runTest - (title := "multiple raw code blocks") - [ - "/-", - "```lean", - "/-- greeting -/", - "def foo := \"Hello World!\"", - "```", - "", - "```lean", - "/-! ### second code block -/", - "", - "def one := 1", - "```", - "-/", - ] - [ - "```lean", - "/-- greeting -/", - "def foo := \"Hello World!\"", - "```", - "", - "```lean", - "/-! ### second code block -/", - "", - "def one := 1", - "```", - ] - -end ConvertToMd diff --git a/Mdgen/Test/File.lean b/Mdgen/Test/File.lean deleted file mode 100644 index 7af57e8..0000000 --- a/Mdgen/Test/File.lean +++ /dev/null @@ -1,17 +0,0 @@ -import Mdgen.File - -open System FilePath - -#guard List.diff ["test", "src", "first"] ["test", "src"] = ["first"] - -#guard List.diff ["test", "src", "first"] ["test", "out"] = ["src", "first"] - -#guard outputFilePath ["."] ["out"] ["foo.lean"] = ofComponents ["out", "foo.md"] - -#guard outputFilePath ["src"] ["."] ["src", "foo.lean"] = ofComponents ["foo.md"] - -#guard outputFilePath ["src"] ["out"] ["src", "foo.lean"] = ofComponents ["out", "foo.md"] - -#guard outputFilePath ["test", "src"] ["test", "out"] ["test", "src", "foo.lean"] = ofComponents ["test", "out", "foo.md"] - -#guard outputFilePath ["src"] ["out", "dist"] ["src", "foo", "bar.lean"] = ofComponents ["out", "dist", "foo", "bar.md"] diff --git a/Test/Exp/First.md b/Test/Exp/First.md index 1393ddc..d27ec79 100644 --- a/Test/Exp/First.md +++ b/Test/Exp/First.md @@ -38,6 +38,12 @@ example (h : P) : P ∨ Q := by -/ apply Or.inl exact h + +/-- doc comment + +/- test of block comment in doc -/ +-/ +macro "foo" : term => `(0) ``` ## nested comment diff --git a/Test/Src/First.lean b/Test/Src/First.lean index 5f260b3..24565b9 100644 --- a/Test/Src/First.lean +++ b/Test/Src/First.lean @@ -49,6 +49,12 @@ example (h : P) : P ∨ Q := by apply Or.inl exact h +/-- doc comment + +/- test of block comment in doc -/ +-/ +macro "foo" : term => `(0) + /- ## nested comment Here is a sample of nested block comment: /- Hi. I am a nested comment! -/ diff --git a/lakefile.lean b/lakefile.lean index 634baf4..7e77978 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL package «mdgen» where - version := v!"1.6.0" + version := v!"1.7.0" keywords := #["cli", "markdown"] description := "Tool to generate markdown files from lean files."