From 9f215527cd99f76b489acaf942a216c7007e7b4a Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joe@lean-fro.org>
Date: Tue, 23 Jan 2024 00:33:33 -0800
Subject: [PATCH] chore: Bump Lean version and add dockerfile for testing

---
 .gitignore             |  4 +---
 LibUV/Stream.lean      |  3 +--
 container/Dockerfile   | 19 +++++++++++++++++++
 include/lean_uv.h      |  1 +
 lean-toolchain         |  2 +-
 scripts/runExamples.sh | 11 +++++++++--
 6 files changed, 32 insertions(+), 8 deletions(-)
 create mode 100644 container/Dockerfile

diff --git a/.gitignore b/.gitignore
index 155f9e5..882b2fe 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,2 @@
-/build
-/lakefile.olean
-/lake-packages/*
+/.lake
 /.vscode
\ No newline at end of file
diff --git a/LibUV/Stream.lean b/LibUV/Stream.lean
index 4c7788b..fb8f193 100644
--- a/LibUV/Stream.lean
+++ b/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
 
 
diff --git a/container/Dockerfile b/container/Dockerfile
new file mode 100644
index 0000000..8cb29c9
--- /dev/null
+++ b/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
diff --git a/include/lean_uv.h b/include/lean_uv.h
index 6741f9b..e7adf43 100644
--- a/include/lean_uv.h
+++ b/include/lean_uv.h
@@ -1,4 +1,5 @@
 #include <lean/lean.h>
+#include <stdarg.h>
 #include <stdlib.h>
 #include <uv.h>
 
diff --git a/lean-toolchain b/lean-toolchain
index 645a4c0..0927c52 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0
\ No newline at end of file
+leanprover/lean4:v4.5.0-rc1
\ No newline at end of file
diff --git a/scripts/runExamples.sh b/scripts/runExamples.sh
index 6349a52..9dedf1b 100755
--- a/scripts/runExamples.sh
+++ b/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