bookshelf-doc/Main.lean

82 lines
2.4 KiB
Plaintext
Raw Normal View History

2021-11-27 15:19:56 +00:00
import DocGen4
import Lean
2022-02-23 21:54:10 +00:00
import Cli
2021-11-27 15:19:56 +00:00
2022-02-23 21:54:10 +00:00
open DocGen4 Lean Cli
2021-11-27 15:19:56 +00:00
def getTopLevelModules (p : Parsed) : IO (List String) := do
let topLevelModules := p.variableArgsAs! String |>.toList
if topLevelModules.length == 0 then
2022-07-23 11:01:25 +00:00
throw <| IO.userError "No topLevelModules provided."
return topLevelModules
def runSingleCmd (p : Parsed) : IO UInt32 := do
2022-08-11 19:37:10 +00:00
let relevantModules := [p.positionalArg! "module" |>.as! String |> String.toName]
let res ← lakeSetup
match res with
| Except.ok ws =>
let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules
IO.println "Outputting HTML"
2023-03-09 20:37:13 +00:00
let baseConfig ← getSimpleBaseContext hierarchy
2022-08-11 19:37:10 +00:00
htmlOutputResults baseConfig doc ws (p.hasFlag "ink")
return 0
2022-08-11 19:37:10 +00:00
| Except.error rc => pure rc
2022-02-23 21:54:10 +00:00
2022-07-23 11:04:36 +00:00
def runIndexCmd (_p : Parsed) : IO UInt32 := do
2022-07-26 10:52:41 +00:00
let hierarchy ← Hierarchy.fromDirectory Output.basePath
2023-03-09 20:37:13 +00:00
let baseConfig ← getSimpleBaseContext hierarchy
htmlOutputIndex baseConfig
return 0
2022-08-11 19:37:10 +00:00
def runGenCoreCmd (_p : Parsed) : IO UInt32 := do
let res ← lakeSetup
match res with
| Except.ok ws =>
2022-08-11 19:37:10 +00:00
let (doc, hierarchy) ← loadCore
IO.println "Outputting HTML"
2023-03-09 20:37:13 +00:00
let baseConfig ← getSimpleBaseContext hierarchy
2022-08-11 19:37:10 +00:00
htmlOutputResults baseConfig doc ws (ink := False)
return 0
| Except.error rc => pure rc
2022-08-11 19:37:10 +00:00
def runDocGenCmd (_p : Parsed) : IO UInt32 := do
IO.println "You most likely want to use me via Lake now, check my README on Github on how to:"
IO.println "https://github.com/leanprover/doc-gen4"
return 0
def singleCmd := `[Cli|
single VIA runSingleCmd;
"Only generate the documentation for the module it was given, might contain broken links unless all documentation is generated."
FLAGS:
2022-07-26 11:56:22 +00:00
ink; "Render the files with LeanInk in addition"
ARGS:
module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules."
]
2022-07-21 19:12:15 +00:00
def indexCmd := `[Cli|
index VIA runIndexCmd;
"Index the documentation that has been generated by single."
2022-07-21 17:07:35 +00:00
ARGS:
...topLevelModule : String; "The top level modules this documentation will be for."
]
2022-08-11 19:37:10 +00:00
def genCoreCmd := `[Cli|
genCore VIA runGenCoreCmd;
"Generate documentation for the core Lean modules: Init and Lean since they are not Lake projects"
2022-08-11 19:37:10 +00:00
]
2022-02-23 21:54:10 +00:00
def docGenCmd : Cmd := `[Cli|
2022-08-11 19:37:10 +00:00
"doc-gen4" VIA runDocGenCmd; ["0.1.0"]
2022-02-23 21:54:10 +00:00
"A documentation generator for Lean 4."
SUBCOMMANDS:
singleCmd;
2022-08-11 19:37:10 +00:00
indexCmd;
genCoreCmd
2022-02-23 21:54:10 +00:00
]
def main (args : List String) : IO UInt32 :=
docGenCmd.validate args