Database access in Lean

Stream: general

[Fabian Huch]

If I wanted to access a database (e.g., postgres) from within lean, how could I do this? Would I have to implement a postgres driver in lean, or is there a way around that (for instance by re-using c++ libraries)?

[Henrik Böving]

Fabian Huch said:

If I wanted to access a database (e.g., postgres) from within lean, how could I do this? Would I have to implement a postgres driver in lean, or is there a way around that (for instance by re-using c++ libraries)?

Both of those are options, Lean has proper C FFI so you can write bindings to a postgres library or use projects like https://github.com/hargoniX/socket.lean to develop the protocol yourself.

[Fabian Huch]

Thanks!

[Florian Würmseer]

Hi @Fabian Huch , I was working on a toy implementation a while back https://github.com/FWuermse/lean-postgres. So far only insert and query operations are supported and the socket lib is outdated. However I'm planning on bumping the socket library and add missing operations througout my upcoming Semester.

[Fabian Huch]

Very cool, that's quite interesting!

[Arthur Paulino]

Also https://github.com/arthurpaulino/LeanMySQL