From 1e598126529eca0d95e03570c9babf042c36df17 Mon Sep 17 00:00:00 2001 From: Srayan Jana Date: Thu, 23 Oct 2025 13:55:15 -0700 Subject: [PATCH 1/4] Update README.md --- README.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/README.md b/README.md index 8dbe87b..8c684bd 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,20 @@ # SQLite Lean +## How to use/build +1. First, you are going to want to set the enviromental variable CC in order to build this library. + - 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. + - Instead we will have to use a seperate C compiler to link SQLite with our Lean code + - On Windows you can use [w64devkit](https://github.com/skeeto/w64devkit), and then set CC like so + ``$Env:CC = "C:\github\w64devkit\w64devkit\bin\gcc.exe"`` + Or wherever the version of gcc that comes with w64devkit is located +2. Then, you should be able to do ``lake test`` to see the library build properly +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 + - ``moreLinkArgs`` are not inherited by child projects + - Currently, that looks something like this + ```lean + moreLinkArgs := if !Platform.isWindows then #["-Wl,--unresolved-symbols=ignore-all"] else #[] -- TODO: Very gross hack + ``` + +## Notes + 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. From 53e0b17b317ba838051cd9680ed3ab3b90f8ec95 Mon Sep 17 00:00:00 2001 From: Srayan Jana Date: Thu, 23 Oct 2025 13:58:02 -0700 Subject: [PATCH 2/4] formatting + extra information --- README.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 8c684bd..6c5adf6 100644 --- a/README.md +++ b/README.md @@ -5,8 +5,14 @@ - 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. - Instead we will have to use a seperate C compiler to link SQLite with our Lean code - On Windows you can use [w64devkit](https://github.com/skeeto/w64devkit), and then set CC like so - ``$Env:CC = "C:\github\w64devkit\w64devkit\bin\gcc.exe"`` + ``` + $Env:CC = "C:\github\w64devkit\w64devkit\bin\gcc.exe" + ``` Or wherever the version of gcc that comes with w64devkit is located + - You can later remove this enviromental variable if you don't want to clutter your terminal like so + ``` + Remove-Item Env:CC + ``` 2. Then, you should be able to do ``lake test`` to see the library build properly 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 - ``moreLinkArgs`` are not inherited by child projects From 4323bec3503288b2ff0ee1191a37ddc26d95bad8 Mon Sep 17 00:00:00 2001 From: Srayan Jana Date: Thu, 23 Oct 2025 14:35:37 -0700 Subject: [PATCH 3/4] fix inaccuracy --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 6c5adf6..5b535f8 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ ## How to use/build 1. First, you are going to want to set the enviromental variable CC in order to build this library. - 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. - - Instead we will have to use a seperate C compiler to link SQLite with our Lean code + - Instead we will have to use a seperate C compiler to build SQLite and then we can use Lean's bundled lld linker to link it with our Lean code. - On Windows you can use [w64devkit](https://github.com/skeeto/w64devkit), and then set CC like so ``` $Env:CC = "C:\github\w64devkit\w64devkit\bin\gcc.exe" From b7058f286e6d0910126993b30a6a935a3d92a645 Mon Sep 17 00:00:00 2001 From: Srayan Jana Date: Thu, 23 Oct 2025 14:57:23 -0700 Subject: [PATCH 4/4] spelling Co-authored-by: Brenno Rodrigues --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 5b535f8..914378e 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ ## How to use/build 1. First, you are going to want to set the enviromental variable CC in order to build this library. - 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. - - Instead we will have to use a seperate C compiler to build SQLite and then we can use Lean's bundled lld linker to link it with our Lean code. + - 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. - On Windows you can use [w64devkit](https://github.com/skeeto/w64devkit), and then set CC like so ``` $Env:CC = "C:\github\w64devkit\w64devkit\bin\gcc.exe"