Skip to content

Commit

Permalink
add a test
Browse files Browse the repository at this point in the history
  • Loading branch information
TwoFX committed Aug 8, 2024
1 parent adf788f commit 12d8c9d
Show file tree
Hide file tree
Showing 6 changed files with 35 additions and 1 deletion.
6 changes: 6 additions & 0 deletions src/Lean/Runtime.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Empty file added src/include/lean/lean_libuv.h
Empty file.
2 changes: 1 addition & 1 deletion src/runtime/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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})
Expand Down
11 changes: 11 additions & 0 deletions src/runtime/libuv.cpp
Original file line number Diff line number Diff line change
@@ -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());
}
11 changes: 11 additions & 0 deletions src/runtime/libuv.h
Original file line number Diff line number Diff line change
@@ -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);
6 changes: 6 additions & 0 deletions tests/lean/run/libuv.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
import Lean.Runtime

-- 77824 -> 0x013000 -> 0x01.0x30.0x00 -> 1.48.0
/-- info: 77824 -/
#guard_msgs in
#eval Lean.libUvVersion

0 comments on commit 12d8c9d

Please sign in to comment.