From a761839228816a99e0012c6cd061d3485dd0c637 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Thu, 20 Jun 2024 15:11:46 +0200
Subject: [PATCH] disable FFI use

---
 lakefile.lean        | 24 ++++++++++++++----------
 test/Test.lean       | 13 +++++++++++++
 time/Time/Basic.lean | 11 ++++++++---
 3 files changed, 35 insertions(+), 13 deletions(-)
 create mode 100644 test/Test.lean

diff --git a/lakefile.lean b/lakefile.lean
index 0cbbd9f..4300302 100644
--- a/lakefile.lean
+++ b/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]
diff --git a/test/Test.lean b/test/Test.lean
new file mode 100644
index 0000000..300ad1a
--- /dev/null
+++ b/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
diff --git a/time/Time/Basic.lean b/time/Time/Basic.lean
index 1e74a53..b868fd2 100644
--- a/time/Time/Basic.lean
+++ b/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 ""