From 404327adf1636ec99dd321e2ac4254e840628a63 Mon Sep 17 00:00:00 2001 From: weihongliang233 <52309635+weihongliang233@users.noreply.github.com> Date: Tue, 5 Mar 2024 05:18:21 +0000 Subject: [PATCH 1/4] add devcontainer support --- .devcontainer/.emacs | 6 ++++++ .devcontainer/DockerFile | 3 +++ .devcontainer/devcontainer.json | 16 ++++++++++++++++ .devcontainer/post-create.sh | 9 +++++++++ 4 files changed, 34 insertions(+) create mode 100644 .devcontainer/.emacs create mode 100644 .devcontainer/DockerFile create mode 100644 .devcontainer/devcontainer.json create mode 100644 .devcontainer/post-create.sh diff --git a/.devcontainer/.emacs b/.devcontainer/.emacs new file mode 100644 index 000000000..77c5acfb1 --- /dev/null +++ b/.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)) diff --git a/.devcontainer/DockerFile b/.devcontainer/DockerFile new file mode 100644 index 000000000..e694c7eac --- /dev/null +++ b/.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 \ No newline at end of file diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json new file mode 100644 index 000000000..572c50a20 --- /dev/null +++ b/.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" + ] + } + } +} \ No newline at end of file diff --git a/.devcontainer/post-create.sh b/.devcontainer/post-create.sh new file mode 100644 index 000000000..8a0b16583 --- /dev/null +++ b/.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 \ No newline at end of file From 8486b099e1792a5606fcfae27f611659d9f07d44 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Tue, 5 Mar 2024 05:56:26 +0000 Subject: [PATCH 2/4] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- .devcontainer/DockerFile | 2 +- .devcontainer/devcontainer.json | 2 +- .devcontainer/post-create.sh | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.devcontainer/DockerFile b/.devcontainer/DockerFile index e694c7eac..e09b5d5e9 100644 --- a/.devcontainer/DockerFile +++ b/.devcontainer/DockerFile @@ -1,3 +1,3 @@ FROM haskell:9.8 RUN apt update && apt install emacs -y -RUN cabal update && cabal install Agda-2.6.3 \ No newline at end of file +RUN cabal update && cabal install Agda-2.6.3 diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 572c50a20..23437d938 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -13,4 +13,4 @@ ] } } -} \ No newline at end of file +} diff --git a/.devcontainer/post-create.sh b/.devcontainer/post-create.sh index 8a0b16583..aee842f3a 100644 --- a/.devcontainer/post-create.sh +++ b/.devcontainer/post-create.sh @@ -6,4 +6,4 @@ cp ~/plfa/data/dotagda/* ~/.agda agda-mode setup agda-mode compile -cat ~/plfa/.devcontainer/.emacs >> ~/.emacs \ No newline at end of file +cat ~/plfa/.devcontainer/.emacs >> ~/.emacs From 7e099368d97544318c3c6c88faf099c2914a63e7 Mon Sep 17 00:00:00 2001 From: weihongliang233 <52309635+weihongliang233@users.noreply.github.com> Date: Thu, 7 Mar 2024 07:49:40 +0000 Subject: [PATCH 3/4] update README --- README.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/README.md b/README.md index b283de90a..46fbfb4bf 100644 --- a/README.md +++ b/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: From 124af450336e70f799b0523fa1cf0a3e68cf973d Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Thu, 7 Mar 2024 07:49:56 +0000 Subject: [PATCH 4/4] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 46fbfb4bf..2582d7b2c 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ Visit https://github.com/plfa/plfa.github.io in your browser, press the dot (`.` 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: