unable to get definition constants in enviroment

Stream: general

[Frederick Pu]

when running this

unsafe def main : IO Unit := do
  let input ← IO.FS.readFile "testfile.lean"
  let fileMap := FileMap.ofString input
  let inputCtx := Parser.mkInputContext input fileName.toString
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  let (env, messages) ← processHeader header {} messages inputCtx
  let imports := env.imports
  let commandState := Command.mkState env messages
  let s ← IO.processCommands inputCtx parserState { commandState with infoState.enabled := true }
  let envAfter := s.commandState.env
  IO.println (envAfter.constants.toList.map (·.1))

as an executable (with supportInterpreter := true), I'm only able to get the constants for the inductive types and not the constants for definitions in the file

[Aaron Liu]

what's in the testfile.lean

[Frederick Pu]

inductive MyNat where
| zero : MyNat
| succ : MyNat -> MyNat

def somefun (x : Nat) : Nat := 2 * x

[Frederick Pu]

the constants for MyNat are showing up but not somefun

[Frederick Pu]

and what's weirder is that if you do #eval (do let env ← getEnv; IO.println (env.constants.toList.map (·.1)) : Lean.MetaM Unit) in testfile.lean the somefun will actually show up

[Aaron Liu]

what if you use MyNat instead of Nat in the definition of somefun

[Aaron Liu]

of course the contents will have to be something other than 2 * x (since multiplication isn't defined on MyNat)

[Frederick Pu]

i dont think that wiill solve it sinc ethe issue is that somefun will get garbage collected

[Frederick Pu]

yeah it doesn't fixx it

[Aaron Liu]

ok I'll have a look later when I can run this locally

[Sebastian Ullrich]

Are you sure the messages are in fact empty?

[Sebastian Ullrich]

Of s as well

[Frederick Pu]

i dont see any messages

[Frederick Pu]

when i print them

[Frederick Pu]

i just realized the mwe i gave earlier doesnt compile. Please refer to this one:

import Lean

open Lean Meta Elab Core

unsafe def main : IO Unit := do
  let input ← IO.FS.readFile "testfile.lean"
  let fileMap := FileMap.ofString input
  let inputCtx := Parser.mkInputContext input "testfile.lean"
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  let (env, messages) ← processHeader header {} messages inputCtx
  let imports := env.imports
  let commandState := Command.mkState env messages
  let s ← IO.processCommands inputCtx parserState { commandState with infoState.enabled := true }
  let envAfter := s.commandState.env
  IO.println (envAfter.constants.toList.map (·.1))

[Frederick Pu]

lakefile:

lean_exe mwe where
  root := `Tactic.MWE
  supportInterpreter := true

[Frederick Pu]

and testfile.lean:

inductive MyNat where
| zero : MyNat
| succ : MyNat -> MyNat

def somefun (x : Nat) : Nat := 2 * x

[Frederick Pu]

and running lake env .lake/build/bin/mwe

[James E Hanson]

Frederick Pu said:

i just realized the mwe i gave earlier doesnt compile. Please refer to this one:

import Lean

open Lean Meta Elab Core

unsafe def main : IO Unit := do
  let input ← IO.FS.readFile "testfile.lean"
  let fileMap := FileMap.ofString input
  let inputCtx := Parser.mkInputContext input "testfile.lean"
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  let (env, messages) ← processHeader header {} messages inputCtx
  let imports := env.imports
  let commandState := Command.mkState env messages
  let s ← IO.processCommands inputCtx parserState { commandState with infoState.enabled := true }
  let envAfter := s.commandState.env
  IO.println (envAfter.constants.toList.map (·.1))

You're not doing anything with fileMap anymore. Is that intentional?

[Frederick Pu]

oh yeah i was using the filemap for somethine else in my main script

[Frederick Pu]

but not relevant for mwe

[Frederick Pu]

also for some reason this works as intended:

import Lean

open Lean Elab Meta

def somefun (x y : Nat) : Nat := x + y

#eval (do let env ← getEnv; let mm := env.getModuleIdx? env.mainModule; IO.println (((← getEnv).constants.toList.map (·.1)).filter (fun x => env.getModuleIdxFor? x == mm)): MetaM Unit)

[Frederick Pu]

but the corresponding version with executable doesn't work

[Frederick Pu]

also the let imports := env.imports is not used either

[Frederick Pu]

so ig an even more minified version would be:

import Lean

open Lean Meta Elab Core

unsafe def main : IO Unit := do
  let input ← IO.FS.readFile "testfile.lean"
  let inputCtx := Parser.mkInputContext input "testfile.lean"
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  let (env, messages) ← processHeader header {} messages inputCtx
  let commandState := Command.mkState env messages
  let s ← IO.processCommands inputCtx parserState { commandState with infoState.enabled := true }
  let envAfter := s.commandState.env
  IO.println (envAfter.constants.toList.map (·.1))

[Frederick Pu]

so it turns out I just had to do Lean.initSearchPath (← Lean.findSysroot) at the start

[Frederick Pu]

but now i'm getting issue where if testfile.lean has a compilation error i can't catch it:

inductive MyNat where
| zero : MyNat
| succ : MyNat -> MyNat

theorem womp : + 2 = 4 := by sorry

def somefun (x : Nat) : Nat := 2 * x

[Frederick Pu]

even when printing messages i don't get anything:

import Lean

open Lean Meta Elab Core

unsafe def main : IO Unit := do
  Lean.initSearchPath (← Lean.findSysroot)
  enableInitializersExecution
  let input ← IO.FS.readFile "testfile.lean"
  let fileMap := FileMap.ofString input
  let inputCtx := Parser.mkInputContext input "testfile.lean"
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  let (env, messages) ← processHeader header {} messages inputCtx
  IO.println (messages.toArray.map (·.caption))
  let imports := env.imports
  let commandState := Command.mkState env messages
  let s ← IO.processCommands inputCtx parserState { commandState with infoState.enabled := true } <&> Frontend.State.commandState
  IO.println (s.messages.toArray.map (·.caption))
  let envAfter := s.env
  -- IO.println (env.constants.toList.map (·.1))
  let mm := env.getModuleIdx? env.mainModule;
  IO.println ((envAfter.constants.toList.map (·.1)).filter (fun x => env.getModuleIdxFor? x == mm))