Skip to content

Commit

Permalink
renaming + clean-up lakefile
Browse files Browse the repository at this point in the history
  • Loading branch information
T-Brick committed Feb 28, 2024
1 parent e5480c9 commit e681987
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 8 deletions.
File renamed without changes.
16 changes: 8 additions & 8 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,13 @@ lean_exe «datetime» where
root := `Main
supportInterpreter := true

target ffi.o pkg : FilePath := do
let oFile := pkg.buildDir / "DateTime" / "c" / "ffi.o"
let srcJob ← inputFile <| pkg.dir / "DateTime" / "c" / "ffi.cpp"
target datetime.o pkg : FilePath := do
let oFile := pkg.buildDir / "DateTime" / "c" / "datetime.o"
let srcJob ← inputFile <| pkg.dir / "DateTime" / "c" / "datetime.cpp"
let weakArgs := #["-I", (← getLeanIncludeDir).toString]
buildO "ffi.cpp" oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace
buildO "datetime.cpp" oFile srcJob weakArgs #["-fPIC"] "g++" getLeanTrace

extern_lib libleanffi pkg := do
let name := nameToStaticLib "leanffi"
let ffiO ← fetch <| pkg.target ``ffi.o
buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
extern_lib lib_datetime pkg := do
let name := nameToStaticLib "datetime"
let datetimeO ← fetch <| pkg.target ``datetime.o
buildStaticLib (pkg.nativeLibDir / name) #[datetimeO]

0 comments on commit e681987

Please sign in to comment.