Skip to content

Commit 5a9c998

Browse files
BRonenBRonen
authored
Merge pull request #1 from ValorZard/master
Vendor SQLite so no longer need nix or package manager to install SQLite
2 parents 75d0dab + 701cbfe commit 5a9c998

File tree

16 files changed

+277554
-99
lines changed

16 files changed

+277554
-99
lines changed

‎.clangd‎

Lines changed: 0 additions & 6 deletions
This file was deleted.

‎.gitignore‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
/ffi/.lake
21
/.lake
32
/.direnv
43
test.sqlite3

‎Main.lean‎

Lines changed: 16 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,41 +1,40 @@
1-
import Sqlite
1+
import SQLite
22

33
open IO
44

55
def double (f : Nat -> Nat) n := f (f n)
66
def inc := fun n => n + 1
77

8-
def cursorExplain (c : Sqlite.FFI.Connection) (emode : UInt32) : IO Unit := do
8+
def cursorExplain (c : SQLite.FFI.Connection) (emode : UInt32) : IO Unit := do
99
match ← c.prepare "select * from users limit 50;" with
1010
| Except.error e => println s!"error {e}"
11-
| Except.ok q => do
11+
| Except.ok q =>
1212
let _ ← q.cursorExplain emode
1313
let c ← q.columnsCount
1414
println s!"columnsCount: {c}"
1515
for i in [0:100] do
1616
match ← q.step with
17-
| false => pure ()
18-
| true => do
17+
| false => return ()
18+
| true =>
1919
println s!"{i} explain: {← q.columnInt 0} {← q.columnText 1}"
2020

21-
22-
def printUser (fuel : Nat) (cursor : Sqlite.FFI.Cursor) : IO Unit := do
21+
def printUser (fuel : Nat) (cursor : SQLite.FFI.Cursor) : IO Unit := do
2322
if fuel = 0 then
24-
pure ()
23+
return ()
2524
else
2625
match ← cursor.step with
27-
| false => pure ()
28-
| true => do
26+
| false => return ()
27+
| true =>
2928
println s!"id: {← cursor.columnInt 0} | name: {← cursor.columnText 1}"
3029
printUser (fuel - 1) cursor
3130

3231
def main : IO Unit := do
33-
println $ ← Sqlite.FFI.sqliteThreadsafe
34-
println Sqlite.FFI.Constants.SQLITE_CONFIG_SINGLETHREAD
35-
println Sqlite.FFI.Constants.SQLITE_CONFIG_MULTITHREAD
36-
println $ ← Sqlite.FFI.sqliteConfig Sqlite.FFI.Constants.SQLITE_CONFIG_MULTITHREAD
37-
let flags := Sqlite.FFI.Constants.SQLITE_OPEN_READWRITE ||| Sqlite.FFI.Constants.SQLITE_OPEN_CREATE
38-
let conn ← Sqlite.FFI.connect "test.sqlite3" flags
32+
println <| ← SQLite.FFI.sqliteThreadsafe
33+
println SQLite.FFI.Constants.SQLITE_CONFIG_SINGLETHREAD
34+
println SQLite.FFI.Constants.SQLITE_CONFIG_MULTITHREAD
35+
println <| ← SQLite.FFI.sqliteConfig SQLite.FFI.Constants.SQLITE_CONFIG_MULTITHREAD
36+
let flags := SQLite.FFI.Constants.SQLITE_OPEN_READWRITE ||| SQLite.FFI.Constants.SQLITE_OPEN_CREATE
37+
let conn ← SQLite.FFI.connect "test.sqlite3" flags
3938
cursorExplain conn 1
4039
match ← conn.prepare "delete from users where id = 154;" with
4140
| Except.ok c => c.step
@@ -58,6 +57,6 @@ def main : IO Unit := do
5857
match ← conn.prepare "select * from users;" with
5958
| Except.error e => println e
6059
| Except.ok c =>
61-
printUser count.toNat c
60+
printUser count.toNatClampNeg c
6261
| Except.error e => println s!"error: {e}"
6362
println s!"Hello, {conn}"

‎README.md‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,3 @@
1-
# Sqlite Lean4
1+
# SQLite Lean
22

3+
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.

‎SQLite.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import SQLite.FFI

Sqlite/FFI.lean renamed to SQLite/FFI.lean

Lines changed: 22 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
namespace Sqlite.FFI
1+
namespace SQLite.FFI
22
namespace Constants
33

44
def SQLITE_CONFIG_SINGLETHREAD : UInt32 := 1
@@ -66,11 +66,11 @@ structure Cursor where
6666
cursor : RawCursor
6767
step : IO Bool
6868
bindText : UInt32 → String → IO Unit
69-
bindInt : UInt32 → Int → IO Unit
69+
bindInt : UInt32 → Int32 → IO Unit
7070
reset : IO Unit
7171
columnsCount : IO UInt32
7272
columnText : UInt32 → IO String
73-
columnInt : UInt32 → IO Int
73+
columnInt : UInt32 → IO Int32
7474
cursorExplain : UInt32 → IO Int
7575

7676
structure Connection where
@@ -97,6 +97,14 @@ private opaque cursorBindText : @&RawCursor → UInt32 → String → IO Unit
9797
@[extern "lean_sqlite_cursor_bind_int"]
9898
private opaque cursorBindInt : @&RawCursor → UInt32 → Int32 → IO Unit
9999

100+
@[extern "lean_sqlite_cursor_bind_int64"]
101+
private opaque cursorBindInt64 : @&RawCursor → UInt32 → Int64 → IO Unit
102+
103+
@[extern "lean_sqlite_cursor_bind_double"]
104+
private opaque cursorBindDouble : @&RawCursor → UInt32 → Float → IO Unit
105+
106+
-- TODO: Support binding ByteArrays
107+
100108
@[extern "lean_sqlite_cursor_bind_parameter_name"]
101109
private opaque cursorBindParameterName : @&RawCursor → Int32 → String → IO Unit
102110

@@ -115,6 +123,12 @@ private opaque cursorColumnText : @&RawCursor → UInt32 → IO String
115123
@[extern "lean_sqlite_cursor_column_int"]
116124
private opaque cursorColumnInt : @&RawCursor → UInt32 → IO Int32
117125

126+
@[extern "lean_sqlite_cursor_column_int64"]
127+
private opaque cursorColumnInt64 : @&RawCursor → UInt32 → IO Int64
128+
129+
@[extern "lean_sqlite_cursor_column_double"]
130+
private opaque cursorColumnDouble : @&RawCursor → UInt32 → IO Float
131+
118132
@[extern "lean_sqlite_cursor_explain"]
119133
private opaque cursorExplain : @&RawCursor → UInt32 → IO Int
120134

@@ -125,7 +139,7 @@ opaque sqliteThreadsafe : IO Int
125139
opaque sqliteConfig : UInt32 → IO Unit
126140

127141
private def sqlitePrepareWrap (conn : RawConn) (query : String) : IO (Except String Cursor) := do
128-
pure $ match ← sqlitePrepare conn query with
142+
return match ← sqlitePrepare conn query with
129143
| Except.ok c => pure { cursor := c,
130144
step := cursorStep c,
131145
bindText := cursorBindText c,
@@ -139,8 +153,8 @@ private def sqlitePrepareWrap (conn : RawConn) (query : String) : IO (Except Str
139153

140154
def connect (s : String) (flags : UInt32) : IO Connection := do
141155
let rawconn ← sqliteOpen s flags
142-
pure { path := s,
143-
conn := rawconn,
144-
prepare := (sqlitePrepareWrap rawconn ·) }
156+
return { path := s,
157+
conn := rawconn,
158+
prepare := (sqlitePrepareWrap rawconn ·) }
145159

146-
end Sqlite.FFI
160+
end SQLite.FFI

‎Sqlite.lean‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

Tests/Sqlite.lean renamed to Tests/SQLite.lean

Lines changed: 37 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
import Sqlite
21
import LSpec
2+
import SQLite
33

44
open LSpec
5-
open Sqlite.FFI
6-
open Sqlite.FFI.Constants
5+
open SQLite.FFI
6+
open SQLite.FFI.Constants
77

88
instance (b : Bool) : Testable b :=
99
if h : b = true then
@@ -17,43 +17,40 @@ structure TestContext where
1717
def setup (s : String) : IO TestContext := do
1818
let flags := SQLITE_OPEN_READWRITE ||| SQLITE_OPEN_CREATE
1919
let conn ← connect s flags
20-
2120
match ← conn.prepare "CREATE TABLE IF NOT EXISTS users (id INTEGER PRIMARY KEY, name TEXT NOT NULL);" with
2221
| Except.ok cursor => cursor.step
2322
| Except.error _ => pure false
24-
2523
match ← conn.prepare "INSERT INTO users (id, name) VALUES (1, 'John Doe');" with
2624
| Except.ok cursor => cursor.step
2725
| Except.error _ => pure false
28-
29-
pure ⟨conn⟩
26+
return ⟨conn⟩
3027

3128
def cleanup (ctx : TestContext) : IO Unit := do
3229
match ← ctx.conn.prepare "DROP TABLE IF EXISTS users;" with
3330
| Except.ok cursor => do
3431
let _ ← cursor.step
35-
pure ()
36-
| Except.error _ => pure ()
32+
return ()
33+
| Except.error _ => return ()
3734

3835
def withTest (test : TestContext → IO Bool) : IO Bool := do
3936
let ctx ← setup "test.sqlite3"
4037
try
4138
let result ← test ctx
4239
cleanup ctx
43-
pure result
40+
return result
4441
catch e =>
4542
IO.println s!"Error: {e}"
4643
cleanup ctx
47-
pure false
44+
return false
4845

4946
def testInsertData (ctx : TestContext) : IO Bool := do
5047
match ← ctx.conn.prepare "INSERT INTO users (id, name) VALUES (?, ?);" with
5148
| Except.ok cursor =>
5249
cursor.bindInt 1 2
5350
cursor.bindText 2 "Jane Doe"
54-
let _ ← cursor.step
55-
pure true
56-
| Except.error _ => pure false
51+
let _ ← cursor.step -- This always returns false
52+
return true
53+
| Except.error _ => return false
5754

5855
def testSelectData (ctx : TestContext) : IO Bool := do
5956
match ← ctx.conn.prepare "SELECT * FROM users WHERE id = 1;" with
@@ -62,41 +59,42 @@ def testSelectData (ctx : TestContext) : IO Bool := do
6259
if hasRow then
6360
let id ← cursor.columnInt 0
6461
let name ← cursor.columnText 1
65-
pure (id = 1 && name == "John Doe")
62+
return (id = 1 && name == "John Doe")
6663
else
67-
pure false
68-
| Except.error _ => pure false
64+
return false
65+
| Except.error _ => return false
6966

7067
def testParameterBinding (ctx : TestContext) : IO Bool := do
7168
match ← ctx.conn.prepare "SELECT * FROM users WHERE id = ? AND name = ?;" with
7269
| Except.ok cursor =>
7370
cursor.bindInt 1 1
7471
cursor.bindText 2 "John Doe"
75-
pure true
76-
| Except.error _ => pure false
72+
return true
73+
| Except.error _ => return false
7774

7875
def testColumnCount (ctx : TestContext) : IO Bool := do
7976
match ← ctx.conn.prepare "SELECT * FROM users;" with
8077
| Except.ok cursor =>
8178
let count ← cursor.columnsCount
82-
pure (count = 2)
83-
| Except.error _ => pure false
84-
85-
def testInvalidSyntax (ctx : TestContext) : IO Bool := do
86-
match ← ctx.conn.prepare "INVALID SQL QUERY;" with
87-
| Except.error _ => pure true
88-
| Except.ok _ => pure false
89-
90-
def testNonExistentTable (ctx : TestContext) : IO Bool := do
91-
match ← ctx.conn.prepare "SELECT * FROM non_existent_table;" with
92-
| Except.error _ => pure true
93-
| Except.ok _ => pure false
94-
95-
def main := do
96-
lspecIO $
97-
test "can insert data" (← withTest testInsertData) $
98-
test "can select data" (← withTest testSelectData) $
99-
test "can bind parameters" (← withTest testParameterBinding) $
100-
test "can get column count" (← withTest testColumnCount) $
101-
test "handles invalid SQL syntax" (← withTest testInvalidSyntax) $
79+
return count = 2
80+
| Except.error _ => return false
81+
82+
def testInvalidSyntax (ctx : TestContext) : IO Bool :=
83+
return match ← ctx.conn.prepare "INVALID SQL QUERY;" with
84+
| Except.error _ => true
85+
| Except.ok _ => false
86+
87+
def testNonExistentTable (ctx : TestContext) : IO Bool :=
88+
return match ← ctx.conn.prepare "SELECT * FROM non_existent_table;" with
89+
| Except.error _ => true
90+
| Except.ok _ => false
91+
92+
def main (args : List String) := do
93+
lspecIO (.ofList [("test suite", [
94+
test "can insert data" (← withTest testInsertData),
95+
test "can select data" (← withTest testSelectData),
96+
test "can bind parameters" (← withTest testParameterBinding),
97+
test "can get column count" (← withTest testColumnCount),
98+
test "handles invalid SQL syntax" (← withTest testInvalidSyntax),
10299
test "handles non-existent table" (← withTest testNonExistentTable)
100+
])]) args

‎lake-manifest.json‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,11 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "8a51034d049c6a229d88dd62f490778a377eec06",
8+
"rev": "1fc461a9b83eeb68da34df72cec2ef1994e906cb",
99
"name": "LSpec",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "8a51034d049c6a229d88dd62f490778a377eec06",
11+
"inputRev": "1fc461a9b83eeb68da34df72cec2ef1994e906cb",
1212
"inherited": false,
13-
"configFile": "lakefile.lean"}],
13+
"configFile": "lakefile.toml"}],
1414
"name": "sqlite",
1515
"lakeDir": ".lake"}

‎lakefile.lean‎

Lines changed: 29 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -3,26 +3,41 @@ open System Lake DSL
33

44
package sqlite
55

6-
lean_lib Sqlite
6+
lean_lib SQLite
77

8-
@[default_target]
9-
lean_exe sqlite where
10-
root := `Main
11-
moreLinkArgs := #["-lsqlite3"]
8+
def compiler := (·.getD "cc") <$> IO.getEnv "CC"
129

13-
lean_exe Tests.Sqlite where
14-
moreLinkArgs := #["-lsqlite3"]
10+
target sqlite.o pkg : FilePath := do
11+
let oFile := pkg.buildDir / "sqlite3.o"
12+
let srcJob ← inputTextFile <| pkg.dir / "native" / "sqlite3.c"
13+
let sqliteHeaders := pkg.dir / "native"
14+
-- Ensure that both sqlite3.h and sqlite3ext.h are available during compilation
15+
let weakArgs := #["-I", sqliteHeaders.toString]
16+
buildO oFile srcJob weakArgs #["-fPIC"] (← compiler) getLeanTrace
1517

1618
target sqliteffi.o pkg : FilePath := do
17-
let oFile := pkg.buildDir / "native" / "sqliteffi.o"
18-
let srcJob ← inputTextFile <| pkg.dir / "native" / "ffi.c"
19-
let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-I/nix/store/8r55amvr43sm771rgm0sszd05rm8j1cr-sqlite-3.46.0-dev/include/"]
20-
buildO oFile srcJob weakArgs #["-fPIC"] "clang" getLeanTrace
19+
let oFile := pkg.buildDir / "sqliteffi.o"
20+
let srcJob ← inputTextFile <| pkg.dir / "native" / "sqliteffi.c"
21+
let sqliteHeaders := pkg.dir / "native"
22+
let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-I", sqliteHeaders.toString]
23+
buildO oFile srcJob weakArgs #["-fPIC"] (← compiler) getLeanTrace
2124

22-
extern_lib libsqliteffi pkg := do
25+
extern_lib libsqlite pkg := do
26+
let sqliteO ← sqlite.o.fetch
2327
let ffiO ← sqliteffi.o.fetch
2428
let name := nameToStaticLib "sqliteffi"
25-
buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
29+
buildStaticLib (pkg.staticLibDir / name) #[sqliteO, ffiO]
30+
31+
@[default_target]
32+
lean_exe sqlite where
33+
root := `Main
34+
moreLinkObjs := #[libsqlite]
35+
moreLinkArgs := #["-Wl,--unresolved-symbols=ignore-all"] -- TODO: Very gross hack
36+
37+
@[test_driver]
38+
lean_exe Tests.SQLite where
39+
moreLinkObjs := #[libsqlite]
40+
moreLinkArgs := #["-Wl,--unresolved-symbols=ignore-all"] -- Same as above
2641

2742
require LSpec from git
28-
"https://github.com/argumentcomputer/lspec/" @ "8a51034d049c6a229d88dd62f490778a377eec06"
43+
"https://github.com/argumentcomputer/lspec/" @ "1fc461a9b83eeb68da34df72cec2ef1994e906cb"

0 commit comments

Comments
 (0)