bookshelf-doc/Main.lean

74 lines
2.3 KiB
Plaintext

import DocGen4
import Lean
import Cli
open DocGen4 Lean Cli
def getTopLevelModules (p : Parsed) : IO (List String) := do
let topLevelModules := p.variableArgsAs! String |>.toList
if topLevelModules.length == 0 then
throw <| IO.userError "No topLevelModules provided."
return topLevelModules
def runSingleCmd (p : Parsed) : IO UInt32 := do
let relevantModules := #[p.positionalArg! "module" |>.as! String |> String.toName]
let gitUrl := p.positionalArg! "gitUrl" |>.as! String
let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules
let baseConfig ← getSimpleBaseContext hierarchy
htmlOutputResults baseConfig doc (some gitUrl) (p.hasFlag "ink")
return 0
def runIndexCmd (_p : Parsed) : IO UInt32 := do
let hierarchy ← Hierarchy.fromDirectory Output.basePath
let baseConfig ← getSimpleBaseContext hierarchy
htmlOutputIndex baseConfig
return 0
def runGenCoreCmd (_p : Parsed) : IO UInt32 := do
let (doc, hierarchy) ← loadCore
let baseConfig ← getSimpleBaseContext hierarchy
htmlOutputResults baseConfig doc none (ink := False)
return 0
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:
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."
gitUrl : String; "The gitUrl as computed by the Lake facet"
]
def indexCmd := `[Cli|
index VIA runIndexCmd;
"Index the documentation that has been generated by single."
ARGS:
...topLevelModule : String; "The top level modules this documentation will be for."
]
def genCoreCmd := `[Cli|
genCore VIA runGenCoreCmd;
"Generate documentation for the core Lean modules: Init and Lean since they are not Lake projects"
]
def docGenCmd : Cmd := `[Cli|
"doc-gen4" VIA runDocGenCmd; ["0.1.0"]
"A documentation generator for Lean 4."
SUBCOMMANDS:
singleCmd;
indexCmd;
genCoreCmd
]
def main (args : List String) : IO UInt32 :=
docGenCmd.validate args