Spaces:
Sleeping
Sleeping
LamZain commited on
Commit ·
3d52ca6
1
Parent(s): 34d7ab3
2026-01-26 test1
Browse files- Dockerfile +6 -0
Dockerfile
CHANGED
|
@@ -10,6 +10,9 @@ RUN apt-get update && apt-get install -y \
|
|
| 10 |
python3-pip \
|
| 11 |
&& rm -rf /var/lib/apt/lists/*
|
| 12 |
|
|
|
|
|
|
|
|
|
|
| 13 |
# Install elan (Lean version manager)
|
| 14 |
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y
|
| 15 |
ENV PATH="/root/.elan/bin:${PATH}"
|
|
@@ -27,6 +30,9 @@ RUN git clone --depth 1 https://github.com/leanprover-community/repl.git
|
|
| 27 |
WORKDIR /app/repl
|
| 28 |
RUN lake build
|
| 29 |
|
|
|
|
|
|
|
|
|
|
| 30 |
# Python setup
|
| 31 |
WORKDIR /app
|
| 32 |
COPY requirements.txt .
|
|
|
|
| 10 |
python3-pip \
|
| 11 |
&& rm -rf /var/lib/apt/lists/*
|
| 12 |
|
| 13 |
+
#Create python symlink (Debian has python3 but not python)
|
| 14 |
+
RUN ln -s /usr/bin/python3 /usr/bin/python
|
| 15 |
+
|
| 16 |
# Install elan (Lean version manager)
|
| 17 |
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y
|
| 18 |
ENV PATH="/root/.elan/bin:${PATH}"
|
|
|
|
| 30 |
WORKDIR /app/repl
|
| 31 |
RUN lake build
|
| 32 |
|
| 33 |
+
# (Optional): Verify REPL binary exists
|
| 34 |
+
RUN test -f /app/repl/.lake/build/bin/repl || (echo "REPL binary not found!" && exit 1)
|
| 35 |
+
|
| 36 |
# Python setup
|
| 37 |
WORKDIR /app
|
| 38 |
COPY requirements.txt .
|