Skip to content

Commit 2ad12b9

Browse files
kisonecatkisonecat
authored
Initial commit
0 parents  commit 2ad12b9

36 files changed

+1016
-0
lines changed

‎.devcontainer/Dockerfile‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
FROM node:20
2+
3+
WORKDIR /
4+
5+
COPY ./lean-toolchain /lean-toolchain
6+
7+
USER node
8+
9+
WORKDIR /home/node
10+
11+
RUN export LEAN_VERSION="$(cat /lean-toolchain | grep -oE '[^:]+$')" && git clone --depth 1 --branch $LEAN_VERSION https://github.com/leanprover-community/lean4game.git
12+
13+
WORKDIR /
14+
15+
USER root
16+
17+
ENV ELAN_HOME=/usr/local/elan \
18+
PATH=/usr/local/elan/bin:$PATH
19+
20+
SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]
21+
22+
RUN export LEAN_VERSION="$(cat /lean-toolchain)" && \
23+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path --default-toolchain $LEAN_VERSION; \
24+
chmod -R a+w $ELAN_HOME; \
25+
elan --version; \
26+
lean --version; \
27+
leanc --version; \
28+
lake --version;

‎.devcontainer/devcontainer.json‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
{
2+
"dockerComposeFile": "./docker-compose.yml",
3+
"service": "game",
4+
"workspaceFolder": "/home/node/game",
5+
"forwardPorts": [3000],
6+
// These settings make sure that the created files (lake-packages etc.) are owned
7+
// by the user and not `root`.
8+
// see also https://containers.dev/implementors/json_reference/
9+
// and https://code.visualstudio.com/remote/advancedcontainers/add-nonroot-user
10+
"remoteUser": "node",
11+
"updateRemoteUserUID": true,
12+
// I don't know why I need this, but I did...
13+
"overrideCommand": true,
14+
"onCreateCommand": {
15+
"npm_install": "(cd ~/lean4game && npm install) || echo \"ERROR: `cd ~/lean4game && npm install` failed\", try running it manually in your dev-container!",
16+
"lake_build": "(cd ~/game && lake update -R && lake build) || echo \"ERROR: `cd ~/game && lake update -R && lake exe cache get && lake build` failed!, try running it manually in your dev-container!\""
17+
},
18+
"postStartCommand": "(cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start) || echo \"ERROR: Did not start game server! See if you have warnings above, then try to start it manually using `cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start`!\"",
19+
"customizations": {
20+
"vscode": {
21+
"settings": {
22+
"remote.autoForwardPorts": false
23+
},
24+
"extensions": [
25+
"leanprover.lean4"
26+
]
27+
},
28+
"codespaces": {
29+
"openFiles": ["Game.lean"]
30+
}
31+
}
32+
}

‎.devcontainer/docker-compose.yml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
version: "3.9"
2+
3+
services:
4+
game:
5+
build:
6+
context: ..
7+
dockerfile: .devcontainer/Dockerfile
8+
volumes:
9+
- ..:/home/node/game
10+
ports:
11+
- "3000:3000"

‎.docker/gitpod/Dockerfile‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
2+
3+
# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
4+
# so we just install everything in one go
5+
FROM ubuntu:22.04
6+
7+
USER root
8+
9+
RUN apt-get update && apt-get --assume-yes install sudo git curl git bash-completion python3 -y && apt-get clean
10+
11+
RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
12+
# passwordless sudo for users in the 'sudo' group
13+
&& sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
14+
USER gitpod
15+
WORKDIR /home/gitpod
16+
17+
SHELL ["/bin/bash", "-c"]
18+
19+
# gitpod bash prompt
20+
RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
21+
22+
# install elan
23+
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
24+
25+
# install whichever toolchain mathlib is currently using
26+
RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
27+
28+
ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:${PATH}"
29+
30+
# fix the infoview when the container is used on gitpod:
31+
ENV VSCODE_API_VERSION="1.50.0"
32+
33+
# ssh to github once to bypass the unknown fingerprint warning
34+
RUN ssh -o StrictHostKeyChecking=no github.com || true
35+
36+
# run sudo once to suppress usage info
37+
RUN sudo echo finished

‎.editorconfig‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
root = true
2+
3+
[*]
4+
indent_style = space
5+
indent_size = 2
6+
charset = utf-8
7+
end_of_line = lf
8+
insert_final_newline = true
9+
trim_trailing_whitespace = true
10+
11+
[*.lean]
12+
max_line_length = 100

‎.github/workflows/build.yml‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
name: Build
2+
run-name: Build the game and save artifact
3+
on:
4+
workflow_dispatch:
5+
push:
6+
branches: [ "main" ]
7+
jobs:
8+
build:
9+
runs-on: ubuntu-latest
10+
steps:
11+
12+
- name: install elan
13+
run: |
14+
set -o pipefail
15+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
16+
./elan-init -y --default-toolchain none
17+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
18+
19+
- uses: actions/checkout@v4
20+
21+
- name: print lean and lake versions
22+
run: |
23+
lean --version
24+
lake --version
25+
26+
# Note: this would also happen in the lake post-update-hook
27+
- name: get mathlib cache
28+
continue-on-error: true
29+
run: |
30+
lake exe cache clean
31+
# We've been seeing many failures at this step recently because of network errors.
32+
# As a band-aid, we try twice.
33+
# The 'sleep 1' is small pause to let the network recover.
34+
lake exe cache get || (sleep 1; lake exe cache get)
35+
36+
- name: create timestamp file
37+
run: touch tmp_timestamp
38+
39+
# Note: this would also happen in the lake post-update-hook
40+
- name: build gameserver executable
41+
run: env LEAN_ABORT_ON_PANIC=1 lake build gameserver
42+
43+
- name: building game
44+
run: env LEAN_ABORT_ON_PANIC=1 lake build
45+
46+
- name: delete unused mathlib cache
47+
continue-on-error: true
48+
run: find . -type d \( -name "*/.git" \) -delete -print && find ./.lake/ -type f \( -name "*.c" -o -name "*.hash" -o -name "*.trace" \) -delete -print && find ./.lake/ -type f \( -name "*.olean" \) \! -neweraa ./tmp_timestamp -delete -print
49+
50+
- name: delete timestamp file
51+
run: rm ./tmp_timestamp
52+
53+
- name: compress built game
54+
#run: tar -czvf ../game.tar.gz .
55+
run: zip game.zip * .lake/ .i18n/ -r
56+
57+
- name: upload compressed game folder
58+
uses: actions/upload-artifact@v4
59+
with:
60+
name: build-for-server-import
61+
path: |
62+
game.zip
63+
64+
- name: What next?
65+
run: echo "To export the game to the Game Server, open https://adam.math.hhu.de/import/trigger/${GITHUB_REPOSITORY,,} \n Afterwards, you can play the game at https://adam.math.hhu.de/#/g/${GITHUB_REPOSITORY,,}"

‎.github/workflows/build_non_main.yml‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
name: Build non-main branch
2+
run-name: Build non-main branch
3+
on:
4+
workflow_dispatch:
5+
push:
6+
branches-ignore:
7+
- 'main'
8+
jobs:
9+
build:
10+
runs-on: ubuntu-latest
11+
steps:
12+
13+
- name: install elan
14+
run: |
15+
set -o pipefail
16+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
17+
./elan-init -y --default-toolchain none
18+
echo "$HOME/.elan/bin" >> $GITHUB_PATH
19+
20+
- uses: actions/checkout@v4
21+
22+
- name: print lean and lake versions
23+
run: |
24+
lean --version
25+
lake --version
26+
27+
- name: get mathlib cache
28+
continue-on-error: true
29+
run: |
30+
lake exe cache clean
31+
# We've been seeing many failures at this step recently because of network errors.
32+
# As a band-aid, we try twice.
33+
# The 'sleep 1' is small pause to let the network recover.
34+
lake exe cache get || (sleep 1; lake exe cache get)
35+
36+
- name: building game
37+
run: env LEAN_ABORT_ON_PANIC=1 lake build

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
build/
2+
lake-packages/
3+
.lake/
4+
**/.DS_Store
5+
.i18n/**/*.mo

‎.gitpod.yml‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
image:
2+
file: .docker/gitpod/Dockerfile
3+
4+
vscode:
5+
extensions:
6+
- leanprover.lean4
7+
8+
tasks:
9+
- init: |
10+
lake exe cache get
11+
- command: |
12+
sudo apt-get --assume-yes install gcc

‎.i18n/config.json‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
{
2+
"sourceLang": "en",
3+
"translationContactEmail": ""
4+
}

0 commit comments

Comments
 (0)