chore: Minor cleanups and bump Lean version. (#3)

LibUV/Check.lean

@@ -24,7 +24,7 @@ static void check_invoke_callback(uv_check_t* check) {  // Get callback and hand
 }
 end
 
-alloy c extern_type Check => lean_uv_check_t := {
+alloy c opaque_extern_type Check => lean_uv_check_t := {
   foreach  := `Check_foreach
   finalize := `Check_finalize
 }

LibUV/Idle.lean

@@ -34,7 +34,7 @@ static void idle_invoke_callback(uv_idle_t* idle) {
 
 end
 
-alloy c extern_type Idle => lean_uv_idle_t := {
+alloy c opaque_extern_type Idle => lean_uv_idle_t := {
   foreach := `Idle_foreach
   finalize := `Idle_finalize
 }

LibUV/Loop.lean

@@ -190,7 +190,7 @@ static void Loop_foreach(void* ptr, b_lean_obj_arg f) {
 
 end
 
-alloy c extern_type Loop => lean_uv_loop_t := {
+alloy c opaque_extern_type Loop => lean_uv_loop_t := {
   foreach := `Loop_foreach
   finalize := `Loop_finalize
 }

LibUV/Stream.lean

@@ -554,27 +554,23 @@ lean_obj_res lean_uv_write(b_lean_obj_arg streamObj, b_lean_obj_arg bufObj,
     return lean_io_result_mk_ok(reqObj);
   }
 }
-
 end
 
-
 section SockAddr
 
 alloy c section
-
 static void SockAddr_finalize(void* ptr) {
   free(ptr);
 }
 
 static void SockAddr_foreach(void* ptr, b_lean_obj_arg f) {
 }
-
 end
 
 /--
 A IPV4 or IPv6 socket address
 -/
-alloy c extern_type SockAddr => struct sockaddr := {
+alloy c opaque_extern_type SockAddr => struct sockaddr := {
   foreach  := `SockAddr_foreach
   finalize := `SockAddr_finalize
 }
@@ -644,7 +640,7 @@ static void TCP_finalize(void* ptr) {
 
 end
 
-alloy c extern_type TCP => uv_tcp_t := {
+alloy c opaque_extern_type TCP => uv_tcp_t := {
   foreach  := `TCP_foreach
   finalize := `TCP_finalize
 }

LibUV/Timer.lean

@@ -6,7 +6,6 @@ alloy c include <lean_uv.h>
 namespace UV
 
 alloy c section
-
 static void Timer_foreach(void* ptr, b_lean_obj_arg f) {
   fatal_st_only("Timer");
 }
@@ -24,7 +23,7 @@ static void timer_callback(uv_timer_t* timer) {
 }
 end
 
-alloy c extern_type Timer => lean_uv_timer_t := {
+alloy c opaque_extern_type Timer => lean_uv_timer_t := {
   foreach  := `Timer_foreach
   finalize := `Timer_finalize
 }

examples/counter.lean

@@ -6,38 +6,16 @@ This is a Lean implementation of `idle-basic/main.c` with a smaller counter in
 -/
 import LibUV
 
-def ex1 : UV.IO Unit := do
-  let l ← UV.mkLoop
-  let counter ← UV.mkRef 0
-  let idle ← l.mkIdle
-  UV.log s!"Active {←(UV.Handle.idle idle).isActive}"
-  let stop := 7
-  idle.start do
-    counter.modify (λc => c + 1)
-    if (←counter.get) ≥ 7 then
-      idle.stop
-  UV.log s!"Active {←(UV.Handle.idle idle).isActive}"
-  UV.log "Idling..."
-  let stillActive ← l.run
-  if stillActive then
-    UV.fatal "Loop stopped while handle still active."
-  if (←counter.get) ≠ stop then
-    UV.fatal s!"Loop stopped early (counter = {←counter.get})"
-  UV.log "Done"
-
-
 def main : IO Unit := UV.IO.run do
   let l ← UV.mkLoop
   let counter ← IO.mkRef 0
   let idle ← l.mkIdle
-  UV.log s!"Active {←(UV.Handle.idle idle).isActive}"
   let stop := 7
   idle.start do
-    counter.modify (λc => c + 1)
-    if (←counter.get) ≥ 7 then
+    counter.modify (·+1)
+    UV.log s!"Step {←counter.get}"
+    if (←counter.get) ≥ stop then
       idle.stop
-  UV.log s!"Active {←(UV.Handle.idle idle).isActive}"
-  UV.log "Idling..."
   let stillActive ← l.run
   if stillActive then
     UV.fatal "Loop stopped while handle still active."

examples/phases.lean

@@ -6,11 +6,6 @@ This is a Lean implementation of `idle-basic/main.c` with a smaller counter in
 -/
 import LibUV
 
-def fatalError (msg:String) : IO Unit := do
-  IO.eprintln msg
-  (← IO.getStderr).flush
-  IO.Process.exit 1
-
 def main : IO Unit := UV.IO.run do
   let l ← UV.mkLoop
   let check ← l.mkCheck

examples/timer.lean

@@ -4,15 +4,18 @@ def main : IO Unit := UV.IO.run do
   let l ← UV.mkLoop
   let t ← l.mkTimer
   let start ← l.now
+  let inc := 10
+  let maxInc := 15
+  let dur := 100
   let e := start + 100
   let last ← IO.mkRef start
-  UV.log s!"Timer started"
-  t.start 10 10 do
+  UV.log s!"Timer will step every {inc}ms and stop after {dur}ms."
+  t.start inc inc do
     let now ← l.now
     let dur := now - (←last.get)
     last.set now
-    UV.log s!"Elapsed {dur}"
-    if dur < 10 || dur > 15 then
+    UV.log s!"Elapsed {now - start}ms"
+    if dur < inc || dur > maxInc then
       UV.fatal s!"Unexpected duration {dur}."
     if now ≥ e then
       t.stop

lake-manifest.json

@@ -1,12 +1,14 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/tydeu/lean4-alloy.git",
-    "subDir?": null,
-    "rev": "3dfe3ef408faa860e4c75504fe51503b56e9adc4",
-    "opts": {},
-    "name": "alloy",
-    "inputRev?": null,
-    "inherited": false}}],
- "name": "LibUV"}
+ [{"url": "https://github.com/tydeu/lean4-alloy.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "98a8cbdd77d0080dc65ea01c50708f616e0717a8",
+   "name": "alloy",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "LibUV",
+ "lakeDir": ".lake"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-10-20
+leanprover/lean4:v4.3.0