diff --git a/Lake/Build/Actions.lean b/Lake/Build/Actions.lean
index ba857db3a4..e1bc31fdfb 100644
--- a/Lake/Build/Actions.lean
+++ b/Lake/Build/Actions.lean
@@ -27,31 +27,20 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
     logError s!"external command {args.cmd} exited with status {out.exitCode}"
     failure
 
-def compileOlean (leanFile oleanFile : FilePath)
+def compileModule (leanFile oleanFile : FilePath) (cFile? : Option FilePath)
 (oleanPath : SearchPath := []) (rootDir : FilePath := ".")
 (leanArgs : Array String := #[]) (lean : FilePath := "lean")
 : BuildM PUnit := do
   createParentDirs oleanFile
+  let ileanFile := oleanFile.withExtension "ilean"
+  let mut args := leanArgs ++ #[
+    "-R", rootDir.toString, "-o", oleanFile.toString, "-i", ileanFile.toString]
+  if let some cFile := cFile? then
+    createParentDirs cFile
+    args := args ++ #["-c", cFile.toString]
   proc {
     cmd := lean.toString
-    args := leanArgs ++ #[
-      "-R", rootDir.toString, "-o", oleanFile.toString, leanFile.toString
-    ]
-    env := #[("LEAN_PATH", oleanPath.toString)]
-  }
-
-def compileOleanAndC (leanFile oleanFile cFile : FilePath)
-(oleanPath : SearchPath := []) (rootDir : FilePath := ".")
-(leanArgs : Array String := #[]) (lean : FilePath := "lean")
-: BuildM PUnit := do
-  createParentDirs cFile
-  createParentDirs oleanFile
-  proc {
-    cmd := lean.toString
-    args := leanArgs ++ #[
-      "-R", rootDir.toString, "-o", oleanFile.toString, "-c",
-      cFile.toString, leanFile.toString
-    ]
+    args := args ++ #[leanFile.toString]
     env := #[("LEAN_PATH", oleanPath.toString)]
   }
 
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index 2f011cb74c..9ada02303b 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -136,14 +136,14 @@ def moduleOleanAndCTarget
 (contents : String)  (depTarget : BuildTarget x)
 (rootDir : FilePath := ".") (leanArgs : Array String := #[]) : OleanAndCTarget :=
   moduleTarget (OleanAndC.mk oleanFile cFile) leanFile traceFile contents depTarget do
-    compileOleanAndC leanFile oleanFile cFile (← getOleanPath) rootDir leanArgs (← getLean)
+    compileModule leanFile oleanFile cFile (← getOleanPath) rootDir leanArgs (← getLean)
 
 def moduleOleanTarget
 (leanFile oleanFile traceFile : FilePath)
 (contents : String) (depTarget : BuildTarget x)
 (rootDir : FilePath := ".") (leanArgs : Array String := #[]) : FileTarget :=
   let target := moduleTarget oleanFile leanFile traceFile contents depTarget do
-    compileOlean leanFile oleanFile (← getOleanPath) rootDir leanArgs (← getLean)
+    compileModule leanFile oleanFile none (← getOleanPath) rootDir leanArgs (← getLean)
   target.withTask do target.bindSync fun oleanFile depTrace => do
     return mixTrace (← computeTrace oleanFile) depTrace