fix: remove empty .out.expected (lint.py flags empty files)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Lean/Elab/BuiltinTerm.lean

@@ -387,7 +387,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   | _ => throwUnsupportedSyntax
 
 private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath :=
-  evalTerm System.FilePath (Lean.mkConst ``System.FilePath) stx
+  evalTerm System.FilePath (Lean.mkConst ``System.FilePath) stx (checkMeta := false)
 
 @[implemented_by evalFilePathUnsafe]
 private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath

src/Lean/Elab/Eval.lean

@@ -14,11 +14,12 @@ public section
 namespace Lean.Elab.Term
 open Meta
 
-unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α := withoutModifyingEnv do
+unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe)
+    (checkMeta : Bool := true) : TermElabM α := withoutModifyingEnv do
   let v ← elabTermEnsuringType value type
   synthesizeSyntheticMVarsNoPostponing
   let v ← instantiateMVars v
   if (← logUnassignedUsingErrorInfos (← getMVars v)) then throwAbortTerm
-  evalExpr α type v safety
+  evalExpr α type v safety (checkMeta := checkMeta)
 
 end Lean.Elab.Term

src/Lean/Meta/Eval.lean

@@ -36,14 +36,16 @@ unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit)
        value, hints := ReducibilityHints.opaque,
        safety
     }
-    modifyEnv (markMeta · name)
+    if checkMeta then
+      modifyEnv (markMeta · name)
     -- compilation will invariably wait on `checked`
     let _ ← traceBlock "compiler env" (← getEnv).checked
     -- now that we've already waited, async would just introduce (minor) overhead and trigger
     -- `Task.get` blocking debug code
     withOptions (Elab.async.set · false) do
     withOptions (Compiler.compiler.postponeCompile.set · false) do
-    withOptions (Compiler.compiler.relaxedMetaCheck.set · true) do
+    withOptions (fun opts => if checkMeta then Compiler.compiler.relaxedMetaCheck.set opts true
+                             else Compiler.compiler.checkMeta.set opts false) do
       addAndCompile decl
       evalConst (checkMeta := checkMeta) α name
 

tests/elab/13310.lean

@@ -0,0 +1,16 @@
+-- Regression test for https://github.com/leanprover/lean4/issues/13310
+-- `include_str` should not require `public meta import Init.System.FilePath`
+
+module
+
+-- Before the fix, this would produce:
+--   Invalid `meta` definition `_tmp✝`, `System.FilePath.mk` is not accessible here;
+--   consider adding `public meta import Init.System.FilePath`
+-- After the fix, `include_str` evaluates the file path without meta checks, so the
+-- only error is about computing the parent directory (expected in the elab test runner
+-- which passes a bare filename without a directory prefix).
+/--
+error: cannot compute parent directory of `13310.lean`
+-/
+#guard_msgs in
+def hello := include_str "13310.txt"