SQLite bindings for Lean

Stream: general

[Anthony Wang]

This is a new thread for discussion about designing and creating SQLite bindings for Lean, inspired by the ideas in #general > Making SDL3 bindings for Lean 4 @ 💬 and #general > Making SDL3 bindings for Lean 4 @ 💬.

[Eric Taucher]

As noted in the related post

Some of my ideas/needs include

• Proofs with the code.
• Hoare pre/post conditions.
• Use of views instead of free form text for queries.
• Having more than one SQLite module that would require proofs versus a binding that does not require proofs.

[Eric Taucher]

One example of a needed proof would be that when making an SQLite API call, that the database schema does not change. Thinking along those lines many others should come to mind. We take these for granted and presume that databases ensure such ideas; having proofs to back these up should be much approachable with Lean 4.

Current line of thought is that SQLite schema cookie could be used.

[Arthur Paulino]

Posting here in case it helps: https://github.com/arthurpaulino/LeanMySQL
Note: last updated 3 years ago.

[Anthony Wang]

There's also https://github.com/BRonen/sqlite3-lean4/ and https://github.com/alex-wellbelove/lean_sqlite but both are very incomplete.

[Srayan Jana]

Yeah okay so, if you guys want to pull this off, you should probably take a look at the lakefile that I made for SDL. I'm pretty sure you could do a similar setup for SQLite:
https://github.com/ValorZard/lean-sdl3/blob/master/lakefile.lean

[Srayan Jana]

I found that building the c library from source and then linking it was more consistent on both windows and linux then trying to figure out where the binary is

[Srayan Jana]

Ah it might be more annoying for SQLite since it doesn't use cmake, and also expects you to have TCL installed somewhere on your system

[Srayan Jana]

I guess what would be neat is to have a few ways of using the library

1. relying on a system installed version of SQLite
2. Bundling a vendored version of SQlite built from source
3. Somehow prebuilding SQlite and bundling together with the library into one binary

[Srayan Jana]

builing BRonen's sqlite3-lean4 and yeah it doesn't work on windows

C:\github\sqlite3-lean4>lake build
info: downloading https://releases.lean-lang.org/lean4/v4.10.0/lean-4.10.0-windows.tar.zst
191.8 MiB / 191.8 MiB (100 %)  36.5 MiB/s ETA:   0 s
info: installing C:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.10.0
info: LSpec: cloning https://github.com/argumentcomputer/lspec/ to '.\.\.lake/packages\LSpec'
Γ£û [2/10] Building sqlite/sqliteffi.o
trace: .> clang -c -o .\.\.lake\build\native\sqliteffi.o .\.\native\ffi.c -I c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.10.0\include -I/nix/store/8r55amvr43sm771rgm0sszd05rm8j1cr-sqlite-3.46.0-dev/include/ -fPIC
info: stderr:
In file included from .\.\native\ffi.c:1:
C:/Users/sraya/.elan/toolchains/leanprover--lean4---v4.10.0/include/lean/lean.h:8:10: fatal error: 'stddef.h' file not found
#include <stddef.h>
         ^~~~~~~~~~
1 error generated.
error: external command 'clang' exited with code 1
Some builds logged failures:
- sqlite/sqliteffi.o
error: build failed

C:\github\sqlite3-lean4>

This is because the version of clang bundled with Lean is missing a bunch of headers necessary for stuff like this to be compiled properly

[Srayan Jana]

https://github.com/ValorZard/sqlite3-lean4.git
made a fork and currently attempting to get this to build properly

[Srayan Jana]

Currently getting stuck here:

sraya@Penelope MSYS /c/github/sqlite3-lean4
$ "C:\Users\sraya\.elan\bin\lake.exe" build
info: LSpec: cloning https://github.com/argumentcomputer/lspec/
info: LSpec: checking out revision '8a51034d049c6a229d88dd62f490778a377eec06'
✖ [9/11] Running sqlite/libsqlite.static
info: Cloning https://github.com/SQLite/SQLite.git into C:\github\sqlite3-lean4\vendor\sqlite
info: https://github.com/SQLite/SQLite.git cloned successfully
info:
info: Building C:\github\sqlite3-lean4\vendor\sqlite with args #[]
error: unspecified system_category error (error code: 193)
Some required targets logged failures:
- sqlite/libsqlite.static
error: build failed

sraya@Penelope MSYS /c/github/sqlite3-lean4
$

[Srayan Jana]

David Richter said:

Hi, I am trying to wrap sqlite https://github.com/drcicero/sqlite.lean

However, when building i get a lot of errors of style undefined reference due to --no-allow-shlib-undefined

$ lake clean; lake exe test
info: [0/4] Compiling leansqlite3.c
info: [0/4] Creating libleansqlite3.a
info: [0/4] Linking libleansqlite3.so
info: [0/4] Building Sqlite
info: [1/4] Compiling Sqlite
info: [1/4] Building Test
info: stdout:
./././Test.lean:14:46: warning: unused variable `nmtp` [linter.unusedVariables]
info: [3/4] Compiling Test
info: [4/4] Linking test
error: > /home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/leanc -o ./.lake/build/bin/test ./.lake/build/ir/Test.c.o ./.lake/build/ir/Sqlite.c.o ./.lake/build/lib/libleansqlite3.a -lsqlite3
error: stderr:
ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_join@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: dlerror@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_mutexattr_destroy@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: exp@GLIBC_2.29
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_create@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: log@GLIBC_2.29
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: stat64@GLIBC_2.33
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_mutexattr_init@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: fstat64@GLIBC_2.33
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: dlopen@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: fcntl64@GLIBC_2.28
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: lstat64@GLIBC_2.33
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_mutexattr_settype@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: dlsym@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_mutex_trylock@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pow@GLIBC_2.29
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: dlclose@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/leanc` exited with code 1

I found another library https://github.com/arthurpaulino/LeanMySQL/blob/master/lakefile.lean which simply adds "-L/usr/lib/x86_64-linux-gnu/" to the moreLinkArgs. If I do that it works for me and I can run some simple queries:

$ lake clean; lake exe test
info: [0/4] Compiling leansqlite3.c
info: [0/4] Creating libleansqlite3.a
info: [0/4] Linking libleansqlite3.so
info: [0/4] Building Sqlite
info: [1/4] Compiling Sqlite
info: [1/4] Building Test
info: stdout:
./././Test.lean:14:46: warning: unused variable `nmtp` [linter.unusedVariables]
info: [3/4] Compiling Test
info: [4/4] Linking test
3.37.2
> SELECT SQLITE_VERSION()
  [(SQLITE_VERSION(), 3)]
  [3.37.2]
  DONE 101
> DROP TABLE IF EXISTS Cars
  []
  DONE 101
> CREATE TABLE Cars(Id INT, Name TEXT, Price INT)
  []
  DONE 101
> INSERT INTO Cars VALUES (1, 'Audi', 52642), (2, 'Mercedes', 57127), (3, 'Skoda', 9000)
  []
  DONE 101
> INSERT INTO Cars VALUES (4, 'Volvo', 29000), (5, 'Bentley', 350000), (6, 'Citroen', 21000)
  []
  DONE 101
> INSERT INTO Cars VALUES (7, 'Hummer', 41400), (8, 'Volkswagen', 21600)
  []
  DONE 101
> SELECT * FROM sqlite_master
  [(type, 3), (name, 3), (tbl_name, 3), (rootpage, 1), (sql, 3)]
  [table, Cars, Cars, 2, CREATE TABLE Cars(Id INT, Name TEXT, Price INT)]
  DONE 101
> SELECT * FROM Cars
  [(Id, 1), (Name, 3), (Price, 1)]
  [1, Audi, 52642]
  [2, Mercedes, 57127]
  [3, Skoda, 9000]
  [4, Volvo, 29000]
  [5, Bentley, 350000]
  [6, Citroen, 21000]
  [7, Hummer, 41400]
  [8, Volkswagen, 21600]
  DONE 101
> SELECT * FROM Cars WHERE Price > 29000
  [(Id, 1), (Name, 3), (Price, 1)]
  [1, Audi, 52642]
  [2, Mercedes, 57127]
  [5, Bentley, 350000]
  [7, Hummer, 41400]
  DONE 101
> SELECT Name FROM Cars WHERE Price > 29000
  [(Name, 3)]
  [Audi]
  [Mercedes]
  [Bentley]
  [Hummer]
  DONE 101

However, I suppose that would make the library platform-dependent, which is unsatisfying? I'm wondering whether there is a better way.

A similar error was posted twice in the past, and Sebastian Ullrich responded with:

It seems the library requires a newer version of glibc than Lean targets. When you interface with system libs, it is safer to compile under LEAN_CC=cc in order to use the system C compiler.

However, that doesn't work for me either:

$ lake clean; LEAN_CC=cc lake exe test
info: [0/4] Compiling leansqlite3.c
info: [0/4] Creating libleansqlite3.a
info: [0/4] Linking libleansqlite3.so
info: [0/4] Building Sqlite
info: [1/4] Compiling Sqlite
info: [1/4] Building Test
info: stdout:
./././Test.lean:14:46: warning: unused variable `nmtp` [linter.unusedVariables]
info: [3/4] Compiling Test
info: [4/4] Linking test
error: > /home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/leanc -o ./.lake/build/bin/test ./.lake/build/ir/Test.c.o ./.lake/build/ir/Sqlite.c.o ./.lake/build/lib/libleansqlite3.a -L/usr/lib/x86_64-linux-gnu/ -lsqlite3
error: stderr:
/usr/bin/ld: cannot find -lc++: No such file or directory
/usr/bin/ld: cannot find -lc++abi: No such file or directory
collect2: error: ld returned 1 exit status
error: external command `/home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/leanc` exited with code 1

Any ideas?

[Srayan Jana]

Found another lean bindings for SQlite, really the main issue seems to be how to bundle SQlite with Lean, writing the actual C bindings is the easy part

[Anthony Wang]

We have a few options (similar to your list above):

1. Don't bundle SQLite and have the user figure it out themselves. On many Linux distros at least, it's easy to install the SQLite header files with something like apt install libsqlite3-dev.
2. The SQLite source code is also available as a single file so we could simply vendor that in our repo and compile and link against it.
3. We could use the Nix package manager along with lean4-nix but users might be annoyed by needing to install Nix in order to use the SQLite bindings.

[Arthur Paulino]

I would prefer option 2 as an user

[Anthony Wang]

Srayan Jana said:

Ah it might be more annoying for SQLite since it doesn't use cmake, and also expects you to have TCL installed somewhere on your system

I just tried compiling the single-file version of SQLite on my Linux computer using gcc main.h sqlite3.c sqlite3.h and it worked perfectly, no Tcl necessary.

[Eric Taucher]

On the Windows side, using vcpkg with manifest mode (local install vs global install) and using MS Visual C++ (CL) compiler with just the command line tools, no need to do a full install of Visual Studio. Since MS Visual C++ come with a version of CMake, a compile of an SQLite demo on WIndows 11 from the command line worked as expected. SQLite3 DLL was installed with .\vcpkg\vcpkg.exe install --triplet=x64-windows and a properly configured vcpkg.json and vcpkg-configuration.json installed the needed Windows SQLite DLL and other needed files.

vcpkg files installed for SQLite3

C:\Users\Groot\Projects\sqlite_lean_demo\vcpkg\packages\sqlite3_x64-windows>tree /A /F
.
| BUILD_INFO
| CONTROL
|
+---bin
| sqlite3.dll
| sqlite3.pdb
|
+---debug
| +---bin
| | sqlite3.dll
| | sqlite3.pdb
| |
| \---lib
| | sqlite3.lib
| |
| \---pkgconfig
| sqlite3.pc
|
+---include
| sqlite3-vcpkg-config.h
| sqlite3.h
| sqlite3ext.h
|
+---lib
| | sqlite3.lib
| |
| \---pkgconfig
| sqlite3.pc
|
\---share
+---sqlite3
| copyright
| usage
| vcpkg.spdx.json
| vcpkg_abi_info.txt
|
\---unofficial-sqlite3
unofficial-sqlite3-config.cmake
unofficial-sqlite3-targets-debug.cmake
unofficial-sqlite3-targets-release.cmake
unofficial-sqlite3-targets.cmake

Holding off on posting the details because they may not be easily reproducible for a novice programmer. As the 8-ball would say Outlook good.

[Srayan Jana]

oo i didn't know about the single file version. ill use that instead

[Srayan Jana]

@Anthony Wang https://github.com/BRonen/sqlite3-lean4/pull/1
got sqlite working

[Anthony Wang]

Awesome! I was able to compile your PR painlessly. I'm now trying to modernize the test suite and get it to pass all the tests again.

[Anthony Wang]

I made a fork and pushed my changes to it, although one test is still mysteriously failing: https://github.com/usernamenotavailablepleasechooseanother/sqlite3-lean4/commit/4536f096ac3c7b4338929845ab9e3912c012f350

[Srayan Jana]

@Anthony Wang you can submit a PR to my fork and i can merge it

[Srayan Jana]

@Brenno Rodrigues is the guy who owns the parent repository. Hello!

[Srayan Jana]

As an aside, I wish Lean had a less annoying way of doing the c compiler stuff. It's weird that Lean comes bundled with a c compiler, and yet its not very useful since its missing a bunch of headers

[Anthony Wang]

I don't think SQLite needs any headers other than the C standard library, since I was able to successfully compile this project using the bundled leanc compiler.

[Srayan Jana]

hm okay, i guess we just gotta link to that instead then. how did you do that btw?

[Anthony Wang]

I changed the line in the lakefile to def compiler := "leanc" and it just worked™.

[Brenno Rodrigues]

Hello! I’m happy to see that my SQLite bindings might be useful. I’ll keep following the discussion, and let me know if there’s anything I can do to help.

[Srayan Jana]

Anthony Wang said:

I changed the line in the lakefile to def compiler := "leanc" and it just worked™.

Oh yeah, that just worked. Neat! No external dependencies!

[Locria Cyber]

Building a persistent extension of Janet is in my backlog. Binding Sqlite3 is not that difficult, as the database logic is on the Sqlite3 side. Since Sqlite3 is not a column database, many use cases can use a network database instead.

tl;dr, Build a network database with Janet object model. It does not have to be fast.

[Locria Cyber]

Prior art: Metakit, whitedb

Janet as a query language is much better than SQL.

[Anthony Wang]

Thanks for the suggestion, but it's off-topic for this project since we already decided on using SQLite. (but feel free to start your own project for Lean bindings to other DBs!)

[Arthur Paulino]

This is more or less related, but one thing that's been in my mind is the creation of Lean bindings for Apache Spark.

Data pipelines could definitely benefit from stronger guarantees that can be achieved with a richer type system. For a single-point example, joining two dataframes is only valid if the joint key is present on both sides. Ideally, such errors should happen at compilation time so the ETL doesn't break at 3am.

[Anthony Wang]

Anthony Wang said:

Awesome! I was able to compile your PR painlessly. I'm now trying to modernize the test suite and get it to pass all the tests again.

Finally found the bug: cursor.bindInt 1 69 actually ends up using 34 instead of 69, since the code was unboxing an already unboxed int32.

[Srayan Jana]

Anthony Wang said:

Anthony Wang said:

Awesome! I was able to compile your PR painlessly. I'm now trying to modernize the test suite and get it to pass all the tests again.

Finally found the bug: cursor.bindInt 1 69 actually ends up using 34 instead of 69, since the code was unboxing an already unboxed int32.

Neat! Send me a PR my way and I'll merge it

[Srayan Jana]

or, what would probably be better
@Brenno Rodrigues you can merge what I have so far, and then Anthony could submit his PR later

[Srayan Jana]

Oh i see you already gave me a pull request for it

[Srayan Jana]

@Anthony Wang

C:\github\sqlite3-lean4>lake build
ℹ [6/12] Replayed sqlite/sqlite.o
info: stderr:
cc1.exe: warning: C:\github\sqlite3-lean4\native\sqlite3.h: not a directory
cc1.exe: warning: C:\github\sqlite3-lean4\native\sqlite3ext.h: not a directory
✖ [7/12] Building sqlite/sqliteffi.o
trace: .> leanc -c -o C:\github\sqlite3-lean4\native\sqliteffi.o C:\github\sqlite3-lean4\native\sqliteffi.c -I c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\include -I C:\github\sqlite3-lean4\native -fPIC
info: stderr:
C:\github\sqlite3-lean4\native\sqliteffi.c:3:10: fatal error: 'stdio.h' file not found
    3 | #include <stdio.h>
      |          ^~~~~~~~~
1 error generated.
error: external command 'leanc' exited with code 1
Some required targets logged failures:
- sqlite/sqliteffi.o
error: build failed

C:\github\sqlite3-lean4>

[Srayan Jana]

Merging your PR breaks building it using lean's built in C compiler

[Srayan Jana]

@Mac Malone this is something I've run into a bunch of times at this point, do you know why leanc doesn't come with stdio.h?

[Mac Malone]

@Srayan Jana Lean comes with minimal C stdlib designed to support building the C code prdouce by lean. If a user needs more of the C standard library, the suggested approach is to use a standard C compiler available on the system rather than leanc to build the code. However, that can be inconvenient, as It makes the distribution of FFI packages more complex (downstream users then need to ensure they also install the proper C toolchain).

[Srayan Jana]

Yeah I really don't want to have to tell people to go and install clang or gcc if they don't need to (especially if your a Mathematician who just wants to use SQLite for stuff)

[Mac Malone]

This is something I would like to see improved in the future, but I am not sure when it will be a priority.

[Srayan Jana]

it also makes it annoying cuz i bet this builds perfectly fine on linux with leanc, but not on windows for whatever reason

[Mac Malone]

It might be worth making an issue on the Lean GitHub repoistory summarizing the difficulties. That could result in action on this front sooner.

[Srayan Jana]

@Mac Malone https://github.com/leanprover/lean4/issues/10831
Did it

[Srayan Jana]

For now, I guess i'll switch to using the CC environment variable

[Anthony Wang]

I also noticed this problem earlier today when trying to compile this project on Ubuntu (although it works fine on NixOS). The Lean developers have said in the past though that they prefer distributing only a minimal set of headers and that FFI projects should use external toolchains: https://github.com/leanprover/lean4/pull/733#issuecomment-948385438

[Srayan Jana]

Anthony Wang said:

I also noticed this problem earlier today when trying to compile this project on Ubuntu (although it works fine on NixOS). The Lean developers have said in the past though that they prefer distributing only a minimal set of headers and that FFI projects should use external toolchains: https://github.com/leanprover/lean4/pull/733#issuecomment-948385438

I think you could still leave a message/thumbs up on the issue and maybe we can get the lean devs to change their minds.

(Also, off topic, but I tried the CC solution you mentioned and it didn't work)

[Anthony Wang]

I tried using gcc instead of leanc on Ubuntu 25.10 and ran into this error:

✖ [31/31] Building Tests.Sqlite:exe
trace: .> /root/.elan/toolchains/leanprover--lean4---4.24.0/bin/clang -o /sqlite3-lean4/.lake/build/bin/Tests-Sqlite /sqlite3-lean4/.lake/build/ir/Tests/Sqlite.c.o.export /sqlite3-lean4/.lake/build/ir/Sqlite/FFI.c.o.export /sqlite3-lean4/.lake/build/ir/Sqlite.c.o.export /sqlite3-lean4/.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Control/DefaultRange.c.o.export /sqlite3-lean4/.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Control/Random.c.o.export /sqlite3-lean4/.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Gen.c.o.export /sqlite3-lean4/.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Sampleable.c.o.export /sqlite3-lean4/.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Checkable.c.o.export /sqlite3-lean4/.lake/packages/LSpec/.lake/build/ir/LSpec/LSpec.c.o.export /sqlite3-lean4/.lake/packages/LSpec/.lake/build/ir/LSpec/Instances.c.o.export /sqlite3-lean4/.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck.c.o.export /sqlite3-lean4/.lake/packages/LSpec/.lake/build/ir/LSpec.c.o.export /sqlite3-lean4/.lake/build/lib/libsqliteffi.a -L /root/.elan/toolchains/leanprover--lean4---4.24.0/lib/lean --sysroot /root/.elan/toolchains/leanprover--lean4---4.24.0 -L /root/.elan/toolchains/leanprover--lean4---4.24.0/lib -L /root/.elan/toolchains/leanprover--lean4---4.24.0/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -lLake -Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed -lm -ldl -pthread
info: stderr:
ld.lld: error: undefined symbol: fcntl64
>>> referenced by sqlite3.c
>>>               sqlite3.o:(aSyscall) in archive /sqlite3-lean4/.lake/build/lib/libsqliteffi.a
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/root/.elan/toolchains/leanprover--lean4---4.24.0/bin/clang' exited with code 1
Some required targets logged failures:
- Tests.Sqlite:exe
error: build failed

My guess is because Ubuntu has a very recent glibc whereas Lean ships with a much older version, so it's failing when trying to link the gcc-compiled sqlite3.o with the other code compiled by leanc.

[Srayan Jana]

I had a similar error when setting compiler to "clang" on windows

PS C:\github\sqlite3-lean4> lake exe Tests.Sqlite
info: LSpec: cloning https://github.com/argumentcomputer/lspec/
info: LSpec: checking out revision '1fc461a9b83eeb68da34df72cec2ef1994e906cb'
✖ [3/31] Building sqlite/sqliteffi.o
trace: .> clang -c -o C:\github\sqlite3-lean4\native\sqliteffi.o C:\github\sqlite3-lean4\native\sqliteffi.c -I c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\include -I C:\github\sqlite3-lean4\native -fPIC
info: stderr:
In file included from C:\github\sqlite3-lean4\native\sqliteffi.c:1:
C:/Users/sraya/.elan/toolchains/leanprover--lean4---v4.24.0/include/lean/lean.h:8:10: fatal error: 'stddef.h' file not found
    8 | #include <stddef.h>
      |          ^~~~~~~~~~
1 error generated.
error: external command 'clang' exited with code 1
✖ [4/31] Building sqlite/sqlite.o
trace: .> clang -c -o C:\github\sqlite3-lean4\native\sqlite3.o C:\github\sqlite3-lean4\native\sqlite3.c -I C:\github\sqlite3-lean4\native -fPIC
info: stderr:
C:\github\sqlite3-lean4\native\sqlite3.c:354:10: fatal error: 'stdarg.h' file not found
  354 | #include <stdarg.h>     /* Needed for the definition of va_list */
      |          ^~~~~~~~~~
1 error generated.
error: external command 'clang' exited with code 1
Some required targets logged failures:
- sqlite/sqliteffi.o
- sqlite/sqlite.o
error: build failed
PS C:\github\sqlite3-lean4>

[Anthony Wang]

Anthony Wang said:

My guess is because Ubuntu has a very recent glibc whereas Lean ships with a much older version, so it's failing when trying to link the gcc-compiled sqlite3.o with the other code compiled by leanc.

"Solved" this issue using a very gross hack in the lakefile: moreLinkArgs := #["-Wl,--unresolved-symbols=ignore-all"]

[Srayan Jana]

If I remember, moreLinkArgs does not get inherited by projects that use this as a dependency, so whoever uses this library will also have to pass that arg in, which is not great

[Srayan Jana]

Mac Malone said:

moreLinkArgs are not inherited, so you may need to add it to the lean_exe (in lean-sdl-test) as well.

[Srayan Jana]

Seems like if we want to distribute this library at all, we might just have to "fix" leanc itself

[Anthony Wang]

Srayan Jana said:

I had a similar error when setting compiler to "clang" on windows

c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\include is the directory for Lean's bundled headers, so on your computer, which files are in there? Is there stddef.h?

[Srayan Jana]

image.png

[Anthony Wang]

What's in the clang folder?

[Srayan Jana]

image.png

[Anthony Wang]

Huh, so it is in there. What's the output of running that clang command manually? Also, there's a c:\ instead of C:\, so could that be the problem?

[Srayan Jana]

PS C:\github\sqlite3-lean4> clang -c -o C:\github\sqlite3-lean4\native\sqliteffi.o C:\github\sqlite3-lean4\native\sqliteffi.c -I c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\include -I C:\github\sqlite3-lean4\native -fPIC
clang: error: unsupported option '-fPIC' for target 'x86_64-pc-windows-msvc'
PS C:\github\sqlite3-lean4> ```

[Anthony Wang]

Oh wait I'm dumb, this is for compiling sqliteffi.o so we should be using the system toolchain's headers instead of Lean's bundled headers, so maybe there's something wrong with your clang installation?

(Ignore the stuff I said about `c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\include, it's probably not relevant)

[Srayan Jana]

ugh for some reason its using the swift version of LLVM???

PS C:\github\sqlite3-lean4> lake exe Tests.Sqlite
✖ [27/31] Building sqlite/sqliteffi.o
trace: .> clang -c -o C:\github\sqlite3-lean4\native\sqliteffi.o C:\github\sqlite3-lean4\native\sqliteffi.c -I c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\include -I C:\github\sqlite3-lean4\native -fPIC
info: stderr:
In file included from C:\github\sqlite3-lean4\native\sqliteffi.c:1:
C:/Users/sraya/.elan/toolchains/leanprover--lean4---v4.24.0/include/lean/lean.h:8:10: fatal error: 'stddef.h' file not found
    8 | #include <stddef.h>
      |          ^~~~~~~~~~
1 error generated.
error: external command 'clang' exited with code 1
✖ [28/31] Building sqlite/sqlite.o
trace: .> clang -c -o C:\github\sqlite3-lean4\native\sqlite3.o C:\github\sqlite3-lean4\native\sqlite3.c -I C:\github\sqlite3-lean4\native -fPIC
info: stderr:
C:\github\sqlite3-lean4\native\sqlite3.c:354:10: fatal error: 'stdarg.h' file not found
  354 | #include <stdarg.h>     /* Needed for the definition of va_list */
      |          ^~~~~~~~~~
1 error generated.
error: external command 'clang' exited with code 1
Some required targets logged failures:
- sqlite/sqliteffi.o
- sqlite/sqlite.o
error: build failed
PS C:\github\sqlite3-lean4> clang -v
clang version 19.1.5
Target: x86_64-unknown-windows-msvc
Thread model: posix
InstalledDir: C:\Users\sraya\AppData\Local\Programs\Swift\Toolchains\6.2.0+Asserts\usr\bin
Build config: +assertions
PS C:\github\sqlite3-lean4>

[Anthony Wang]

Yeah that would explain it.

[Anthony Wang]

Have you tried using WSL to compile it?

[Anthony Wang]

Arthur Paulino said:

Posting here in case it helps: https://github.com/arthurpaulino/LeanMySQL
Note: last updated 3 years ago.

I'm currently reading the code for LeanMySQL since we might be able to borrow large portions of SQLDSL.lean and SQLSyntax.lean for our SQLite project.

[Srayan Jana]

@Anthony Wang

sraya@Penelope:~/sqlite3-lean4$ lake build
info: downloading https://releases.lean-lang.org/lean4/v4.24.0/lean-4.24.0-linux.tar.zst
438.3 MiB / 438.3 MiB (100 %)   9.7 MiB/s ETA:   0 s
info: installing /home/sraya/.elan/toolchains/leanprover--lean4---v4.24.0
info: LSpec: cloning https://github.com/argumentcomputer/lspec/
info: LSpec: checking out revision '1fc461a9b83eeb68da34df72cec2ef1994e906cb'
✖ [2/12] Building sqlite/sqliteffi.o
trace: .> leanc -c -o /home/sraya/sqlite3-lean4/native/sqliteffi.o /home/sraya/sqlite3-lean4/native/sqliteffi.c -I /home/sraya/.elan/toolchains/leanprover--lean4---v4.24.0/include -I /home/sraya/sqlite3-lean4/native -fPIC
info: stderr:
/home/sraya/sqlite3-lean4/native/sqliteffi.c:3:10: fatal error: 'stdio.h' file not found
    3 | #include <stdio.h>
      |          ^~~~~~~~~
1 error generated.
error: external command 'leanc' exited with code 1
✖ [7/12] Building sqlite/sqlite.o
trace: .> leanc -c -o /home/sraya/sqlite3-lean4/native/sqlite3.o /home/sraya/sqlite3-lean4/native/sqlite3.c -I /home/sraya/sqlite3-lean4/native -fPIC
info: stderr:
/home/sraya/sqlite3-lean4/native/sqlite3.c:15049:10: fatal error: 'stdio.h' file not found
 15049 | #include <stdio.h>
       |          ^~~~~~~~~
1 error generated.
error: external command 'leanc' exited with code 1
Some required targets logged failures:
- sqlite/sqliteffi.o
- sqlite/sqlite.o
error: build failed
sraya@Penelope:~/sqlite3-lean4$

i get this same error on ubuntu ugh

[Anthony Wang]

Can you try building my fork? It has a commit that should fix that problem.

[Srayan Jana]

sraya@Penelope:~/sqlite3-lean4$ cd ..
sraya@Penelope:~$ rm -rf /sqlite3-lean4
sraya@Penelope:~$ ls
SDL  guile  life  sdl3-hs  sqlite3-lean4
sraya@Penelope:~$ explorer.exe .
sraya@Penelope:~$ git clone https://github.com/usernamenotavailablepleasechooseanother/sqlite3-lean4.git
Cloning into 'sqlite3-lean4'...
remote: Enumerating objects: 263, done.
remote: Counting objects: 100% (263/263), done.
remote: Compressing objects: 100% (104/104), done.
remote: Total 263 (delta 122), reused 236 (delta 98), pack-reused 0 (from 0)
Receiving objects: 100% (263/263), 2.75 MiB | 7.89 MiB/s, done.
Resolving deltas: 100% (122/122), done.
sraya@Penelope:~$ cd s
sdl3-hs/       sqlite3-lean4/
sraya@Penelope:~$ cd sqlite3-lean4/
sraya@Penelope:~/sqlite3-lean4$ lake build
info: LSpec: cloning https://github.com/argumentcomputer/lspec/
info: LSpec: checking out revision '1fc461a9b83eeb68da34df72cec2ef1994e906cb'
ℹ [2/12] Built sqlite/sqliteffi.o
info: stderr:
/home/sraya/sqlite3-lean4/native/sqliteffi.c: In function ‘connection_finalize’:
/home/sraya/sqlite3-lean4/native/sqliteffi.c:29:33: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘void *’ [-Wformat=]
   29 |   printf("connection_finalize: %x\n", conn);
      |                                ~^     ~~~~
      |                                 |     |
      |                                 |     void *
      |                                 unsigned int
      |                                %p
/home/sraya/sqlite3-lean4/native/sqliteffi.c: In function ‘cursor_finalize’:
/home/sraya/sqlite3-lean4/native/sqliteffi.c:37:29: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘void *’ [-Wformat=]
   37 |   printf("cursor_finalize: %x\n", cursor);
      |                            ~^     ~~~~~~
      |                             |     |
      |                             |     void *
      |                             unsigned int
      |                            %p
/home/sraya/sqlite3-lean4/native/sqliteffi.c: In function ‘lean_sqlite_open’:
/home/sraya/sqlite3-lean4/native/sqliteffi.c:52:35: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘sqlite3 *’ [-Wformat=]
   52 |   printf("initialize_connection: %x\n", conn);
      |                                  ~^     ~~~~
      |                                   |     |
      |                                   |     sqlite3 *
      |                                   unsigned int
/home/sraya/sqlite3-lean4/native/sqliteffi.c: In function ‘lean_sqlite_prepare’:
/home/sraya/sqlite3-lean4/native/sqliteffi.c:72:31: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘sqlite3_stmt *’ [-Wformat=]
   72 |   printf("initialize_cursor: %x\n", cursor);
      |                              ~^     ~~~~~~
      |                               |     |
      |                               |     sqlite3_stmt *
      |                               unsigned int
Build completed successfully (12 jobs).
sraya@Penelope:~/sqlite3-lean4$

[Srayan Jana]

yippe! lemme try this on windows real quick

[Srayan Jana]

PS C:\github\sqlite3-lean4-wang> lake build
info: LSpec: cloning https://github.com/argumentcomputer/lspec/
info: LSpec: checking out revision '1fc461a9b83eeb68da34df72cec2ef1994e906cb'
✖ [2/12] Building sqlite/sqlite.o
trace: .> cc -c -o C:\github\sqlite3-lean4-wang\native\sqlite3.o C:\github\sqlite3-lean4-wang\native\sqlite3.c -I C:\github\sqlite3-lean4-wang\native -fPIC
error: failed to execute 'cc': no such file or directory (error code: 2)
✖ [3/12] Building sqlite/sqliteffi.o
trace: .> cc -c -o C:\github\sqlite3-lean4-wang\native\sqliteffi.o C:\github\sqlite3-lean4-wang\native\sqliteffi.c -I c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\include -I C:\github\sqlite3-lean4-wang\native -fPIC
error: failed to execute 'cc': no such file or directory (error code: 2)
Some required targets logged failures:
- sqlite/sqlite.o
- sqlite/sqliteffi.o
error: build failed
PS C:\github\sqlite3-lean4-wang>

[Srayan Jana]

yep as expected fails on windows (on my computer at least)

[Srayan Jana]

PS C:\Users\sraya> echo $Env:CC
C:\Users\sraya\scoop\apps\gcc\current\bin
PS C:\Users\sraya>

[Srayan Jana]

so, what should we do now? think we should go back and just have it so that you need gcc on your computer to compile it?

[Anthony Wang]

I think we should first merge the two PRs and move on for now to working on other features like embedding SQL syntax into Lean. Maybe the Lean bug you created about leanc missing headers might get fixed in the future, or we come up with other ideas for making compilation less painful. So we shouldn't let it be a blocker for now, as long as you have some workaround for compiling it (I think you said WSL works).

[Srayan Jana]

Yeah I guess we just have to tell people to use Linux or WSL for now

[Srayan Jana]

@Brenno Rodrigues think we’re ready to merge (make sure to test on your computer first though)

[Srayan Jana]

If anyone else here is using windows, I’d appreciate if people could test on their computer as well

[Srayan Jana]

We should add a reference to this issue on the readme explaining why we recommend sticking with Linux for now (https://github.com/leanprover/lean4/issues/10831)

[Brenno Rodrigues]

I’ll take a look and merge later. I can also try testing on a windows machine I have here too

[Brenno Rodrigues]

I tested it on both Linux and Windows and it worked pretty well, merged.
Also, do you guys want to keep the github action? I fixed it to run without the old Nix setup.
https://github.com/BRonen/sqlite3-lean4/pull/2

[Eric Taucher]

Brenno Rodrigues said:

tested it on both Linux and Windows

As I have an interest in Lean code that works on Windows might also test it on Windows, but at present not sure of exactly what it is, can you provide the details for just Windows.

If this requires the use of WSL then will pass on trying it.

[Brenno Rodrigues]

I didn’t use WSL, I installed MinGW and set the compiler with

$Env:CC = "C:\MinGW\bin\gcc.exe"

and then ran lake test.
I saw you mentioned using the Visual Studio compiler earlier in the thread, but I didn't test with that setup.

[Eric Taucher]

(deleted)

[Eric Taucher]

Brenno Rodrigues said:

I didn’t use WSL, I installed MinGW and set the compiler with

$Env:CC = "C:\MinGW\bin\gcc.exe"

and then ran lake test.

Hope to give that a try later, maybe today.

Thanks.

[Eric Taucher]

(deleted)

[Eric Taucher]

(deleted)

[Eric Taucher]

A related topic on Lean FFI worth reading:

#lean4 > Understanding Lean's Foreign Function Interface (FFI)

[Srayan Jana]

@Anthony Wang @Brenno Rodrigues
I tried doing this on my own computer and got this

PS C:\github\sqlite3-lean4> $Env:CC = "C:\Users\sraya\scoop\apps\gcc\current\bin\gcc.exe"
PS C:\github\sqlite3-lean4> lake test
info: LSpec: cloning https://github.com/argumentcomputer/lspec/
info: LSpec: checking out revision '1fc461a9b83eeb68da34df72cec2ef1994e906cb'
✖ [31/31] Building Tests.SQLite:exe
trace: .> c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\bin\clang.exe -o C:\github\sqlite3-lean4\.lake\build\bin\Tests-SQLite.exe @C:\github\sqlite3-lean4\.lake\build\bin\Tests-SQLite.exe.rsp
info: stderr:
lld: error: unknown argument: --unresolved-symbols=ignore-all
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\bin\clang.exe' exited with code 1
Some required targets logged failures:
- Tests.SQLite:exe
error: build failed
PS C:\github\sqlite3-lean4>

[Srayan Jana]

I tried with a different gcc install, but no dice

PS C:\github\sqlite3-lean4> $Env:CC = "C:\Users\sraya\scoop\apps\msys2\current\usr\bin\gcc.exe"
PS C:\github\sqlite3-lean4> lake test
✖ [31/31] Building Tests.SQLite:exe
trace: .> c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\bin\clang.exe -o C:\github\sqlite3-lean4\.lake\build\bin\Tests-SQLite.exe @C:\github\sqlite3-lean4\.lake\build\bin\Tests-SQLite.exe.rsp
info: stderr:
lld: error: unknown argument: --unresolved-symbols=ignore-all
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\bin\clang.exe' exited with code 1
Some required targets logged failures:
- Tests.SQLite:exe
error: build failed

[Srayan Jana]

Tried inside MSYS2 itself, and still no dice

sraya@Penelope MSYS /c/github/sqlite3-lean4
$ "C:\Users\sraya\.elan\bin\lake.exe" test
✖ [31/31] Building Tests.SQLite:exe
trace: .> c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\bin\clang.exe -o C:\github\sqlite3-lean4\.lake\build\bin\Tests-SQLite.exe @C:\github\sqlite3-lean4\.lake\build\bin\Tests-SQLite.exe.rsp
info: stderr:
lld: error: unknown argument: --unresolved-symbols=ignore-all
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\bin\clang.exe' exited with code 1
Some required targets logged failures:
- Tests.SQLite:exe
error: build failed

[Anthony Wang]

It looks like your gcc is working correctly, but the final step of linking sqlite.o with the compiled Lean code is failing. Maybe we should only use --unresolved-symbols=ignore-all on Linux? This appears to be what your lean-sdl3 lakefile does: https://github.com/ValorZard/lean-sdl3/blob/3582357b4c4028e04c3d3065a1b703fa3ae354fd/lakefile.lean#L173

[Anthony Wang]

I pushed a commit to my fork with that fix, @Srayan Jana could you try compiling it?

[Brenno Rodrigues]

Oh maybe I messed something up when testing? I was pretty sure it worked for me on Windows

[Eric Taucher]

(deleted)

[Srayan Jana]

Anthony Wang said:

I pushed a commit to my fork with that fix, Srayan Jana could you try compiling it?

This is what I got

PS C:\github\sqlite3-lean4-wang> $Env:CC = "C:\Users\sraya\scoop\apps\msys2\current\usr\bin\gcc.exe"
PS C:\github\sqlite3-lean4-wang> lake test
info: LSpec: cloning https://github.com/argumentcomputer/lspec/
info: LSpec: checking out revision '1fc461a9b83eeb68da34df72cec2ef1994e906cb'
✖ [3/31] Building sqlite/sqlite.o
trace: .> C:\Users\sraya\scoop\apps\msys2\current\usr\bin\gcc.exe -c -o C:\github\sqlite3-lean4-wang\.lake\build\sqlite3.o C:\github\sqlite3-lean4-wang\native\sqlite3.c -I C:\github\sqlite3-lean4-wang\native -fPIC
info: stderr:
C:/Users/sraya/scoop/apps/msys2/2025-08-30/usr/lib/gcc/x86_64-pc-cygwin/15.2.0/cc1.exe: error while loading shared libraries: ?: cannot open shared object file: No such file or directory
error: external command 'C:\Users\sraya\scoop\apps\msys2\current\usr\bin\gcc.exe' exited with code 1
✖ [6/31] Building sqlite/sqliteffi.o
trace: .> C:\Users\sraya\scoop\apps\msys2\current\usr\bin\gcc.exe -c -o C:\github\sqlite3-lean4-wang\.lake\build\sqliteffi.o C:\github\sqlite3-lean4-wang\native\sqliteffi.c -I c:\Users\sraya\.elan\toolchains\leanprover--lean4---v4.24.0\include -I C:\github\sqlite3-lean4-wang\native -fPIC
info: stderr:
C:/Users/sraya/scoop/apps/msys2/2025-08-30/usr/lib/gcc/x86_64-pc-cygwin/15.2.0/cc1.exe: error while loading shared libraries: ?: cannot open shared object file: No such file or directory
error: external command 'C:\Users\sraya\scoop\apps\msys2\current\usr\bin\gcc.exe' exited with code 1
Some required targets logged failures:
- sqlite/sqlite.o
- sqlite/sqliteffi.o
error: build failed
PS C:\github\sqlite3-lean4-wang>

[Srayan Jana]

oh weird, it works with w64devkit

PS C:\github\sqlite3-lean4-wang> $Env:CC = "C:\github\w64devkit\w64devkit\bin\gcc.exe"
PS C:\github\sqlite3-lean4-wang> lake test
test suite
  ✓ can select data

  ✓ can insert data

  ✓ can bind parameters

  ✓ can get column count

  ✓ handles invalid SQL syntax

  ✓ handles non-existent table

PS C:\github\sqlite3-lean4-wang>

[Srayan Jana]

There should be something in the readme explaining all of this lol

[Brenno Rodrigues]

Someone already knows why this happens? lol

[Srayan Jana]

Honestly? Windows is just weird man.

[Srayan Jana]

Added an issue for this: https://github.com/BRonen/sqlite3-lean4/issues/4

[Srayan Jana]

Once Anthony's PR gets merged, I'll do a PR that does a proper writeup in the README about all of this

[Brenno Rodrigues]

Go ahead, it’s merged now

[Srayan Jana]

@Brenno Rodrigues https://github.com/BRonen/sqlite-lean/pull/5
you can give this a look over (and try out the instructions I wrote)

[Srayan Jana]

@Mac Malone is there anything you would add to the explanation in the README? https://github.com/BRonen/sqlite-lean does that all sound about right?

[Eric Taucher]

(deleted)

[Eric Taucher]

(deleted)

[Eric Taucher]

(deleted)

[Markus Himmel]

Is there a reproducer for this issue? There was a possibly relevant bugfix between 4.24.0 and 4.25.0-rc1 (lean4#10444), so it would be good to know if the issue is still present on the lastest version.

[Eric Taucher]

Markus Himmel said:

Is there a reproducer for this issue?

Thanks for the info and asking.

I have not created a reproducer but will try and create one if needed. However if the issue has been fixed will be happy to upgrade to/past the fix and see if the issue is still present. I would much prefer to just make users aware of the item with the best course of action to just be up to a version that works correctly.

[Eric Taucher]

Markus Himmel said:

it would be good to know if the issue is still present on the latest version.

Short answer: After upgrading to v4.25.0-rc2 , no longer a problem for my project.

Thanks for the info. :slight_smile:

[Eric Taucher]

(deleted)

[Anthony Wang]

I ported a C program that I wrote a few years ago to use Lean and sqlite-lean instead: https://git.unnamed.website/slean/tree/Main.lean

The current sqlite-lean interface is pretty low-level and annoying to use so I've started working on a type-safe based on https://github.com/arthurpaulino/LeanMySQL.

[Srayan Jana]

@Anthony Wang do you think that the requirement for clang/gcc is a blocker for you?

[Srayan Jana]

(Also, is that new lean sqlite thing going to be a PR to the current repo or something new?)

[Anthony Wang]

1st question: No.
2nd: Yes.