-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDockerfile
65 lines (49 loc) · 2.4 KB
/
Dockerfile
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
####################################################################################################
# Build Agda
####################################################################################################
ARG GHC_VERSION=9.4.7
FROM fossa/haskell-static-alpine:ghc-${GHC_VERSION} AS agda
WORKDIR /build/agda
# Agda 2.6.4.3
ARG AGDA_VERSION=714c7d2c76c5ffda3180e95c28669259f0dc5b5c
RUN \
git init && \
git remote add origin https://github.com/agda/agda.git && \
git fetch --depth 1 origin "${AGDA_VERSION}" && \
git checkout FETCH_HEAD
# We build Agda and place it in /dist along with its data files.
# We explicitly use v1-install because v2-install does not support --datadir and --bindir
# to relocate executables and data files yet.
RUN \
mkdir -p /dist && \
cabal update && \
cabal v2-install alex happy-2.0.2 && \
cabal v1-install --bindir=/dist --datadir=/dist --datasubdir=/dist/data --enable-executable-static
####################################################################################################
# Type-check Agda files
####################################################################################################
FROM alpine AS hottagda
COPY ["HoTT-Agda", "/build/HoTT-Agda"]
COPY ["Colimit-code", "/build/Colimit-code"]
FROM alpine
COPY --from=agda /dist /dist
COPY --from=hottagda /build /build
COPY ["Pullback-stability", "/build/Pullback-stability"]
COPY agda-html.sh /
RUN echo "/build/HoTT-Agda/hott-core.agda-lib" >> /dist/libraries
RUN echo "/build/HoTT-Agda/hott-theorems.agda-lib" >> /dist/libraries
RUN echo "/build/Colimit-code/cos-colim.agda-lib" >> /dist/libraries
RUN echo "/build/Pullback-stability/stab.agda-lib" >> /dist/libraries
WORKDIR /build/HoTT-Agda
RUN /dist/agda --library-file=/dist/libraries ./theorems/homotopy/SuspAdjointLoop.agda
WORKDIR /build/Colimit-code
RUN /dist/agda --library-file=/dist/libraries ./Trunc-Cos/TruncAdj.agda
RUN /dist/agda --library-file=/dist/libraries ./Main-Theorem/CosColim-Adjunction.agda
WORKDIR /build/Pullback-stability
RUN /dist/agda --library-file=/dist/libraries ./Stability.agda
####################################################################################################
# Execute shell script to create html files for colimit code
####################################################################################################
WORKDIR /build
RUN ["chmod", "+x", "/agda-html.sh"]
CMD ["sh", "/agda-html.sh"]