Merge pull request BRonen#2 from usernamenotavailablepleasechooseanother/master

Fix failing test

Author: ValorZard

README.md

@@ -1,3 +1,3 @@
-# Sqlite Lean4
+# SQLite Lean
 
-Uses the (amalgamation)[https://sqlite.org/amalgamation.html] of (SQLite)[https://sqlite.org/download.html], which bundles all of SQLite into one .c file for easy compilation.
+Uses the [amalgamation](https://sqlite.org/amalgamation.html) of [SQLite](https://sqlite.org/), which bundles all of SQLite into one .c file for easy compilation.

Tests/Sqlite.lean

@@ -46,9 +46,9 @@ def withTest (test : TestContext → IO Bool) : IO Bool := do
 def testInsertData (ctx : TestContext) : IO Bool := do
   match ← ctx.conn.prepare "INSERT INTO users (id, name) VALUES (?, ?);" with
   | Except.ok cursor =>
-    cursor.bindInt 1 2 -- TODO: This test fails when set to 2 or 3, but other numbers work???
+    cursor.bindInt 1 2
     cursor.bindText 2 "Jane Doe"
-    let _ ← cursor.step
+    let _ ← cursor.step -- This always returns false
     return true
   | Except.error _ => return false
 

lakefile.lean

@@ -13,15 +13,13 @@ target sqlite.o pkg : FilePath := do
   let sqliteHeaders := pkg.dir / "native"
   -- Ensure that both sqlite3.h and sqlite3ext.h are available during compilation
   let weakArgs := #["-I", sqliteHeaders.toString]
-  -- Use configured compiler variable to allow Windows toolchains to choose the proper C compiler
   buildO oFile srcJob weakArgs #["-fPIC"] compiler getLeanTrace
 
 target sqliteffi.o pkg : FilePath := do
   let oFile := pkg.dir / "native" / "sqliteffi.o"
   let srcJob ← inputTextFile <| pkg.dir / "native" / "sqliteffi.c"
   let sqliteHeaders := pkg.dir / "native"
   let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-I", sqliteHeaders.toString]
-  -- Use configured compiler variable to allow Windows toolchains to choose the proper C compiler
   buildO oFile srcJob weakArgs #["-fPIC"] compiler getLeanTrace
 
 extern_lib libsqlite pkg := do

native/sqliteffi.c

@@ -101,9 +101,8 @@ lean_obj_res lean_sqlite_cursor_bind_text(b_lean_obj_arg cursor_box, uint32_t co
   return lean_io_result_mk_ok(lean_box(0));
 }
 
-lean_obj_res lean_sqlite_cursor_bind_int(b_lean_obj_arg cursor_box, uint32_t col, b_lean_obj_arg value_box) {
+lean_obj_res lean_sqlite_cursor_bind_int(b_lean_obj_arg cursor_box, uint32_t col, int32_t value) {
   sqlite3_stmt* cursor = unbox_cursor(cursor_box);
-  int32_t value = (int32_t) lean_unbox(value_box);
 
   const int32_t c = sqlite3_bind_int(cursor, col, value);