Spaces:
Sleeping
Sleeping
调整 mathlib 预编译缓存下载和构建顺序
Browse files- Dockerfile +4 -1
Dockerfile
CHANGED
|
@@ -18,11 +18,14 @@ WORKDIR /app
|
|
| 18 |
RUN lake new eval_project math
|
| 19 |
WORKDIR /app/eval_project
|
| 20 |
|
|
|
|
|
|
|
|
|
|
| 21 |
# 构建 repl(单独仓库)。运行时用 `lake env` 提供 mathlib 环境。
|
| 22 |
WORKDIR /app
|
| 23 |
RUN git clone --depth 1 https://github.com/leanprover-community/repl.git /app/repl
|
| 24 |
WORKDIR /app/repl
|
| 25 |
-
RUN lake
|
| 26 |
|
| 27 |
# 回到 app 目录准备 Python 环境
|
| 28 |
WORKDIR /app
|
|
|
|
| 18 |
RUN lake new eval_project math
|
| 19 |
WORKDIR /app/eval_project
|
| 20 |
|
| 21 |
+
# 下载 mathlib 的预编译缓存并预构建(这里才有 `lake exe cache`)
|
| 22 |
+
RUN lake exe cache get && lake build
|
| 23 |
+
|
| 24 |
# 构建 repl(单独仓库)。运行时用 `lake env` 提供 mathlib 环境。
|
| 25 |
WORKDIR /app
|
| 26 |
RUN git clone --depth 1 https://github.com/leanprover-community/repl.git /app/repl
|
| 27 |
WORKDIR /app/repl
|
| 28 |
+
RUN lake build
|
| 29 |
|
| 30 |
# 回到 app 目录准备 Python 环境
|
| 31 |
WORKDIR /app
|