diff --git a/lakefile.lean b/lakefile.lean index cc7c73c..e4e9edf 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,16 +14,16 @@ def srcNames := #[ def wrapperName := "wrapper" def buildDir := defaultBuildDir -def cmarkOTarget (pkg : Package) (srcName : String) : FetchM (BuildJob FilePath) := do +def cmarkOTarget (pkg : Package) (srcName : String) : FetchM (Job FilePath) := do let oFile := pkg.dir / buildDir / cmarkDir / ⟨ srcName ++ ".o" ⟩ - let srcTarget ← inputFile <| pkg.dir / cmarkDir / ⟨ srcName ++ ".c" ⟩ + let srcTarget ← inputFile (pkg.dir / cmarkDir / ⟨ srcName ++ ".c" ⟩) true buildFileAfterDep oFile srcTarget λ srcFile => do let flags := #["-I", (pkg.dir / cmarkDir).toString, "-fPIC"] compileO oFile srcFile flags -def wrapperOTarget (pkg : Package) : FetchM (BuildJob FilePath) := do +def wrapperOTarget (pkg : Package) : FetchM (Job FilePath) := do let oFile := pkg.dir / buildDir / wrapperDir / ⟨ wrapperName ++ ".o" ⟩ - let srcTarget ← inputFile <| pkg.dir / wrapperDir / ⟨ wrapperName ++ ".c" ⟩ + let srcTarget ← inputFile (pkg.dir / wrapperDir / ⟨ wrapperName ++ ".c" ⟩) true buildFileAfterDep oFile srcTarget λ srcFile => do let flags := #["-I", (← getLeanIncludeDir).toString, "-I", (pkg.dir / cmarkDir).toString, "-fPIC"] compileO oFile srcFile flags diff --git a/lean-toolchain b/lean-toolchain index d8a6d7e..62ccd71 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc1 +leanprover/lean4:v4.16.0-rc1