From cf972266825a808ab6eed6e538a2b4a0c892c737 Mon Sep 17 00:00:00 2001 From: Anthony Wang Date: Thu, 23 Oct 2025 14:00:32 -0400 Subject: [PATCH 1/4] Fix linker error on Windows --- lakefile.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 295032a..fa9021e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -32,12 +32,12 @@ extern_lib libsqlite pkg := do lean_exe sqlite where root := `Main moreLinkObjs := #[libsqlite] - moreLinkArgs := #["-Wl,--unresolved-symbols=ignore-all"] -- TODO: Very gross hack + moreLinkArgs := if !Platform.isWindows then #["-Wl,--unresolved-symbols=ignore-all"] else #[] -- TODO: Very gross hack @[test_driver] lean_exe Tests.SQLite where moreLinkObjs := #[libsqlite] - moreLinkArgs := #["-Wl,--unresolved-symbols=ignore-all"] -- Same as above + moreLinkArgs := if !Platform.isWindows then #["-Wl,--unresolved-symbols=ignore-all"] else #[] -- Same as above require LSpec from git "https://github.com/argumentcomputer/lspec/" @ "1fc461a9b83eeb68da34df72cec2ef1994e906cb" From 4bcd10a61b6332b0c6af335e42781dd2e47fe949 Mon Sep 17 00:00:00 2001 From: Anthony Wang Date: Thu, 23 Oct 2025 14:43:57 -0400 Subject: [PATCH 2/4] Fix typo in lean-toolchain --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 077c4ce..c00a535 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.24.0 +leanprover/lean4:v4.24.0 From 471f2dee37c7e6b331aa87ebb47d9895f80b333c Mon Sep 17 00:00:00 2001 From: Anthony Wang Date: Thu, 23 Oct 2025 15:40:00 -0400 Subject: [PATCH 3/4] Correctly implement support for int64 and float and test it --- SQLite/FFI.lean | 8 +++++++ Tests/SQLite.lean | 54 ++++++++++++++++++++++++++++++---------------- lakefile.lean | 1 + native/sqliteffi.c | 7 +++--- 4 files changed, 48 insertions(+), 22 deletions(-) diff --git a/SQLite/FFI.lean b/SQLite/FFI.lean index 448a97d..875e8c6 100644 --- a/SQLite/FFI.lean +++ b/SQLite/FFI.lean @@ -67,10 +67,14 @@ structure Cursor where step : IO Bool bindText : UInt32 → String → IO Unit bindInt : UInt32 → Int32 → IO Unit + bindInt64 : UInt32 → Int64 → IO Unit + bindDouble : UInt32 → Float → IO Unit reset : IO Unit columnsCount : IO UInt32 columnText : UInt32 → IO String columnInt : UInt32 → IO Int32 + columnInt64 : UInt32 → IO Int64 + columnDouble : UInt32 → IO Float cursorExplain : UInt32 → IO Int structure Connection where @@ -144,10 +148,14 @@ private def sqlitePrepareWrap (conn : RawConn) (query : String) : IO (Except Str step := cursorStep c, bindText := cursorBindText c, bindInt := cursorBindInt c, + bindInt64 := cursorBindInt64 c, + bindDouble := cursorBindDouble c, reset := cursorReset c, columnsCount := cursorColumnsCount c, columnText := cursorColumnText c, columnInt := cursorColumnInt c, + columnInt64 := cursorColumnInt64 c, + columnDouble := cursorColumnDouble c, cursorExplain := cursorExplain c, } | Except.error e => Except.error e diff --git a/Tests/SQLite.lean b/Tests/SQLite.lean index aa45dd1..ee7f238 100644 --- a/Tests/SQLite.lean +++ b/Tests/SQLite.lean @@ -17,10 +17,10 @@ structure TestContext where def setup (s : String) : IO TestContext := do let flags := SQLITE_OPEN_READWRITE ||| SQLITE_OPEN_CREATE let conn ← connect s flags - match ← conn.prepare "CREATE TABLE IF NOT EXISTS users (id INTEGER PRIMARY KEY, name TEXT NOT NULL);" with + match ← conn.prepare "CREATE TABLE IF NOT EXISTS users (id INTEGER PRIMARY KEY, name TEXT, height REAL) STRICT;" with | Except.ok cursor => cursor.step | Except.error _ => pure false - match ← conn.prepare "INSERT INTO users (id, name) VALUES (1, 'John Doe');" with + match ← conn.prepare "INSERT INTO users (id, name, height) VALUES (1, 'John Doe', 2.3);" with | Except.ok cursor => cursor.step | Except.error _ => pure false return ⟨conn⟩ @@ -43,15 +43,6 @@ def withTest (test : TestContext → IO Bool) : IO Bool := do cleanup ctx return false -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 - cursor.bindText 2 "Jane Doe" - let _ ← cursor.step -- This always returns false - return true - | Except.error _ => return false - def testSelectData (ctx : TestContext) : IO Bool := do match ← ctx.conn.prepare "SELECT * FROM users WHERE id = 1;" with | Except.ok cursor => @@ -59,25 +50,50 @@ def testSelectData (ctx : TestContext) : IO Bool := do if hasRow then let id ← cursor.columnInt 0 let name ← cursor.columnText 1 - return (id = 1 && name == "John Doe") + let height ← cursor.columnDouble 2 + return id == 1 && name == "John Doe" && height == 2.3 + else + return false + | Except.error err => throw <| .userError err + +def testInsertData (ctx : TestContext) : IO Bool := do + let id := -2 ^ 63 |>.toInt64 + let name := "Jane Doe" + let height := 20.25 + match ← ctx.conn.prepare "INSERT INTO users (id, name, height) VALUES (?, ?, ?);" with + | Except.ok cursor => + cursor.bindInt64 1 id + cursor.bindText 2 name + cursor.bindDouble 3 height + let _ ← cursor.step -- This always returns false + | Except.error err => throw <| .userError err + match ← ctx.conn.prepare "SELECT * FROM users WHERE id = ?;" with + | Except.ok cursor => + cursor.bindInt64 1 id + let hasRow ← cursor.step + if hasRow then + let id' ← cursor.columnInt64 0 + let name' ← cursor.columnText 1 + let height' ← cursor.columnDouble 2 + return id == id' && name == name' && height == height' else return false - | Except.error _ => return false + | Except.error err => throw <| .userError err def testParameterBinding (ctx : TestContext) : IO Bool := do - match ← ctx.conn.prepare "SELECT * FROM users WHERE id = ? AND name = ?;" with + match ← ctx.conn.prepare "SELECT * FROM users WHERE id > ? AND name = ?;" with | Except.ok cursor => - cursor.bindInt 1 1 + cursor.bindInt 1 0 cursor.bindText 2 "John Doe" return true - | Except.error _ => return false + | Except.error err => throw <| .userError err def testColumnCount (ctx : TestContext) : IO Bool := do match ← ctx.conn.prepare "SELECT * FROM users;" with | Except.ok cursor => let count ← cursor.columnsCount - return count = 2 - | Except.error _ => return false + return count == 3 + | Except.error err => throw <| .userError err def testInvalidSyntax (ctx : TestContext) : IO Bool := return match ← ctx.conn.prepare "INVALID SQL QUERY;" with @@ -91,8 +107,8 @@ def testNonExistentTable (ctx : TestContext) : IO Bool := def main (args : List String) := do lspecIO (.ofList [("test suite", [ - test "can insert data" (← withTest testInsertData), test "can select data" (← withTest testSelectData), + test "can insert data" (← withTest testInsertData), test "can bind parameters" (← withTest testParameterBinding), test "can get column count" (← withTest testColumnCount), test "handles invalid SQL syntax" (← withTest testInvalidSyntax), diff --git a/lakefile.lean b/lakefile.lean index fa9021e..4ba20c1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -36,6 +36,7 @@ lean_exe sqlite where @[test_driver] lean_exe Tests.SQLite where + buildType := .debug moreLinkObjs := #[libsqlite] moreLinkArgs := if !Platform.isWindows then #["-Wl,--unresolved-symbols=ignore-all"] else #[] -- Same as above diff --git a/native/sqliteffi.c b/native/sqliteffi.c index 1214134..244c06d 100644 --- a/native/sqliteffi.c +++ b/native/sqliteffi.c @@ -154,7 +154,6 @@ lean_obj_res lean_sqlite_cursor_column_int(b_lean_obj_arg cursor_box, uint32_t c const int32_t value = sqlite3_column_int(cursor, col); - /* TODO: int32's do not need to be boxe */ return lean_io_result_mk_ok(lean_box(value)); } @@ -163,7 +162,9 @@ lean_obj_res lean_sqlite_cursor_column_int64(b_lean_obj_arg cursor_box, uint32_t const int64_t value = sqlite3_column_int64(cursor, col); - return lean_io_result_mk_ok(lean_box(value)); + // This is a bit sketchy but it seems to work + // There's no lean_box_int64 + return lean_io_result_mk_ok(lean_box_uint64(value)); } lean_obj_res lean_sqlite_cursor_column_double(b_lean_obj_arg cursor_box, uint32_t col) { @@ -171,7 +172,7 @@ lean_obj_res lean_sqlite_cursor_column_double(b_lean_obj_arg cursor_box, uint32_ const double value = sqlite3_column_double(cursor, col); - return lean_io_result_mk_ok(lean_box(value)); + return lean_io_result_mk_ok(lean_box_float(value)); } lean_obj_res lean_sqlite_cursor_step(b_lean_obj_arg cursor_box) { From 4649869b74e82bdf72d9f00b235490f6e51177cf Mon Sep 17 00:00:00 2001 From: Anthony Wang Date: Thu, 23 Oct 2025 16:33:02 -0400 Subject: [PATCH 4/4] Link to signed ints FFI GitHub issue --- native/sqliteffi.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/native/sqliteffi.c b/native/sqliteffi.c index 244c06d..06d2970 100644 --- a/native/sqliteffi.c +++ b/native/sqliteffi.c @@ -162,8 +162,8 @@ lean_obj_res lean_sqlite_cursor_column_int64(b_lean_obj_arg cursor_box, uint32_t const int64_t value = sqlite3_column_int64(cursor, col); - // This is a bit sketchy but it seems to work - // There's no lean_box_int64 + // There's no lean_box_int64 but this seems to work + // https://github.com/leanprover/lean4/issues/10561 return lean_io_result_mk_ok(lean_box_uint64(value)); }