用于编译Lean源码的简易容器脚本
初步准备
系统要求
要求1core以上的处理器，至少2GB以上系统内存，2GB的交换空间；
要求40GB以上的磁盘空间，用于存放编译目录
必须使用支持Linux docker的操作系统
已经安装docker并能正常使用
使用方法
安装docker
复制执行，需要sudo或root权限，直接root执行请去掉sudo
export MYUSER=$(whoami)
sudo curl -sSL https://get.docker.com |bash ||sudo wget –qO- https://get.docker.com |bash
sudo usermod -aG docker $MYUSER #root用户不需要执行这条命令
生成命令
# 指定源码存放路径(自行修改)
export OPDIR=/opt/youdir
# 生成命令
su
