search

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
222 stars 89 forks source link

Add docker / gitpod integrations #565

Open alexjbest opened 6 months ago

alexjbest commented 6 months ago

Mathlib has .docker and .devcontainer folders that (for one thing) make it easy to quickly load in to a fresh install of lean + mathlib (eg with gitpod.io). I think adding these to Std would be helpful

semorrison commented 5 months ago

PR welcome! :-)

Note that we're hoping to distribute Std directly with Lean itself (i.e. no require std required for projects that use it), but I think these integrations would remain just as useful even if we can pull that off.

alexjbest commented 5 months ago

Ok, I'll make a PR when I get a chance!