Merge pull request #3 from usernamenotavailablepleasechooseanother/master

Fix linker error on Windows, improve tests

Author: BRonen

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
 

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,41 +43,57 @@ 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 =>
     let hasRow ← cursor.step
     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),

lakefile.lean

@@ -32,12 +32,13 @@ 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
+  buildType := .debug
   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"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:4.24.0
+leanprover/lean4:v4.24.0

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,15 +162,17 @@ 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));
+  // 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));
 }
 
 lean_obj_res lean_sqlite_cursor_column_double(b_lean_obj_arg cursor_box, uint32_t col) {
   sqlite3_stmt* cursor = unbox_cursor(cursor_box);
 
   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) {