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

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