Today I announce that Pantograph v0.2.13 has been sufficiently stable for usage.

Pantograph is a library for machine-to-machine interactions with Lean. It provides two interfaces:

1. A REPL interface via stdin/stdout
2. A C library interface via shared libraries (see Pantograph/Library.lean)

The documentations are included in README.md

For instructions on using the C library, see this guide

Pantograph provides the following features:

1. Interaction with Lean’s proof assistant features via tactics and proof terms
2. Inspection of the catalog
3. Inspection of symbols of an arbitrary Lean project
4. Typing calls to Lean’s kernel
5. Expression AST printing using s-expressions