Add devcontainer support

.devcontainer/.emacs

@@ -0,0 +1,6 @@
+;; auto-load agda-mode for .agda and .lagda.md
+(setq auto-mode-alist
+   (append
+     '(("\\.agda\\'" . agda2-mode)
+       ("\\.lagda.md\\'" . agda2-mode))
+     auto-mode-alist))

.devcontainer/DockerFile

@@ -0,0 +1,3 @@
+FROM haskell:9.8
+RUN apt update && apt install emacs -y
+RUN cabal update && cabal install Agda-2.6.3

.devcontainer/devcontainer.json

@@ -0,0 +1,16 @@
+{
+    "name": "Agda",
+    "build" : {
+        "dockerfile": "DockerFile"
+    },
+    "workspaceMount": "source=${localWorkspaceFolder},target=/root/plfa,type=bind",
+    "workspaceFolder": "/root/plfa",
+    "postCreateCommand": "bash ./.devcontainer/post-create.sh",
+    "customizations": {
+        "vscode": {
+            "extensions": [
+                "banacorn.agda-mode"
+            ]
+        }
+    }
+}

.devcontainer/post-create.sh

@@ -0,0 +1,9 @@
+cd ~/plfa && git submodule update --init --recursive
+
+mkdir  ~/.agda
+cp ~/plfa/data/dotagda/* ~/.agda
+
+agda-mode setup
+agda-mode compile
+
+cat ~/plfa/.devcontainer/.emacs >> ~/.emacs

README.md

@@ -26,6 +26,15 @@ PLFA is tested against specific versions of Agda and the standard library, which
 
 There are several versions of Agda and its standard library online. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out of date. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. Therefore, it’s important to have the specific versions of Agda and the standard library shown above.
 
+### In Dev Containers
+With the help of [Dev Containers and Codespaces](https://docs.github.com/en/codespaces/setting-up-your-project-for-codespaces/adding-a-dev-container-configuration/introduction-to-dev-containers), you can build an environment pre-installed with the Agda toolchain required for the tutorial without the need to execute installation commands.
+
+Visit https://github.com/plfa/plfa.github.io in your browser, press the dot (`.`) key on the webpage, it will take you to the online VSCode editor. From there, you can create a codespace. The build process takes approximately 10 minutes, and the built codespace will include: [Agda](#install-agda), [Emacs with agda-mode](#using-agda-mode-in-emacs), [VSCode extension for agda](#visual-studio-code). Then you can interact with the code!
+
+Apart from using the web version of VSCode, you can also connect to the codespace from your local VSCode. Here is the [instruction](https://docs.github.com/en/codespaces/developing-in-a-codespace/using-github-codespaces-in-visual-studio-code).
+
+Optionally, you can run the devcontainer on your local machine. Git clone the [repo](https://github.com/plfa/plfa.github.io) to your computer, open it with VSCode, and then the editor will prompt you to reopen in container. For more details, please refer to the [documentation](https://code.visualstudio.com/docs/devcontainers/tutorial).
+
 ### On macOS: Install the XCode Command Line Tools
 
 On macOS, you’ll need to install [The XCode Command Line Tools][xcode]. For most versions of macOS, you can install these by running the following command: