tydeu / lean4-alloy Goto Github PK
View Code? Open in Web Editor NEWWrite C shims from within Lean code.
License: Apache License 2.0
Write C shims from within Lean code.
License: Apache License 2.0
My Lean4 LSP starts with a C_INCLUDE_PATH variable set. This is inherited by the clangd server started by alloy (checked through /proc/<clang-pid>/environ
), but it doesn't pick up on the sqlite.h file in that include path.
If I edit a c file using the clangd LSP directly, it finds the header.
A lake build
is fine though. ๐คท
Hi, alloy sounds nice!
I wonder, how does one link a library -- in particular, with gcc for example, I would add the flag -lsqlite3
to link the library and make its symbols available. How would I add a -l
flag using alloy?
For example
sudo apt install sqlite3-dev
import Alloy.C
open scoped Alloy.C
alloy c include <lean/lean.h> <sqlite3.h> <stdio.h>
alloy c extern
def sqliteversion : BaseIO UInt32 :=
printf("%s\n", sqlite3_libversion())
return lean_io_result_mk_ok(lean_box(0))
$ lake build
...
error: stderr:
ld.lld: error: undefined symbol: sqlite3_libversion
>>> referenced by Sqlite.alloy.c:6 (./.lake/build/ir/Sqlite.alloy.c:6)
>>> ./.lake/build/ir/Sqlite.alloy.c.o:(_alloy_c_l_sqliteversion)
...
/home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/lean: symbol lookup error: ./.lake/build/lib/libSqlite-1.so: undefined symbol: sqlite3_libversion
It seems that if I change my .lean
file (Seccomp.lean
), it does not rebuild the .alloy.c.
file. I can make it do so by deleting it explicitly.
Here, loogle
is an executable using Seccomp
, and Seccomp.lean
has been changed:
~/build/lean/mathlib4 $ lake build loogle
[258/374] Building Seccomp
[372/374] Building Loogle.Main
~/build/lean/mathlib4 $ lake build +Seccomp:alloy.c
~/build/lean/mathlib4 $ rm ./build/ir/Seccomp.alloy.c
~/build/lean/mathlib4 $ lake build +Seccomp:alloy.c
Generating Seccomp alloy
~/build/lean/mathlib4 $ lake build loogle
[370/374] Compiling Seccomp alloy
[371/374] Linking Seccomp
[372/374] Building Loogle.Main
[374/374] Linking loogle
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.