chore: using flake and upgrade lean4

Author: BRonen

.envrc

@@ -1 +1 @@
-use nix
+use flake

Main.lean

@@ -58,6 +58,6 @@ def main : IO Unit := do
     match ← conn.prepare "select * from users;" with
      | Except.error e => println e
      | Except.ok c =>
-       printUser count.toNat c
+       printUser count.toNatClampNeg c
   | Except.error e => println s!"error: {e}"
   println s!"Hello, {conn}"

Sqlite/FFI.lean

@@ -66,11 +66,11 @@ structure Cursor where
   cursor : RawCursor
   step : IO Bool
   bindText : UInt32 → String → IO Unit
-  bindInt : UInt32 → Int → IO Unit
+  bindInt : UInt32 → Int32 → IO Unit
   reset : IO Unit
   columnsCount : IO UInt32
   columnText : UInt32 → IO String
-  columnInt : UInt32 → IO Int
+  columnInt : UInt32 → IO Int32
   cursorExplain : UInt32 → IO Int
 
 structure Connection where
@@ -83,6 +83,7 @@ instance : ToString Connection where
 
 @[extern "lean_sqlite_initialize"]
 private opaque sqliteInit : IO Unit
+
 builtin_initialize sqliteInit
 
 @[extern "lean_sqlite_open"]

flake.lock

@@ -0,0 +1,16 @@
+{
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.05";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachSystem [ "x86_64-darwin" "x86_64-linux" "i686-linux" ] (system:
+      let pkgs = import nixpkgs { inherit system; };
+      in {
+        defaultPackage = pkgs.mkShell {
+          buildInputs = with pkgs; [ sqlite lean4 ];
+        };
+      }
+    );
+}

flake.nix

@@ -17,12 +17,12 @@ target sqliteffi.o pkg : FilePath := do
   let oFile := pkg.buildDir / "native" / "sqliteffi.o"
   let srcJob ← inputTextFile <| pkg.dir / "native" / "ffi.c"
   let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-I/nix/store/8r55amvr43sm771rgm0sszd05rm8j1cr-sqlite-3.46.0-dev/include/"]
-  buildO oFile srcJob weakArgs #["-fPIC"] "clang" getLeanTrace
+  buildO oFile srcJob weakArgs #["-fPIC"] "gcc" getLeanTrace
 
 extern_lib libsqliteffi pkg := do
   let ffiO ← sqliteffi.o.fetch
   let name := nameToStaticLib "sqliteffi"
-  buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+  buildStaticLib (pkg.staticLibDir / name) #[ffiO]
 
 require LSpec from git
   "https://github.com/argumentcomputer/lspec/" @ "8a51034d049c6a229d88dd62f490778a377eec06"

lakefile.lean

@@ -1 +1 @@
-leanprover/lean4:4.10.0
+leanprover/lean4:4.20.0

lean-toolchain

@@ -26,16 +26,12 @@ sqlite3_stmt* unbox_cursor(lean_object* o) {
 void connection_finalize(void* conn) {
   if (!conn) return;
 
-  printf("connection_finalize: %x\n", conn);
-
   sqlite3_close(conn);
 }
 
 void cursor_finalize(void* cursor) {
   if (!cursor) return;
 
-  printf("cursor_finalize: %x\n", cursor);
-
   sqlite3_finalize(cursor);
 }
 
@@ -49,8 +45,6 @@ lean_obj_res lean_sqlite_open(b_lean_obj_arg path, uint32_t flags) {
   const char* path_str = lean_string_cstr(path);
   sqlite3* conn = malloc(sizeof(sqlite3*));
 
-  printf("initialize_connection: %x\n", conn);
-
   int32_t c = sqlite3_open_v2(path_str, &conn, flags, NULL);
 
   if (c == SQLITE_OK)
@@ -69,8 +63,6 @@ lean_obj_res lean_sqlite_prepare(b_lean_obj_arg conn_box, b_lean_obj_arg query_s
 
   sqlite3_stmt* cursor = malloc(sizeof(sqlite3_stmt*));
 
-  printf("initialize_cursor: %x\n", cursor);
-
   int32_t c = sqlite3_prepare_v2(conn, query, -1, &cursor, NULL);
 
   if (c != SQLITE_OK) {