-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathDockerfile
More file actions
116 lines (85 loc) · 3.52 KB
/
Copy pathDockerfile
File metadata and controls
116 lines (85 loc) · 3.52 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
# syntax=docker/dockerfile:1.7
FROM node:22-bookworm-slim AS base
ENV CI=true \
NPM_CONFIG_UPDATE_NOTIFIER=false \
PIP_DISABLE_PIP_VERSION_CHECK=1 \
PIP_NO_CACHE_DIR=1 \
TRUTH_HARNESS_CONTAINER=1 \
TRUTH_HARNESS_MAXIMA=maxima-sage \
TRUTH_HARNESS_Z3=z3 \
TRUTH_HARNESS_CVC5=cvc5 \
PATH="/opt/truth-harness-python/bin:${PATH}"
RUN apt-get update \
&& apt-get install -y --no-install-recommends ca-certificates cvc5 graphviz maxima-sage maxima-sage-share python3 python3-pip python3-venv tini z3 \
&& python3 -m venv /opt/truth-harness-python \
&& /opt/truth-harness-python/bin/python -m pip install sympy==1.14.0 \
&& useradd --create-home --uid 10001 truth \
&& mkdir -p /workspace \
&& chown -R truth:truth /workspace /home/truth \
&& rm -rf /var/lib/apt/lists/*
USER truth
WORKDIR /workspace
COPY --chown=truth:truth package.json package-lock.json ./
COPY --chown=truth:truth apps/cli/package.json apps/cli/package.json
COPY --chown=truth:truth packages/benchmarks/package.json packages/benchmarks/package.json
COPY --chown=truth:truth packages/core/package.json packages/core/package.json
COPY --chown=truth:truth packages/mcp-server/package.json packages/mcp-server/package.json
RUN npm ci
COPY --chown=truth:truth . .
RUN npm run build
FROM base AS dev
ENTRYPOINT ["tini", "--"]
CMD ["npm", "run", "check"]
FROM dev AS verify
RUN npm run check && npm run proof:launch:engines && npm run engines:verify:docker-core
FROM dev AS sage-math
USER root
RUN apt-get update \
&& apt-get install -y --no-install-recommends sagemath \
&& rm -rf /var/lib/apt/lists/*
USER truth
ENV TRUTH_HARNESS_SAGE=sage
RUN sage --version && npm run demo:sage && npm run engines:verify:sage
CMD ["npm", "run", "engines:verify:sage"]
FROM dev AS lean-proof
USER root
RUN apt-get update \
&& apt-get install -y --no-install-recommends curl git xz-utils \
&& rm -rf /var/lib/apt/lists/*
USER truth
ENV ELAN_HOME="/home/truth/.elan" \
PATH="/home/truth/.elan/bin:${PATH}" \
TRUTH_HARNESS_LEAN=lean
RUN curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
| sh -s -- -y --default-toolchain leanprover/lean4:v4.12.0 \
&& elan toolchain install leanprover/lean4:v4.12.0 \
&& lean --version
RUN npm run proof:lean-suite && npm run engines:verify:lean
CMD ["npm", "run", "proof:lean-suite"]
FROM lean-proof AS mathlib-proof
RUN if [ ! -f docs/examples/lean-mathlib-template/lake-manifest.json ]; then \
echo "docs/examples/lean-mathlib-template/lake-manifest.json is required before building the mathlib-proof target" >&2; \
echo "Run Lake dependency resolution in a reviewed networked build step, commit the manifest, then rebuild this target." >&2; \
exit 1; \
fi \
&& cd docs/examples/lean-mathlib-template \
&& lake exe cache get \
&& lake build
RUN npm run proof:mathlib-template:check
CMD ["npm", "run", "proof:mathlib-template:check"]
FROM sage-math AS all-engines
USER root
RUN apt-get update \
&& apt-get install -y --no-install-recommends curl git xz-utils \
&& rm -rf /var/lib/apt/lists/*
USER truth
ENV ELAN_HOME="/home/truth/.elan" \
PATH="/home/truth/.elan/bin:${PATH}" \
TRUTH_HARNESS_LEAN=lean \
TRUTH_HARNESS_SAGE=sage
RUN curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
| sh -s -- -y --default-toolchain leanprover/lean4:v4.12.0 \
&& elan toolchain install leanprover/lean4:v4.12.0 \
&& lean --version
RUN npm run proof:lean-suite && npm run engines:verify:all
CMD ["npm", "run", "engines:verify:all"]