chore: bump toolchain to v4.16.0-rc1

acmepjz · Jan 5, 2025 · 26b1d51 · 26b1d51
1 parent f8ed91f
commit 26b1d51
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/lakefile.lean b/lakefile.lean
@@ -10,7 +10,7 @@ def srcNames := #["entity", "md4c", "md4c-html"]
 def wrapperName := "wrapper"
 def buildDir := defaultBuildDir
 
-def md4cOTarget (pkg : Package) (srcName : String) : FetchM (BuildJob FilePath) := do
+def md4cOTarget (pkg : Package) (srcName : String) : FetchM (Job FilePath) := do
   let oFile := pkg.dir / buildDir / md4cDir / ⟨ srcName ++ ".o" ⟩
   let srcTarget ← inputTextFile <| pkg.dir / md4cDir / ⟨ srcName ++ ".c" ⟩
   buildFileAfterDep oFile srcTarget fun srcFile => do
@@ -23,7 +23,7 @@ def md4cOTarget (pkg : Package) (srcName : String) : FetchM (BuildJob FilePath)
       let flags := #["-I", (pkg.dir / md4cDir).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 ← inputTextFile <| pkg.dir / wrapperDir / ⟨ wrapperName ++ ".c" ⟩
   buildFileAfterDep oFile srcTarget fun srcFile => do

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.16.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.14.0-rc2
		leanprover/lean4:v4.16.0-rc1