init

Author: bennn

.docker/gitpod/Dockerfile

@@ -0,0 +1,29 @@
+# Adapted from Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+
+FROM ubuntu:jammy
+
+USER root
+
+RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-pip racket default-jdk default-jre -y && apt-get clean
+
+RUN raco pkg install --auto forge froglet
+
+RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
+    # passwordless sudo for users in the 'sudo' group
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.gitignore

@@ -0,0 +1 @@
+/build

.gitpod.yml

@@ -0,0 +1,3 @@
+image:
+  file: .docker/gitpod/Dockerfile
+

.vscode/settings.json

@@ -0,0 +1,8 @@
+{ 
+    "editor.minimap.enabled": false,
+    "editor.insertSpaces": true,
+    "editor.tabSize": 2,
+    "editor.semanticTokenColorCustomizations": {
+        "[Gitpod Light]": {"rules": {"other": "#335f66", "variable": "#7f197f"}}
+    }
+}

README.md

@@ -0,0 +1,22 @@
+# PBT GitPod
+
+## Setup
+
+0. Sign up for a GitHub account
+1. Go to <https://gitpod.io/#https://github.com/utahplt/forge-gitpod>
+    * Log in with GitHub
+2. Wait for VSCode to appear
+3. Go to <https://gitpod.io>, find the new workspace, click the `...` on the
+   right, and pin this workspace.
+    * If you don't pin it, GitPod may throw it away after N days!!
+
+## Usage
+
+Write code in VSCode like normal.
+
+Run code from the terminal:
+
+```
+racket FILE.frg
+```
+