From d9ad78043a85e3885ada9593e42e927f23ace8f4 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 20 Dec 2023 23:44:49 -0800 Subject: [PATCH] chore: Minor cleanups and bump Lean version. (#3) --- LibUV/Check.lean | 2 +- LibUV/Idle.lean | 2 +- LibUV/Loop.lean | 2 +- LibUV/Stream.lean | 8 ++------ LibUV/Timer.lean | 3 +-- examples/counter.lean | 28 +++------------------------- examples/phases.lean | 5 ----- examples/timer.lean | 11 +++++++---- lake-manifest.json | 24 +++++++++++++----------- lean-toolchain | 2 +- 10 files changed, 30 insertions(+), 57 deletions(-) diff --git a/LibUV/Check.lean b/LibUV/Check.lean index eaba012..c49101b 100644 --- a/LibUV/Check.lean +++ b/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 } diff --git a/LibUV/Idle.lean b/LibUV/Idle.lean index 42c4d40..ba0ffeb 100644 --- a/LibUV/Idle.lean +++ b/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 } diff --git a/LibUV/Loop.lean b/LibUV/Loop.lean index a04aa9d..8960212 100644 --- a/LibUV/Loop.lean +++ b/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 } diff --git a/LibUV/Stream.lean b/LibUV/Stream.lean index a302865..4c7788b 100644 --- a/LibUV/Stream.lean +++ b/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 } diff --git a/LibUV/Timer.lean b/LibUV/Timer.lean index a293e96..8770e2e 100644 --- a/LibUV/Timer.lean +++ b/LibUV/Timer.lean @@ -6,7 +6,6 @@ alloy c include 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 } diff --git a/examples/counter.lean b/examples/counter.lean index 4c38104..293d514 100644 --- a/examples/counter.lean +++ b/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." diff --git a/examples/phases.lean b/examples/phases.lean index 2fbf699..344331b 100644 --- a/examples/phases.lean +++ b/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 diff --git a/examples/timer.lean b/examples/timer.lean index cf74aa7..da5641f 100644 --- a/examples/timer.lean +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index e0e79e8..ffd755c 100644 --- a/lake-manifest.json +++ b/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"} diff --git a/lean-toolchain b/lean-toolchain index b0a17be..645a4c0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-10-20 +leanprover/lean4:v4.3.0 \ No newline at end of file