/lean4-protobuf

A WIP Protobuf package for Lean 4.

Primary LanguageLean

lean4-protobuf

A WIP Protobuf package for Lean 4.

Roadmap

  • Parsing of .proto files (except for MessageValue constants, adding this is a TODO).
  • Type definition codegen. (Planning to support both an import_protobuf macro for doing this at compile time, as well as a protoc plugin for if you want to view and commit the generated code.)
  • Encoding and decoding codegen. (Planning to do this with deriving ProtobufMessage.)
  • Passing Protobuf conformance tests.
  • Visibility refactor (ensure things that should be private are).
  • Good docs and examples.