Zulip Chat Archive

Stream: lean4

Topic: Lean Protobuf


view this post on Zulip Zygimantas Straznickas (Mar 27 2021 at 16:44):

Hi everyone!
Announcing a protocol buffer implementation for Lean 4: https://github.com/zygi/lean-protoc-plugin. It includes both codegen and serialization/deserialization code. Unfortunately it uses a small amount of custom native code, so for now it's only conveniently available through Nix.

(Context for more math-focused users: this is infrastructure code, making it easier for Lean programs to interact with programs written in other programming languages)

view this post on Zulip Zygimantas Straznickas (Mar 27 2021 at 16:57):

(Also, big thanks to Lean 4 developers -- Lean 4 has been by far the smoothest functional programming experience I've ever had. Monad autolifting + pseudo-imperative notation is awesome! )


Last updated: May 07 2021 at 13:21 UTC