low level external verifier?

Stream: general

[tangentstorm]

A few months ago, I was looking at a github repository with a low-level external verifier for lean proofs. I'm about 80% certain it was written in rust, but I can't find it anywhere. Can someone point me in the right direction?

[Johan Commelin]

Was it olean-rs? I don't know if that's a verifier.

[tangentstorm]

no, but that's very interesting!
i could have sworn it was a parser for this: https://github.com/leanprover/lean/blob/master/doc/export_format.md

[tangentstorm]

perhaps i was just hallucinating, or it would be on the list on that page. :D

[Mauricio Collares]

https://github.com/ammkrn/nanoda_lib?

[tangentstorm]

aha! yes, it was the old version of that. i was confused because the new README(s) didn't match what i remembered.. I was looking at this before: https://github.com/ammkrn/nanoda/blob/master/OLD_README.md

[tangentstorm]

thanks!