Using Lake's Internal API to Programatically Access the Lake Workspace
Sometimes it is useful to programmatically understand the structure of a Lean package or Lake environment. Lake’s internal API is a powerful tool, but isn’t always easy to access. In this post we will explore how to access Lake’s API and look at some example use cases. Alternatives to consider Before diving into Lake’s internal API, consider the following alternatives: manually parsing lakefile.{lean, toml} manually parsing lake-manifest.json. running lake check-test or lake check-lint to identify test_driver and lint_driver targets....