Something went wrong. Try again.
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940import Lakeopen Lake DSL
package «mlang» where version := v!"0.1.0"
extern_lib mlang_http_ffi pkg := do let srcJob ← inputTextFile (pkg.dir / "native" / "mlang_http_ffi.c") let oJob ← buildLeanO (pkg.buildDir / "mlang_http_ffi.o") srcJob buildStaticLib (pkg.staticLibDir / "libmlang_http_ffi.a") #[oJob]
extern_lib mlang_http pkg := do let nativeDir := pkg.dir / "native" / "mlang_http" let srcJob ← inputDir nativeDir true (fun path => path.extension == some "rs" || path.fileName == "Cargo.toml") let outFile := pkg.staticLibDir / "libmlang_http.a" buildFileAfterDep outFile srcJob fun _ => do let cargoToml := nativeDir / "Cargo.toml" let targetDir := nativeDir / "target" proc { cmd := "cargo" args := #[ "build", "--release", "--manifest-path", cargoToml.toString, "--target-dir", targetDir.toString ] } IO.FS.createDirAll pkg.staticLibDir let bytes ← IO.FS.readBinFile (targetDir / "release" / "libmlang_http.a") IO.FS.writeBinFile outFile bytes
lean_lib «Mlang» where
@[default_target]lean_exe «mlang» where root := `Main