Access lake workspace during elaboration

Stream: metaprogramming / tactics

[Christian Merten]

Is there a way to get the current docs#Lake.Workspace (if lake is running) in say CommandElabM? I managed to obtain a Lake.LoadConfig, but this is not enough as far as I can tell:

import Lean
import Lake.CLI.Main

open Lean Elab Command

elab "#foobaz" : command => do
  let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall?
  let config ← liftIO <| Lake.MonadError.runEIO <|
    Lake.mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
  logInfo s!"{config.lakeDir}"

#foobaz

More specifically, I would like to get a list of the dependencies of the current project in a command.

[Anne Baanen]

You might find some useful code in Mathlib's scripts/lint-style.lean, which uses Lake to parse options from the Lakefile.

[Anne Baanen]

On the other hand, maybe it would be easier to parse lake-manifest.json yourself?

[Christian Merten]

The code you linked to unfortunately calls getWorkspaceRoot which in turn calls Lake.loadWorkspace. Running this in a command triggers an infinite recursion:

import Lean
import Lake.CLI.Main

open Lean Elab Command

elab "#foobaz" : command => do
  let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall?
  let config ← liftIO <| Lake.MonadError.runEIO <|
    Lake.mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
  let some workspace ← Lake.loadWorkspace config |>.toBaseIO
    | throwError "failed to load Lake workspace"
  IO.println "hi"

#foobaz

[Christian Merten]

Anne Baanen said:

On the other hand, maybe it would be easier to parse lake-manifest.json yourself?

This is what I have been doing, but seems a bit hacky. That's why I asked if there is a intended way to do this. But thanks, I guess I'll stick to manual parsing for now.