fix build.sh
This commit is contained in:
+10
-15
@@ -3,29 +3,24 @@
|
||||
# Operate in the directory where this file is located
|
||||
cd $(dirname $0)
|
||||
|
||||
# TODO: Pull prebuilt docker images from GitHub
|
||||
|
||||
# Build elan image if not already present
|
||||
docker build --pull --rm -f elan.Dockerfile -t elan:latest .
|
||||
|
||||
# Build Adam
|
||||
( rm -rf adam
|
||||
git clone https://github.com/hhu-adam/Robo adam/
|
||||
cd adam
|
||||
lake exe cache get
|
||||
lake build)
|
||||
docker rmi adam:latest || true
|
||||
docker build \
|
||||
--build-arg GAME_DIR=adam \
|
||||
--rm -f server.Dockerfile -t adam:latest .
|
||||
lake build
|
||||
docker rmi adam:latest || true
|
||||
docker build \
|
||||
--rm -f Dockerfile -t adam:latest .
|
||||
)
|
||||
|
||||
# Build NNG
|
||||
( rm -rf nng
|
||||
git clone https://github.com/hhu-adam/NNG4 nng/
|
||||
cd nng
|
||||
lake exe cache get
|
||||
lake build)
|
||||
docker rmi nng:latest || true
|
||||
docker build \
|
||||
--build-arg GAME_DIR=nng \
|
||||
--rm -f server.Dockerfile -t nng:latest .
|
||||
lake build
|
||||
docker rmi nng:latest || true
|
||||
docker build \
|
||||
--rm -f Dockerfile -t nng:latest .
|
||||
)
|
||||
|
||||
@@ -1,13 +0,0 @@
|
||||
FROM ubuntu:18.04
|
||||
|
||||
WORKDIR /
|
||||
|
||||
RUN apt-get update
|
||||
RUN apt-get upgrade -y
|
||||
RUN apt-get install -y git curl libatomic1
|
||||
|
||||
# Install elan
|
||||
RUN curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
|
||||
RUN ./elan-init -y --default-toolchain leanprover/lean4:nightly-2022-09-23
|
||||
# TODO: Read out lean version from lean-toolchain file
|
||||
ENV PATH="${PATH}:/root/.elan/bin"
|
||||
@@ -1,19 +0,0 @@
|
||||
ARG GAME_DIR
|
||||
FROM elan:latest
|
||||
|
||||
WORKDIR /
|
||||
|
||||
# Copy lean files
|
||||
COPY GameServer ./GameServer
|
||||
COPY Main.lean ./Main
|
||||
COPY lakefile.lean ./lakefile.lean
|
||||
COPY lake-manifest.json ./lake-manifest.json
|
||||
COPY lean-toolchain ./lean-toolchain
|
||||
COPY $GAME_DIR ./$GAME_DIR
|
||||
# TODO: make `adam` a build argument
|
||||
|
||||
WORKDIR /
|
||||
RUN rm -f ./build/bin/gameserver
|
||||
RUN lake build
|
||||
|
||||
WORKDIR /build/bin/
|
||||
Reference in New Issue
Block a user