You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+16-31Lines changed: 16 additions & 31 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -20,8 +20,8 @@ Idris Versions: `v0.5.1`, `v0.6.0`, `latest` (Up to date with [Idris2/main](http
20
20
-[Command Line](#command-line)
21
21
-[Base Image](#base-image)
22
22
-[Running Locally](#running-locally)
23
-
-[Build Latest (or a Specific Commit)](#build-latest-or-a-specific-commit)
24
-
-[Build From a Tagged Release](#build-from-a-tagged-release)
23
+
-[Build Latest](#build-latest)
24
+
-[Build From a Tagged Release/SHA commit](#build-from-a-tagged-releasesha-commit)
25
25
-[Credit](#credit)
26
26
27
27
## Motivation
@@ -30,7 +30,8 @@ Installing Idris2 is [quite time consuming](https://idris2.readthedocs.io/en/lat
30
30
31
31
## Images
32
32
33
-
*[idris-2-docker/devcontainer](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fdevcontainer) - Debian bullseye built off of [Microsoft's Devcontainer Base image](https://github.com/microsoft/vscode-dev-containers/tree/main/containers/debian)
33
+
*[idris-2-docker/base](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fbase) - Base image with Idris2 installed from source.
34
+
*[idris-2-docker/devcontainer](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fdevcontainer) - Includes [Idris2 LSP](https://github.com/idris-community/idris2-lsp)
@@ -65,7 +66,7 @@ Click "Reopen in Container" and it will download the image and open the project
65
66
Add devcontainers to your own project by copying the following contents to `Dockerfile` in the root of your project:
66
67
67
68
```dockerfile
68
-
FROM ghcr.io/joshuanianji/idris-2-docker/devcontainer:v0.5.1
69
+
FROM ghcr.io/joshuanianji/idris-2-docker/devcontainer:v0.7.0
69
70
```
70
71
71
72
Then, using Microsoft's Remote SSH tools, click "Reopen in container" and choose that Dockerfile.
@@ -94,40 +95,24 @@ FROM ghcr.io/joshuanianji/idris-2-docker/debian:v0.5.1
94
95
95
96
## Running Locally
96
97
97
-
To run the images locally, I recommend opening the workspace in the Devcontainer to provide a fully-featured development environment.
98
+
To run the images locally, I recommend opening the workspace in the Devcontainer to provide a fully-featured development environment. I made a `scripts/build-image.py` which can build the base, debian, ubuntu or devcontainer from an idris version or a SHA commit.
98
99
99
-
### Build Latest (or a Specific Commit)
100
+
### Build Latest
101
+
102
+
This is the default behaviour when running the script.
100
103
101
104
```bash
102
-
export IDRIS_VERSION=latest
103
-
# get latest commit - here we're using the github api and jq
0 commit comments