nandi.uk
This repository has no description
1import Lake
2open Lake DSL
3
4package «mlang» where
5 version := v!"0.1.0"
6
7extern_lib mlang_http_ffi pkg := do
8 let srcJob ← inputTextFile (pkg.dir / "native" / "mlang_http_ffi.c")
9 let oJob ← buildLeanO (pkg.buildDir / "mlang_http_ffi.o") srcJob
10 buildStaticLib (pkg.staticLibDir / "libmlang_http_ffi.a") #[oJob]
11
12extern_lib mlang_http pkg := do
13 let nativeDir := pkg.dir / "native" / "mlang_http"
14 let srcJob ← inputDir nativeDir true (fun path =>
15 path.extension == some "rs" || path.fileName == "Cargo.toml")
16 let outFile := pkg.staticLibDir / "libmlang_http.a"
17 buildFileAfterDep outFile srcJob fun _ => do
18 let cargoToml := nativeDir / "Cargo.toml"
19 let targetDir := nativeDir / "target"
20 proc {
21 cmd := "cargo"
22 args := #[
23 "build",
24 "--release",
25 "--manifest-path",
26 cargoToml.toString,
27 "--target-dir",
28 targetDir.toString
29 ]
30 }
31 IO.FS.createDirAll pkg.staticLibDir
32 let bytes ← IO.FS.readBinFile (targetDir / "release" / "libmlang_http.a")
33 IO.FS.writeBinFile outFile bytes
34
35lean_lib «Mlang» where
36
37@[default_target]
38lean_exe «mlang» where
39 root := `Main