|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Lean FRO LLC. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Author: David Thrane Christiansen |
| 5 | +-/ |
| 6 | +import Lake |
| 7 | +import Lake.Load.Lean |
| 8 | +import Lake.Load.Package |
| 9 | + |
| 10 | +import SubVerso.Compat |
| 11 | +import SubVerso.Highlighting.Code |
| 12 | +import SubVerso.Module |
| 13 | + |
| 14 | +import Manual.Meta.LakeToml.PackageTest |
| 15 | + |
| 16 | +/-! |
| 17 | +# Lean-format Lakefile Extractor |
| 18 | +
|
| 19 | +This executable elaborates a Lean-format `lakefile.lean` and emits, as JSON: |
| 20 | +
|
| 21 | + * `package`: the elaborated `Lake.Package`, formatted with the same `Manual.Toml.Test` instances |
| 22 | + used to render the “expected elaboration result” for TOML lakefiles. This is the analog of what |
| 23 | + `checkTomlPackage` produces for a `lakefile.toml`, so that the `lakeLean` directive can validate |
| 24 | + it against an `expected` block exactly as `lakeToml` does. |
| 25 | +
|
| 26 | + * `module`: the SubVerso highlighted representation of the lakefile source, so that the `lakeLean` |
| 27 | + directive can render the configuration with full syntax highlighting and hover information. |
| 28 | +
|
| 29 | +The implementation is based on `leanprover/verso-slides#21`: a Lean-format lakefile cannot be |
| 30 | +elaborated by the ordinary module extractor, because it imports `Lake` and uses the package |
| 31 | +configuration DSL (`package`, `lean_lib`, `lean_exe`, …). It must therefore be elaborated by a |
| 32 | +process that statically links Lake's DSL, which is what this executable does. |
| 33 | +-/ |
| 34 | + |
| 35 | +open SubVerso |
| 36 | +open SubVerso.Highlighting (Highlighted highlightFrontendResult) |
| 37 | +open SubVerso.Module (ModuleItem) |
| 38 | + |
| 39 | +open Lean Elab System |
| 40 | +open Lean.Elab.Command hiding Context |
| 41 | +open Lean.Elab.Frontend |
| 42 | + |
| 43 | +/-- Returns the node kind of the command, skipping outer `in` nodes. -/ |
| 44 | +partial def commandKind (cmd : Syntax) : SyntaxNodeKind := |
| 45 | + match cmd with |
| 46 | + | `(command|$_cmd1 in $cmd2) => commandKind cmd2 |
| 47 | + | _ => cmd.getKind |
| 48 | + |
| 49 | +/-- |
| 50 | +Reconstruct a `Lake.Package` from the environment produced by elaborating a configuration file. |
| 51 | +Mirrors `Lake.loadLeanConfig`, but operates on an already-elaborated environment so that the same |
| 52 | +elaboration can also be highlighted. |
| 53 | +-/ |
| 54 | +def extractPackage (env : Environment) (opts : Options := {}) : Lake.LogIO Lake.Package := do |
| 55 | + let fileCfg ← Lake.LakefileConfig.loadFromEnv env opts |
| 56 | + let .ok lakeEnv ← (Lake.Env.compute {home := ""} {sysroot := ""} none none).toBaseIO |
| 57 | + | Lake.error "Failed to compute a Lake environment" |
| 58 | + -- The recorded package directory and configuration file are canonical rather than the actual |
| 59 | + -- (temporary) location of the example, so that the elaboration result is deterministic. |
| 60 | + let loadCfg : Lake.LoadConfig := { |
| 61 | + lakeEnv, wsDir := ".", pkgDir := ".", |
| 62 | + relConfigFile := "lakefile.lean", configFile := "lakefile.lean" |
| 63 | + } |
| 64 | + return Lake.mkPackage loadCfg fileCfg |
| 65 | + |
| 66 | +/-- |
| 67 | +Elaborate the configuration file at `configFile`, returning both the elaborated `Lake.Package` |
| 68 | +and the SubVerso highlighting of its source. |
| 69 | +-/ |
| 70 | +unsafe def extract (realConfigFile : FilePath) : |
| 71 | + IO (Lake.Package × SubVerso.Module.Module) := do |
| 72 | + initSearchPath (← findSysroot) |
| 73 | + |
| 74 | + -- The recorded package directory and configuration file are canonical rather than the actual |
| 75 | + -- (temporary) location of the example, so that the elaboration result is deterministic. |
| 76 | + let pkgDir : FilePath := "." |
| 77 | + let relConfigFile : FilePath := "lakefile.lean" |
| 78 | + |
| 79 | + let contents ← IO.FS.readFile realConfigFile |
| 80 | + let fm := FileMap.ofString contents |
| 81 | + let ictx := Parser.mkInputContext contents relConfigFile.toString |
| 82 | + let (headerStx, parserState, msgs) ← Parser.parseHeader ictx |
| 83 | + let imports := headerToImports headerStx |
| 84 | + |
| 85 | + -- Lake's DSL macros and attributes are registered via initializers, so they must run when the |
| 86 | + -- configuration's imports are loaded. |
| 87 | + enableInitializersExecution |
| 88 | + let env ← importModules imports {} (trustLevel := 1024) (loadExts := true) |
| 89 | + |
| 90 | + -- Configure the Lake DSL environment extensions exactly as `Lake.elabConfigFile` does, so that |
| 91 | + -- the package's name and directory defaults resolve the way Lake would resolve them. |
| 92 | + let env := env.setMainModule Lake.configModuleName |
| 93 | + let env := Lake.nameExt.setState env ⟨0, .anonymous⟩ |
| 94 | + let env := Lake.dirExt.setState env (some pkgDir) |
| 95 | + let env := Lake.optsExt.setState env (some {}) |
| 96 | + |
| 97 | + let pctx : Context := { inputCtx := ictx } |
| 98 | + let commandState : Command.State := { env, maxRecDepth := defaultMaxRecDepth, messages := msgs } |
| 99 | + -- `pp.tagAppFns` makes the highlighter associate constants with their applications. |
| 100 | + let scopes := |
| 101 | + let sc := commandState.scopes[0]! |
| 102 | + { sc with opts := sc.opts.setBool `pp.tagAppFns true } :: commandState.scopes.tail! |
| 103 | + let commandState := { commandState with scopes } |
| 104 | + let cmdSt ← IO.mkRef { commandState, parserState, cmdPos := parserState.pos } |
| 105 | + |
| 106 | + let res ← Compat.Frontend.processCommands headerStx pctx cmdSt |
| 107 | + |
| 108 | + let finalState ← cmdSt.get |
| 109 | + let finalEnv := finalState.commandState.env |
| 110 | + if finalState.commandState.messages.hasErrors then |
| 111 | + let errs ← finalState.commandState.messages.toList.filterMapM fun m => do |
| 112 | + if m.severity == .error then pure (some (← m.toString)) else pure none |
| 113 | + throw <| .userError s!"{realConfigFile}: configuration has errors:\n{"\n".intercalate errs}" |
| 114 | + |
| 115 | + -- Extract the elaborated package configuration. |
| 116 | + let some pkg ← (extractPackage finalEnv).toBaseIO |
| 117 | + | throw <| .userError s!"{realConfigFile}: failed to load package configuration" |
| 118 | + |
| 119 | + -- Highlight the source. |
| 120 | + let res := res.updateLeading contents |
| 121 | + let hls ← (Frontend.runCommandElabM <| liftTermElabM <| |
| 122 | + highlightFrontendResult res (suppressNamespaces := [])) pctx cmdSt |
| 123 | + let items : Array ModuleItem := hls.zip res.syntax |>.map fun (hl, stx) => { |
| 124 | + defines := hl.definedNames.toArray |
| 125 | + kind := commandKind stx |
| 126 | + range := stx.getRange?.map fun ⟨s, e⟩ => (fm.toPosition s, fm.toPosition e) |
| 127 | + code := hl |
| 128 | + } |
| 129 | + |
| 130 | + return (pkg, SubVerso.Module.Module.mk items) |
| 131 | + |
| 132 | +structure Args where |
| 133 | + lakefile : String |
| 134 | + jsonFile : String |
| 135 | + pkgDir? : Option String := none |
| 136 | + |
| 137 | +def processArgs (args : List String) : IO Args := do |
| 138 | + let rec go (pkgDir? : Option String) (positional : Array String) : |
| 139 | + List String → IO Args |
| 140 | + | "--pkg-dir" :: dir :: more => go (some dir) positional more |
| 141 | + | arg :: more => go pkgDir? (positional.push arg) more |
| 142 | + | [] => |
| 143 | + match positional.toList with |
| 144 | + | [lakefile, jsonFile] => pure { lakefile, jsonFile, pkgDir? } |
| 145 | + | other => throw <| .userError s!"\ |
| 146 | + Expected: [--pkg-dir DIR] LAKEFILE OUT\n\ |
| 147 | + where LAKEFILE is the path to a Lean-format lakefile and OUT is the destination of \ |
| 148 | + the JSON.\n\ |
| 149 | + Got positional arguments: {other}" |
| 150 | + go none #[] args |
| 151 | + |
| 152 | +unsafe def main (args : List String) : IO UInt32 := do |
| 153 | + try |
| 154 | + let { lakefile, jsonFile, .. } ← processArgs args |
| 155 | + let (pkg, mod) ← extract lakefile |
| 156 | + let package := (Manual.Toml.Test.toString pkg).pretty ++ "\n" |
| 157 | + let out := Json.mkObj [ |
| 158 | + ("package", Json.str package), |
| 159 | + ("module", mod.toJson) |
| 160 | + ] |
| 161 | + if let some parent := (jsonFile : FilePath).parent then |
| 162 | + IO.FS.createDirAll parent |
| 163 | + IO.FS.writeFile jsonFile (toString out) |
| 164 | + return (0 : UInt32) |
| 165 | + catch e => |
| 166 | + IO.eprintln s!"extract-lakefile: {toString e}" |
| 167 | + return (1 : UInt32) |
0 commit comments