Using Environment.evalConst

Stream: lean4

[Amir Livne Bar-on]

I'm trying to look at exported values (for introspection scripts in the Equational Theories project), and I can't get Environment.evalConst to work.

I've been able to reproduce with a small example, based on the initial repo generated by lake. This is Main.lean:

import Lean.Util.SearchPath
import Testimport

open Lean

def main : IO Unit := do
  IO.println s!"Hello, {hello}!"

  searchPathRef.set compile_time_search_path%
  let env ← importModules #[{module := `Testimport}] {} (trustLevel := 1024)
  match unsafe Environment.evalConst String env {} `Testimport.Basic.hello with
  | Except.ok value =>
    IO.println s!"Hello, {value}!"
  | Except.error err =>
    IO.println err

When running this (after allowing the interpreter in the lakefile) I'm getting this output:

Hello, world!
unknown declaration 'Testimport.Basic.hello'

What am I doing wrong? How can I access exported values by name?

[Sebastian Ullrich]

I don't think the definition is namespaced? Try `hello

[Amir Livne Bar-on]

Yes, this works. But the analogue doesn't work in the equational theories project, I'll try to dig into why.

[Amir Livne Bar-on]

The definitions I'm interested in ("equations") are defined through a tag declaration extension. The relevant part of the code is

initialize magmaLawExt : TagDeclarationExtension ← mkTagDeclarationExtension

elab mods:declModifiers tk:"equation " i:num " := " tsyn:term : command => Command.liftTermElabM do
  [...]
  let lawName := .mkSimple s!"Law{i.getNat}"
  addDecl <| .defnDecl {
    name := lawName
    [...]
  }
  addMarkup lawName
  [...]
  modifyEnv (magmaLawExt.tag · lawName)

and in the extraction script I have

env.find? `Law1

finding the expression for the definition, but

unsafe Environment.evalConst Law.NatMagmaLaw env {} `Law1

failing to evaluate it (with unknown declaration).

[Sebastian Ullrich]

You should use addAndCompile in that case instead of addDecl

[Mario Carneiro]

sorry, mea culpa

[Amir Livne Bar-on]

Mario Carneiro said:

sorry, mea culpa

Are you changing this? I don't feel comfortable touching this foundational part of the code (though I verified it works in our case)

[Mario Carneiro]

yes I'm writing the PR

[Mario Carneiro]

equational#530