Script acting on current lib but provided by external lib

Stream: lean4

[Patrick Massot]

I’m slowly working on improving the UX for leanblueprint and I reached the point where I need to check that some declaration names exists in the current project. Say I want a blueprint for FLT. The python side of leanblueprint creates a text file with declaration names, with one name per line. Say this file is called lean_decls.txt. I would like to simply add a line to flt/lakefile.lean which says

require checkdecls from from git "https://github.com/leanprover-community/checkdecls.git"

and then, from inside the flt folder, I want to be able to run lake exe checkdecls lean_decls.txt and that should execute some code sitting at the – currently non-existent – https://github.com/leanprover-community/checkdecls.git that either succeeds (i.e. exists with a zero exit code) or prints the list of non-existing declaration if the main target lib designated in flt/lakefile.lean (including declaration defined in libs imported by flt). I have no trouble writing meta code that check whether a name is in the current environment. What I don’t know about is the required lake magic to execute a script defined by a required lib and make sure it has access to the current library.

[Patrick Massot]

I guess this is mostly a question for @Mac Malone but @Mario Carneiro and everybody else is welcome to answer. There is extra credit for answers that wouldn’t break every month with each new Lean release.

[Mario Carneiro]

@Patrick Massot The extra credit is hard (I believe this program already looked different in v4.5.0), but it is now possible (though awkward) to access properties of the current lake project by using the lake API. Here's an implementation of your checkdecls command, minus the file parsing part:

lakefile.lean:

package test
lean_lib Test

lean_exe checkdecls where
  root := `CheckDecls.Main
  supportInterpreter := true

Test.lean:

def foo := 1

CheckDecls/Main.lean:

import Lake.CLI.Main
open Lake Lean

def main : IO UInt32 := do
  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
  let config ← MonadError.runEIO <| mkLoadConfig.{0} { elanInstall?, leanInstall?, lakeInstall? }
  let ws ← MonadError.runEIO <| (loadWorkspace config).run (.eio .normal)
  let imports := ws.root.leanLibs.concatMap (·.config.roots.map fun module => { module })
  let env ← Lean.importModules imports {}
  let mut ok := true
  for n in [`Nat, `foo, `bar] do
    unless env.contains n do
      println! "{n} is missing"
      ok := false
  return if ok then 0 else 1

result:

$ lake exe checkdecls
info: [1/3] Building CheckDecls.Main
info: [2/3] Compiling CheckDecls.Main
info: [3/3] Linking checkdecls
bar is missing

The CheckDecls exe can be defined in a dependency. This implementation looks at all lean_libs - originally I wrote it to use only the default_target ones but lean_exe targets have inaccessible module names which makes them a bit weird. In practice you will only have one lean_lib so this should be fine.

[Patrick Massot]

Thanks! Don’t worry, the extra credit part was a joke. I know this isn’t currently possible (but one can still dream).

[Patrick Massot]

@Mario Carneiro this doesn’t seem to work. I pushed your code at https://github.com/PatrickMassot/checkdecls and then if I had to the sphere eversion project lakefile a line saying

require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"

and run inside the sphere eversion repo lake exe checkdecls then I get the error message

uncaught exception: unknown package 'SphereEversion'
You might need to open '/home/pmassot/lean/sphere-eversion' as a workspace in your editor

[Mario Carneiro]

did you compile the project first?

[Patrick Massot]

Ah. Maybe not.

[Patrick Massot]

Indeed this fixes the issue. Thanks! And sorry about the noise.

[Patrick Massot]

The hilarious thing is that this script reports bar is missing from the Sphere eversion project, but foo is ok (and it’s true).