Skip to content

Commit 81959b8

Browse files
committed
Update README
1 parent 442e9d0 commit 81959b8

File tree

1 file changed

+6
-22
lines changed

1 file changed

+6
-22
lines changed

README.md

Lines changed: 6 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,7 @@ Idris Versions: `v0.5.1`, `v0.6.0`, `v0.7.0`, `latest` (Up to date with [Idris2/
1212
- [Table of Contents](#table-of-contents)
1313
- [Motivation](#motivation)
1414
- [Images](#images)
15-
- [Devcontainer Demo: Wordle in Idris](#devcontainer-demo-wordle-in-idris)
16-
- [Prerequisites](#prerequisites)
17-
- [Opening in a Devcontainer](#opening-in-a-devcontainer)
15+
- [Example Project](#example-project)
1816
- [Usage](#usage)
1917
- [Devcontainer](#devcontainer)
2018
- [Command Line](#command-line)
@@ -35,30 +33,16 @@ Installing Idris2 is [quite time consuming](https://idris2.readthedocs.io/en/lat
3533
* [idris-2-docker/ubuntu](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fubuntu) - Ubuntu 20.04
3634
* [idris-2-docker/debian](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fdebian) - Debian bullseye
3735

38-
## Devcontainer Demo: Wordle in Idris
36+
## Example Project
3937

40-
Devcontainers use a Docker container as a full-featured development environment, making it super simple to get started with Idris2. For more information, check out [Microsoft's documentation](https://code.visualstudio.com/docs/remote/containers).
41-
42-
If you want to try out a quick ready-to-use project, take a look at [calebji123/WordleInIdris](https://github.com/calebji123/WordleInIdris). The devcontainer files there are set up and it's super fun to play around with!
43-
44-
### Prerequisites
45-
46-
* A working instance of [Docker](https://docs.docker.com/get-docker/)
47-
* [VSCode](https://code.visualstudio.com/download)
48-
* [Remote Development Extension Pack](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.vscode-remote-extensionpack) for VSCode
49-
50-
### Opening in a Devcontainer
38+
An example Hello World project taken from the [Getting Started Guide](https://idris2.readthedocs.io/en/latest/tutorial/starting.html) can be found in [example](./example). It uses Idris 0.7.0. To start, clone this repo and open the example folder (not the root!) in VSCode.
5139

5240
```bash
53-
git clone https://github.com/calebji123/WordleInIdris.git
41+
git clone [email protected]:joshuanianji/idris-2-docker.git
42+
cd idris-2-docker/example
43+
code .
5444
```
5545

56-
Once you clone the repo, open the folder in VSCode. There will be a prompt on the bottom right.
57-
58-
![Reopen in Container](./docs/reopen-in-container.png)
59-
60-
Click "Reopen in Container" and it will download the image and open the project in a devcontainer. You'll be able to [run the project right away](https://github.com/calebji123/WordleInIdris#how-to-run-it)!
61-
6246
## Usage
6347

6448
### Devcontainer

0 commit comments

Comments
 (0)