merge master

src/Lean/ToExpr.lean

@@ -106,6 +106,10 @@ instance : ToExpr Unit where
   toExpr     := fun _ => mkConst `Unit.unit
   toTypeExpr := mkConst ``Unit
 
+instance : ToExpr System.FilePath where
+  toExpr p := mkApp (mkConst ``System.FilePath.mk) (toExpr p.toString)
+  toTypeExpr := mkConst ``System.FilePath
+
 private def Name.toExprAux (n : Name) : Expr :=
   if isSimple n 0 then
     mkStr n 0 #[]

src/Lean/Util.lean

@@ -29,4 +29,5 @@ import Lean.Util.OccursCheck
 import Lean.Util.HasConstCache
 import Lean.Util.FileSetupInfo
 import Lean.Util.Heartbeats
+import Lean.Util.SearchPath
 import Lean.Util.SafeExponentiation

src/Lean/Util/SearchPath.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.ToExpr
+import Lean.Util.Path
+import Lean.Elab.Term
+
+open Lean
+
+/--
+Term elaborator that retrieves the current `SearchPath`.
+
+Typical usage is `searchPathRef.set compile_time_search_path%`.
+
+This must not be used in files that are potentially compiled on another machine and then imported.
+(That is, if used in an imported file it will embed the search path from whichever machine
+compiled the `.olean`.)
+-/
+elab "compile_time_search_path%" : term =>
+  return toExpr (← searchPathRef.get)

src/lake/Lake/Util/FilePath.lean

@@ -22,7 +22,3 @@ def mkRelPathString (path : FilePath) : String :=
 
 scoped instance : ToJson FilePath where
   toJson path := toJson <| mkRelPathString path
-
-scoped instance : ToExpr FilePath where
-  toExpr p := mkApp (mkConst ``System.FilePath.mk) (toExpr p.toString)
-  toTypeExpr := mkConst ``System.FilePath