rework build process
parent
b8cea5b0f4
commit
732754c9fc
File diff suppressed because it is too large
Load Diff
@ -1,2 +0,0 @@
|
||||
build
|
||||
node_modules
|
@ -1,25 +0,0 @@
|
||||
FROM ubuntu:18.04
|
||||
|
||||
WORKDIR /
|
||||
|
||||
RUN apt-get update
|
||||
RUN apt-get upgrade -y
|
||||
RUN apt-get install -y git curl
|
||||
|
||||
# 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:stable
|
||||
ENV PATH="${PATH}:/root/.elan/bin"
|
||||
|
||||
# clone repos
|
||||
RUN git clone https://github.com/hhu-adam/lean4-game-server.git game-server
|
||||
RUN cd game-server && git checkout gvisor
|
||||
RUN cd game-server && lake build
|
||||
|
||||
RUN git clone https://github.com/hhu-adam/NNG4.git
|
||||
|
||||
WORKDIR /NNG4
|
||||
|
||||
RUN git checkout gvisor
|
||||
RUN lake build
|
||||
CMD ["./build/bin/nng"]
|
@ -0,0 +1,12 @@
|
||||
#!/usr/bin/env sh
|
||||
|
||||
# Operate in the directory where this file is located
|
||||
cd $(dirname $0)
|
||||
|
||||
# Build elan image if not already present
|
||||
docker build --pull --rm -f elan.Dockerfile -t elan:latest .
|
||||
|
||||
(cd leanserver && lake build)
|
||||
(cd testgame && lake build)
|
||||
docker rmi testgame:latest || true
|
||||
docker build --rm -f server.Dockerfile -t testgame:latest .
|
@ -0,0 +1,13 @@
|
||||
FROM ubuntu:18.04
|
||||
|
||||
WORKDIR /
|
||||
|
||||
RUN apt-get update
|
||||
RUN apt-get upgrade -y
|
||||
RUN apt-get install -y git curl
|
||||
|
||||
# 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"
|
@ -0,0 +1,11 @@
|
||||
FROM elan:latest
|
||||
|
||||
WORKDIR /
|
||||
|
||||
# Copy lean files
|
||||
COPY leanserver ./leanserver
|
||||
COPY testgame ./testgame
|
||||
# TODO: make `testgame` a build argument
|
||||
|
||||
WORKDIR /leanserver
|
||||
CMD ["./build/bin/gameserver", "TestGame", "../testgame"]
|
@ -0,0 +1 @@
|
||||
build
|
@ -1,7 +1,7 @@
|
||||
import Lake
|
||||
open Lake DSL
|
||||
|
||||
require GameServer from ".."/"server"
|
||||
require GameServer from ".."/"leanserver"
|
||||
|
||||
package TestGame
|
||||
|
Loading…
Reference in New Issue