mathlib3

2dabe5af - feat(.docker): Docker containers for debian, alpine, and gitpod (#6515)

feat(.docker): Docker containers for debian, alpine, and gitpod (#6515) # Docker containers The `.docker` directory contains instructions for building Docker containers with Lean and mathlib. ## Build You can build these containers using `scripts/docker_build.sh`. This will result in the creation of two containers: * `leanprovercommunity/lean` - contains elan, lean, and leanproject * `leanprovercommunity/mathlib` - additionally contains a copy of mathlib, with oleans In fact, for each container you'll get three different tags, `:debian`, `:alpine` and `:latest`. `:debian` and `:alpine` use those respective distributions, and `:latest` just points at `:debian`. Finally, there is also a `leanprovercommunity/mathlib:gitpod` for use at [https://gitpod.io/](https://gitpod.io/). ## Usage ### gitpod.io There is a container based on `gitpod/workspace-base` enabling [https://gitpod.io/](https://gitpod.io/) to create in-browser VSCode sessions with elan/lean/leanproject/mathlib already set up. Either prepend `https://gitpod.io/#` to basically any URL at github, e.g. [https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/docker](https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/docker), or install a [gitpod browser extension](https://www.gitpod.io/docs/browser-extension/) which will add buttons directly on github. ### Command line You can use these containers as virtual machines: ```sh docker run -it leanprovercommunity/mathlib ``` ### Docker registry These containers are deployed to the Docker registry, so anyone can just `docker run -it leanprovercommunity/mathlib` to get a local lean+mathlib environment. There is a local script in `scripts/docker_push.sh` for deployment, but I have also set up `hub.docker.com` to watch the `docker` branch for updates and automatically rebuild. If this PR is merged to master we should change that to watch `master`. ### Remote containers for VSCode Installing the `Remote - Containers` VSCode extension will allow you to open a project inside the `leanprovercommunity/mathlib` container (meaning you don't even need a local copy of lean installed). The file `/.devcontainer/devcontainer.json` sets this up: if you have the extension installed, you'll be prompted to ask if you'd like to run inside the container, no configuration necessary. Co-authored-by: Alex J. Best <alex.j.best@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>