fix: Elaborate the source body in getFileEnv (#456)

* fix: getFileEnv elaborates the file body, not just imports

`getFileEnv` ran only `processHeaderCore`, so the returned environment
held the file's imports but none of its own definitions. As a result
`ix compile foo.lean` produced an env without foo's constants, and
`--only-const <name>` over the resulting `.ixe` could not resolve any
name defined in the source file (e.g. `myReflEq` in MinimalDefs).

Run the body through `IO.processCommands` (as `runFrontend` does) so the
environment includes the file's definitions. Also fixes `ix validate`
and `ix ingress`, which share `getFileEnv`.

* test: guard that getFileEnv loads the file body, not just imports

Adds `Tests.Ix.EnvBody`, run in the default suite: it loads the existing
`Tests/Ix/Fixtures/Export.lean` fixture via `getFileEnv` and asserts its
body definition (`inductive MyNat`) is present, alongside an imported
constant (`Nat`). The body assertion is red under the header-only
regression and green with the body-elaboration fix.

Author: samuelburnham

Ix/Meta.lean

@@ -41,7 +41,15 @@ def getFileEnv (path : FilePath) : IO Environment := do
   if messages.hasErrors then
     throw $ IO.userError $ "\n\n".intercalate $
       (← messages.toList.mapM (·.toString)).map (String.trimAscii · |>.toString)
-  return env
+  -- Elaborate the file body too, so the env contains the file's own
+  -- definitions and not just its imports.
+  let env := env.setMainModule default
+  let s ← IO.processCommands inputCtx parserState (Command.mkState env messages)
+  let cmdMessages := s.commandState.messages
+  if cmdMessages.hasErrors then
+    throw $ IO.userError $ "\n\n".intercalate $
+      (← cmdMessages.toList.mapM (·.toString)).map (String.trimAscii · |>.toString)
+  return s.commandState.env
 
 /-- Captures the current module and its imports at compile time. -/
 elab "this_file!" : term => do

Tests/Ix/EnvBody.lean

@@ -0,0 +1,34 @@
+/-
+Regression guard: `getFileEnv` must load a file's own definitions (its body),
+not only its imports.
+
+`getFileEnv` previously ran only `processHeaderCore`, so the environment it
+returned held the file's imports but none of its own constants — meaning
+`ix compile`/`validate`/`ingress` emitted an env missing the file's definitions.
+This loads an existing fixture (`Export.lean`, which defines `inductive MyNat`)
+and asserts that body definition is present, alongside an imported constant.
+-/
+
+module
+
+public import Ix.Meta
+public import LSpec
+public import Lean
+
+open LSpec
+
+namespace Tests.Ix.EnvBody
+
+/-- Path is relative to the repository root, which is the working directory when
+`lake test` runs the `IxTests` executable. -/
+def fixturePath : System.FilePath := "Tests/Ix/Fixtures/Export.lean"
+
+public def suite : IO LSpec.TestSeq := do
+  let env ← getFileEnv fixturePath
+  pure $
+    LSpec.test "getFileEnv includes the file body (not just imports)"
+      ((env.constants.find? `MyNat).isSome)
+    ++ LSpec.test "getFileEnv still includes imports"
+      ((env.constants.find? `Nat).isSome)
+
+end Tests.Ix.EnvBody

Tests/Main.lean

@@ -27,6 +27,7 @@ import Tests.Keccak
 import Tests.MultiStark
 import Tests.Cli
 import Tests.ShardMap
+import Tests.Ix.EnvBody
 import Ix.Common
 import Ix.Meta
 import Ix.IxVM
@@ -144,6 +145,10 @@ def main (args : List String) : IO UInt32 := do
     let primaryArgs := if runIgnored || includeIgnored then [] else filterArgs
     let primaryResult ← LSpec.lspecIO primarySuites primaryArgs
     if primaryResult != 0 then return primaryResult
+    -- getFileEnv body-inclusion regression guard (IO: loads a fixture file)
+    let envBodySeq ← Tests.Ix.EnvBody.suite
+    let envBodyResult ← LSpec.lspecIO (.ofList [("getfileenv-body", [envBodySeq])]) primaryArgs
+    if envBodyResult != 0 then return envBodyResult
 
   -- Run ignored tests when --ignored or --include-ignored is specified
   if runIgnored || includeIgnored then