2021-11-27 15:19:56 +00:00
|
|
|
import DocGen4
|
|
|
|
|
import Lean
|
|
|
|
|
|
2021-12-05 13:56:25 +00:00
|
|
|
open DocGen4 Lean IO
|
2021-11-27 15:19:56 +00:00
|
|
|
|
2021-12-05 13:56:25 +00:00
|
|
|
def main (args : List String) : IO Unit := do
|
|
|
|
|
let modules := args
|
|
|
|
|
let path ← lakeSetupSearchPath (←getLakePath) modules.toArray
|
|
|
|
|
IO.println s!"Loading modules from: {path}"
|
|
|
|
|
let doc ← load $ modules.map Name.mkSimple
|
2021-12-15 11:02:05 +00:00
|
|
|
IO.println "Outputting HTML"
|
2021-12-12 12:21:53 +00:00
|
|
|
htmlOutput doc
|
