Welcome to Austin’s site

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....

Sometimes we know what we want to do with text even if we don’t know what the text is. Regular expressions are an important feature of many tools (programing languages, command line tools, etc.), but they play an especially important role in Vim. Text in Vim is first class, so all of Vim’s features should ultimately serve the purpose of editing text. Here we will explore some examples where regular expressions serve Vim well in this effort....

“To the man who only has a hammer, everything he encounters begins to look like a nail.” ― Abraham Maslow Word processors have monopolized the domain of text composition for the last quarter century. At their core, these programs involve text entry at the cursor, but with this function come a peripheral of features: formatting, grammar and spell checking, support for annotation. However, the essential functionality is simple: move the cursor with the mouse or the arrow keys and type or delete letters at the cursor....