Skip to content

Commit

Permalink
change pkg structure for Time
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Feb 29, 2024
1 parent 2f37b63 commit a771d43
Show file tree
Hide file tree
Showing 5 changed files with 15 additions and 35 deletions.
8 changes: 1 addition & 7 deletions lake-manifest.json
Original file line number Diff line number Diff line change
@@ -1,11 +1,5 @@
{"version": 7,
"packagesDir": ".lake/packages",
"packages":
[{"type": "path",
"name": "time",
"manifestFile": "lake-manifest.json",
"inherited": false,
"dir": "./time",
"configFile": "lakefile.lean"}],
"packages": [],
"name": "i18n",
"lakeDir": ".lake"}
15 changes: 14 additions & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ package i18n where
-- add package configuration options here

-- require datetime from git "https://github.com/T-Brick/DateTime.git" @ "main"
require time from "time"

@[default_target]
lean_lib I18n where
Expand All @@ -26,3 +25,17 @@ lean_lib I18n where
-- -- `runFrontend`) at the expense of increased binary size on Linux.
-- -- Remove this line if you do not need such functionality.
-- supportInterpreter := false

lean_lib Time where
-- add library configuration options here

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

extern_lib libLeanTime pkg := do
let name := nameToStaticLib "leanTime"
let timeO ← fetch <| pkg.target ``time.o
buildStaticLib (pkg.nativeLibDir / name) #[timeO]
5 changes: 0 additions & 5 deletions time/lake-manifest.json

This file was deleted.

21 changes: 0 additions & 21 deletions time/lakefile.lean

This file was deleted.

1 change: 0 additions & 1 deletion time/lean-toolchain

This file was deleted.

0 comments on commit a771d43

Please sign in to comment.