diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean
index 5db5b9d6d159..650ae2207062 100644
--- a/src/lake/Lake/DSL/Targets.lean
+++ b/src/lake/Lake/DSL/Targets.lean
@@ -12,6 +12,7 @@ Macros for declaring Lake targets and facets.
 
 namespace Lake.DSL
 open Lean Parser Command
+open System (FilePath)
 
 syntax buildDeclSig :=
   identOrStr (ppSpace simpleBinder)? Term.typeSpec declValSimple
diff --git a/src/lake/examples/targets/lakefile.lean b/src/lake/examples/targets/lakefile.lean
index 432e9aa36c91..0333524f63d9 100644
--- a/src/lake/examples/targets/lakefile.lean
+++ b/src/lake/examples/targets/lakefile.lean
@@ -40,7 +40,7 @@ package_facet print_name pkg : Unit := Job.async do
   IO.println pkg.name
   return ((), .nil)
 
-module_facet get_src mod : FilePath := do
+module_facet get_src mod : System.FilePath := do
   inputTextFile mod.leanFile
 
 module_facet print_src mod : Unit := do