From 12d8c9d91c5250c1b8df4f7712f0f81169a4eacb Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 8 Aug 2024 18:32:12 +0200
Subject: [PATCH] add a test

---
 src/Lean/Runtime.lean         |  6 ++++++
 src/include/lean/lean_libuv.h |  0
 src/runtime/CMakeLists.txt    |  2 +-
 src/runtime/libuv.cpp         | 11 +++++++++++
 src/runtime/libuv.h           | 11 +++++++++++
 tests/lean/run/libuv.lean     |  6 ++++++
 6 files changed, 35 insertions(+), 1 deletion(-)
 create mode 100644 src/include/lean/lean_libuv.h
 create mode 100644 src/runtime/libuv.cpp
 create mode 100644 src/runtime/libuv.h
 create mode 100644 tests/lean/run/libuv.lean

diff --git a/src/Lean/Runtime.lean b/src/Lean/Runtime.lean
index 4cac6f13794b..aae7d9ca6af8 100644
--- a/src/Lean/Runtime.lean
+++ b/src/Lean/Runtime.lean
@@ -20,4 +20,10 @@ def closureMaxArgs : Nat :=
 def maxSmallNat : Nat :=
   maxSmallNatFn ()
 
+@[extern "lean_libuv_version"]
+opaque libUvVersionFn : Unit → Nat
+
+def libUvVersion : Nat :=
+  libUvVersionFn ()
+
 end Lean
diff --git a/src/include/lean/lean_libuv.h b/src/include/lean/lean_libuv.h
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt
index f69610853169..367c7c298038 100644
--- a/src/runtime/CMakeLists.txt
+++ b/src/runtime/CMakeLists.txt
@@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
 stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
-process.cpp object_ref.cpp mpn.cpp mutex.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp)
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
 set_target_properties(leanrt_initial-exec PROPERTIES
   ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
diff --git a/src/runtime/libuv.cpp b/src/runtime/libuv.cpp
new file mode 100644
index 000000000000..89b41aa157ed
--- /dev/null
+++ b/src/runtime/libuv.cpp
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Markus Himmel
+*/
+#include "runtime/libuv.h"
+
+extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg o) {
+    return lean_unsigned_to_nat(uv_version());
+}
diff --git a/src/runtime/libuv.h b/src/runtime/libuv.h
new file mode 100644
index 000000000000..3e0eb34fb9e2
--- /dev/null
+++ b/src/runtime/libuv.h
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Markus Himmel
+*/
+#pragma once
+#include <lean/lean.h>
+#include <uv.h>
+
+extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg);
diff --git a/tests/lean/run/libuv.lean b/tests/lean/run/libuv.lean
new file mode 100644
index 000000000000..51681c847e40
--- /dev/null
+++ b/tests/lean/run/libuv.lean
@@ -0,0 +1,6 @@
+import Lean.Runtime
+
+-- 77824 -> 0x013000 -> 0x01.0x30.0x00 -> 1.48.0
+/-- info: 77824 -/
+#guard_msgs in
+#eval Lean.libUvVersion