disable FFI use

lakefile.lean

@@ -27,13 +27,17 @@ lean_lib Time where
   srcDir := "." / "time"
   precompileModules := true
 
-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 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]
+/-
+TODO: If the user does not have `c++` available this makes the package
+and all dependencies unusable. Reactivate if there is a better solution
+-/
+-- 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 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]

test/Test.lean

@@ -0,0 +1,13 @@
+import I18n
+
+-- set_language de
+
+def hello := t!"hello world"
+
+def hello2 := t!"Test \n"
+
+#eval hello
+#eval hello2
+
+
+#export_i18n

time/Time/Basic.lean

@@ -2,7 +2,12 @@ import Lean
 
 namespace Time
 
-/-- Returns the local date/time as a string. -/
-@[extern "formatLocalTime"]
-opaque getLocalTime : IO String
+/-
+TODO: see comment in lakefile about `c++`.
+-/
+-- /-- Returns the local date/time as a string. -/
+-- @[extern "formatLocalTime"]
+-- opaque getLocalTime : IO String
 
+/-- Dummy implementation because FFI does not work for everybody. TODO: fix me. -/
+def getLocalTime : IO String := do return ""