bookshelf/lakefile.lean

import Lake

open System Lake DSL

package «bookshelf»

-- ========================================
-- Imports
-- ========================================

require Cli from git
  "https://github.com/mhuisi/lean4-cli" @
    "nightly"
require CMark from git
  "https://github.com/xubaiw/CMark.lean" @
    "main"
require UnicodeBasic from git
  "https://github.com/fgdorais/lean4-unicode-basic" @
    "main"
require leanInk from git
  "https://github.com/hargonix/LeanInk" @
    "doc-gen"
require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @
    "master"
require std from git
  "https://github.com/leanprover/std4.git" @
    "main"

-- ========================================
-- Documentation Generator
-- ========================================

lean_lib DocGen4

lean_exe «doc-gen4» {
  root := `Main
  supportInterpreter := true
}

/--
Turns a Github git remote URL into an HTTPS Github URL.
Three link types from git supported:
- https://github.com/org/repo
- https://github.com/org/repo.git
- git@github.com:org/repo.git
TODO: This function is quite brittle and very Github specific, we can
probably do better.
-/
def getGithubBaseUrl (gitUrl : String) : String := Id.run do
  let mut url := gitUrl
  if url.startsWith "git@" then
    url := url.drop 15
    url := url.dropRight 4
    return s!"https://github.com/{url}"
  else if url.endsWith ".git" then
    return url.dropRight 4
  else
    return url

/--
Obtain the Github URL of a project by parsing the origin remote.
-/
def getProjectGithubUrl (directory : System.FilePath := "." ) : IO String := do
  let out ← IO.Process.output {
    cmd := "git",
    args := #["remote", "get-url", "origin"],
    cwd := directory
  }
  if out.exitCode != 0 then
    throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the git remote in {directory}"
  return out.stdout.trimRight

/--
Obtain the git commit hash of the project that is currently getting analyzed.
-/
def getProjectCommit (directory : System.FilePath := "." ) : IO String := do
  let out ← IO.Process.output {
    cmd := "git",
    args := #["rev-parse", "HEAD"]
    cwd := directory
  }
  if out.exitCode != 0 then
    throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the current commit in {directory}"
  return out.stdout.trimRight

def getGitUrl (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do
  let baseUrl := getGithubBaseUrl (← getProjectGithubUrl pkg.dir)
  let commit ← getProjectCommit pkg.dir

  let parts := mod.name.components.map toString
  let path := String.intercalate "/" parts
  let libPath := pkg.config.srcDir / lib.srcDir
  let basePath := String.intercalate "/" (libPath.components.filter (· != "."))
  let url := s!"{baseUrl}/blob/{commit}/{basePath}/{path}.lean"
  return url

module_facet docs (mod) : FilePath := do
  let some docGen4 ← findLeanExe? `«doc-gen4»
    | error "no doc-gen4 executable configuration found in workspace"
  let exeJob ← docGen4.exe.fetch
  let modJob ← mod.leanArts.fetch
  let ws ← getWorkspace
  let pkg ← ws.packages.find? (·.isLocalModule mod.name)
  let libConfig ← pkg.leanLibConfigs.toArray.find? (·.isLocalModule mod.name)
  -- Build all documentation imported modules
  let imports ← mod.imports.fetch
  let depDocJobs ← BuildJob.mixArray <| ← imports.mapM fun mod => fetch <| mod.facet `docs
  let gitUrl ← getGitUrl pkg libConfig mod
  let buildDir := ws.root.buildDir
  let docFile := mod.filePath (buildDir / "doc") "html"
  depDocJobs.bindAsync fun _ depDocTrace => do
  exeJob.bindAsync fun exeFile exeTrace => do
  modJob.bindSync fun _ modTrace => do
    let depTrace := mixTraceArray #[exeTrace, modTrace, depDocTrace]
    let trace ← buildFileUnlessUpToDate docFile depTrace do
      logStep s!"Documenting module: {mod.name}"
      proc {
        cmd := exeFile.toString
        args := #["single", mod.name.toString, gitUrl]
        env := ← getAugmentedEnv
      }
    return (docFile, trace)

-- TODO: technically speaking this facet does not show all file dependencies
target coreDocs : FilePath := do
  let some docGen4 ← findLeanExe? `«doc-gen4»
    | error "no doc-gen4 executable configuration found in workspace"
  let exeJob ← docGen4.exe.fetch
  let basePath := (←getWorkspace).root.buildDir / "doc"
  let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
  exeJob.bindSync fun exeFile exeTrace => do
    let trace ← buildFileUnlessUpToDate dataFile exeTrace do
      logStep "Documenting Lean core: Init and Lean"
      proc {
        cmd := exeFile.toString
        args := #["genCore"]
        env := ← getAugmentedEnv
      }
    return (dataFile, trace)

library_facet docs (lib) : FilePath := do
  -- Ordering is important. The index file is generated by walking through the
  -- filesystem directory. Files copied from the shell scripts need to exist
  -- prior to this.
  let mods ← lib.modules.fetch
  let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
  let coreJob : BuildJob FilePath ← coreDocs.fetch
  let exeJob ← «doc-gen4».fetch
  -- Shared with DocGen4.Output
  let basePath := (←getWorkspace).root.buildDir / "doc"
  let dataFile := basePath / "declarations" / "declaration-data.bmp"
  let staticFiles := #[
    basePath / "style.css",
    basePath / "declaration-data.js",
    basePath / "color-scheme.js",
    basePath / "nav.js",
    basePath / "jump-src.js",
    basePath / "expand-nav.js",
    basePath / "how-about.js",
    basePath / "search.js",
    basePath / "mathjax-config.js",
    basePath / "instances.js",
    basePath / "importedBy.js",
    basePath / "index.html",
    basePath / "404.html",
    basePath / "navbar.html",
    basePath / "search.html",
    basePath / "find" / "index.html",
    basePath / "find" / "find.js",
    basePath / "src"  / "alectryon.css",
    basePath / "src"  / "alectryon.js",
    basePath / "src"  / "docutils_basic.css",
    basePath / "src"  / "pygments.css"
  ]
  coreJob.bindAsync fun _ coreInputTrace => do
    exeJob.bindAsync fun exeFile exeTrace => do
      moduleJobs.bindSync fun _ inputTrace => do
        let depTrace := mixTraceArray #[inputTrace, exeTrace, coreInputTrace]
        let trace ← buildFileUnlessUpToDate dataFile depTrace do
          logInfo "Documentation indexing"
          proc {
            cmd := exeFile.toString
            args := #["index"]
          }
        let traces ← staticFiles.mapM computeTrace
        let indexTrace := mixTraceArray traces

        return (dataFile, trace.mix indexTrace)

-- ========================================
-- Bookshelf
-- ========================================

@[default_target]
lean_lib «Bookshelf» {
  roots := #[`Bookshelf, `Common]
}

/--
The contents of our `.env` file.
-/
structure Config where
  port : Nat := 5555

/--
Read in the `.env` file into an in-memory structure.
-/
private def readConfig : StateT Config ScriptM Unit := do
  let env <- IO.FS.readFile ".env"
  for line in env.trim.split (fun c => c == '\n') do
    match line.split (fun c => c == '=') with
    | ["PORT", port] => modify (fun c => { c with port := String.toNat! port })
    | _ => error "Malformed `.env` file."
  return ()

/--
Start an HTTP server for locally serving documentation. It is expected the
documentation has already been generated prior via

```bash
> lake build Bookshelf:docs
```

USAGE:
  lake run server
-/
script server (_args) do
  let ((), config) <- StateT.run readConfig {}
  IO.println s!"Running Lean on `http://localhost:{config.port}`"
  _ <- IO.Process.run {
    cmd := "python3",
    args := #["-m", "http.server", toString config.port, "-d", "build/doc"],
  }
  return 0