a lean4 template project with blueprints

Stream: general

[Walter Moreira]

I usually forget how I setup things in the past, and I have to re-think the issues I encounter. To mitigate that, I created a Lean4 template that includes Lean Blueprints, and a Nix development environment that tries to reduce the work of setting up a new Lean repository. I thought it could be interesting for some folks, particularly if they have been having issues setting up blueprints:

https://github.com/provables/lean4-template

It's kind of "opinionated" and it might not fit your use case (it barely fits mine :laughing: ), it's just scratching an itch at the moment. User beware!

Sample use:

nix run github:provables/lean4-template DEST_DIR
cd DEST_DIR/<my-project-name>
nix develop

This should give you a working Lean installation with blueprints and a task manager.