Lean Protobuf

Stream: lean4

[Zygimantas Straznickas]

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)

[Zygimantas Straznickas]

(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! )