Lean type checkers overview

Stream: general

[Kevin Buzzard]

I'm sorry for the naive question. Let's say I have some olean file called something random like liquid.olean and there's some sorry-free term in the corresponding Lean file called something random like first_target. I would like to run this term or this file through what I think is called a typechecker. Is it meaningful to ask for a complete list of typecheckers which can do this job?

[Kevin Buzzard]

Have now discovered very helpful Trepplein README https://github.com/leanprover/lean/blob/master/doc/export_format.md . Thanks @Gabriel Ebner !

[Chris B]

Per the readme's instructions, you need to produce a special export file. The typecheckers are:
https://github.com/leanprover-community/lean/tree/master/src/checker
https://github.com/gebner/trepplein.git
https://github.com/leanprover/tc
https://github.com/ammkrn/nanoda_lib