chore: Bump Lean version and add dockerfile for testing

.gitignore

@@ -1,4 +1,2 @@
-/build
-/lakefile.olean
-/lake-packages/*
+/.lake
 /.vscode

LibUV/Stream.lean

@@ -1,8 +1,7 @@
 import LibUV.Loop
 
 open scoped Alloy.C
-alloy c include <stdlib.h> <lean_uv.h>
-
+alloy c include <stdlib.h> <string.h> <lean_uv.h>
 section NonemptyProp
 
 

container/Dockerfile

@@ -0,0 +1,19 @@
+# This is a fairly minimal Ubuntu container that can build
+# lean-libuv for testing purposes.
+FROM ubuntu:jammy
+
+USER root
+
+RUN apt-get update && \
+    DEBIAN_FRONTEND=noninteractive apt-get install -y --no-install-recommends \
+      curl ca-certificates clang-14 expect git libuv1-dev pkg-config && \
+    apt-get clean
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | \
+    sh -s -- -y --default-toolchain none
+
+RUN update-alternatives --install /usr/bin/cc cc /usr/bin/clang-14 100
+
+ENV PATH="/root/.elan/bin:${PATH}"
+
+WORKDIR /libuv

include/lean_uv.h

@@ -1,4 +1,5 @@
 #include <lean/lean.h>
+#include <stdarg.h>
 #include <stdlib.h>
 #include <uv.h>
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.5.0-rc1

scripts/runExamples.sh

@@ -2,8 +2,15 @@
 lake build
 
 search_dir=/the/path/to/base/dir
-dylibs=""
-for entry in "build/lib"/*.dylib;
+if [[ "$OSTYPE" == "darwin"* ]]; then
+  dsoext=.dylib
+else
+  dsoext=.so
+fi
+
+
+dynlibs=""
+for entry in ".lake/build/lib"/*$dsoext
 do
   dylibs+=" --load-dynlib=$entry"
 done