lean and vscode remote containers

Stream: general

[Daniel Bush]

Hi there,
I'm a bit new to lean, but I've got the "doing math in lean" bug so I'm slowly working my way through TPIL.
I had a bit of a play with installing lean 3 in a docker container and using vscode's Remote Containers extension to make that container the development and shell environment within vscode. In case it's of use I've put it up here: https://github.com/danielbush/lean-remote-containers . Basically you get a self-contained virtualized lean environment (using debian linux) attached to your vscode. vscode effectively builds and installs lean for you via docker. Haven't really tested using lean this way in anger though.
Anyway, love this project.
Happy new year everyone!
Daniel