Merge pull request #79 from joshuanianji/example

Example Project

Author: joshuanianji

README.md

@@ -12,9 +12,7 @@ Idris Versions: `v0.5.1`, `v0.6.0`, `v0.7.0`, `latest` (Up to date with [Idris2/
   - [Table of Contents](#table-of-contents)
   - [Motivation](#motivation)
   - [Images](#images)
-  - [Devcontainer Demo: Wordle in Idris](#devcontainer-demo-wordle-in-idris)
-    - [Prerequisites](#prerequisites)
-    - [Opening in a Devcontainer](#opening-in-a-devcontainer)
+  - [Example Project](#example-project)
   - [Usage](#usage)
     - [Devcontainer](#devcontainer)
     - [Command Line](#command-line)
@@ -35,30 +33,16 @@ Installing Idris2 is [quite time consuming](https://idris2.readthedocs.io/en/lat
 * [idris-2-docker/ubuntu](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fubuntu) - Ubuntu 20.04
 * [idris-2-docker/debian](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fdebian) - Debian bullseye
 
-## Devcontainer Demo: Wordle in Idris
+## Example Project
 
-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).
-
-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!
-
-### Prerequisites
-
-* A working instance of [Docker](https://docs.docker.com/get-docker/)
-* [VSCode](https://code.visualstudio.com/download)
-* [Remote Development Extension Pack](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.vscode-remote-extensionpack) for VSCode
-
-### Opening in a Devcontainer
+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.
 
 ```bash
-git clone https://github.com/calebji123/WordleInIdris.git
+git clone [email protected]:joshuanianji/idris-2-docker.git
+cd idris-2-docker/example
+code .
 ```
 
-Once you clone the repo, open the folder in VSCode. There will be a prompt on the bottom right.
-
-![Reopen in Container](./docs/reopen-in-container.png)
-
-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)!
-
 ## Usage
 
 ### Devcontainer

example/.devcontainer/devcontainer.json

@@ -0,0 +1,24 @@
+// For format details, see https://aka.ms/devcontainer.json. For config options, see the
+// README at: https://github.com/devcontainers/templates/tree/main/src/debian
+{
+    "name": "Idris2 Devcontainer",
+    "image": "ghcr.io/joshuanianji/idris-2-docker/devcontainer:v0.7.0",
+    "features": {
+        "ghcr.io/devcontainers/features/common-utils:2": {}
+    },
+    "customizations": {
+        "vscode": {
+            "extensions": [
+                "bamboo.idris2-lsp"
+            ]
+        }
+    }
+    // Features to add to the dev container. More info: https://containers.dev/features.
+    // "features": {},
+    // Use 'forwardPorts' to make a list of ports inside the container available locally.
+    // "forwardPorts": [],
+    // Configure tool-specific properties.
+    // "customizations": {},
+    // Uncomment to connect as root instead. More info: https://aka.ms/dev-containers-non-root.
+    // "remoteUser": "root"
+}

example/.gitignore

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

example/README.md

@@ -0,0 +1,24 @@
+# Hello World
+
+This is a simple hello-world example using Idris 0.7, taken from the [Getting Started Guide](https://idris2.readthedocs.io/en/latest/tutorial/starting.html).
+
+To start, open the example folder in vscode and run `Reopen in Container` from the command palette.
+
+Once the container is running, you can play with Idris2!
+
+```bash
+$ idris2 hello.idr
+     ____    __     _         ___
+    /  _/___/ /____(_)____   |__ \
+    / // __  / ___/ / ___/   __/ /     Version 0.7.0
+  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
+ /___/\__,_/_/  /_/____/   /____/      Type :? for help
+
+Welcome to Idris 2.  Enjoy yourself!
+Main> :t main
+Main.main : IO ()
+Main> :c hello main
+File build/exec/hello written
+Main> :q
+Bye for now!
+```

example/hello.idr

@@ -0,0 +1,4 @@
+module Main
+
+main : IO ()
+main = putStrLn "Hello world"

example/hello.ipkg

@@ -0,0 +1,47 @@
+package hello
+-- version =
+-- authors =
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+-- langversion
+
+-- packages to add to search path
+-- depends =
+
+-- modules to install
+modules = README
+
+-- main file (i.e. file to load at REPL)
+-- main =
+
+-- name of executable
+-- executable =
+-- opts =
+-- sourcedir =
+-- builddir =
+-- outputdir =
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =