You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
1. First, you are going to want to set the enviromental variable CC in order to build this library.
5
+
- Due to a [limitation with leanc](https://github.com/leanprover/lean4/issues/10831), we cannot use the bundled-in version of clang that comes with Lean in order to build this library.
6
+
- Instead we will have to use a separate C compiler to build SQLite and then we can use Lean's bundled lld linker to link it with our Lean code.
7
+
- On Windows you can use [w64devkit](https://github.com/skeeto/w64devkit), and then set CC like so
Or wherever the version of gcc that comes with w64devkit is located
12
+
- You can later remove this enviromental variable if you don't want to clutter your terminal like so
13
+
```
14
+
Remove-Item Env:CC
15
+
```
16
+
2. Then, you should be able to do ``lake test`` to see the library build properly
17
+
3. If you want to use this library with your own code, make sure you are passing the exact same ``moreLinkArgs`` that this library has
18
+
- ``moreLinkArgs`` are not inherited by child projects
19
+
- Currently, that looks something like this
20
+
```lean
21
+
moreLinkArgs := if !Platform.isWindows then #["-Wl,--unresolved-symbols=ignore-all"] else #[] -- TODO: Very gross hack
22
+
```
23
+
24
+
## Notes
25
+
3
26
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.
0 commit comments