File tree Expand file tree Collapse file tree 5 files changed +100
-0
lines changed Expand file tree Collapse file tree 5 files changed +100
-0
lines changed Original file line number Diff line number Diff line change
1
+ // For format details, see https://aka.ms/devcontainer.json. For config options, see the
2
+ // README at: https://github.com/devcontainers/templates/tree/main/src/debian
3
+ {
4
+ "name" : " Idris2 Devcontainer" ,
5
+ "image" : " ghcr.io/joshuanianji/idris-2-docker/devcontainer:v0.7.0" ,
6
+ "features" : {
7
+ "ghcr.io/devcontainers/features/common-utils:2" : {}
8
+ },
9
+ "customizations" : {
10
+ "vscode" : {
11
+ "extensions" : [
12
+ " bamboo.idris2-lsp"
13
+ ]
14
+ }
15
+ }
16
+ // Features to add to the dev container. More info: https://containers.dev/features.
17
+ // "features": {},
18
+ // Use 'forwardPorts' to make a list of ports inside the container available locally.
19
+ // "forwardPorts": [],
20
+ // Configure tool-specific properties.
21
+ // "customizations": {},
22
+ // Uncomment to connect as root instead. More info: https://aka.ms/dev-containers-non-root.
23
+ // "remoteUser": "root"
24
+ }
Original file line number Diff line number Diff line change
1
+ build
Original file line number Diff line number Diff line change
1
+ # Hello World
2
+
3
+ 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 ) .
4
+
5
+ To start, open the example folder in vscode and run ` Reopen in Container ` from the command palette.
6
+
7
+ Once the container is running, you can play with Idris2!
8
+
9
+ ``` bash
10
+ $ idris2 hello.idr
11
+ ____ __ _ ___
12
+ / _/___/ /____(_)____ | __ \
13
+ / // __ / ___/ / ___/ __/ / Version 0.7.0
14
+ _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
15
+ /___/\_ _,_/_/ /_/____/ /____/ Type :? for help
16
+
17
+ Welcome to Idris 2. Enjoy yourself!
18
+ Main> :t main
19
+ Main.main : IO ()
20
+ Main> :c hello main
21
+ File build/exec/hello written
22
+ Main> :q
23
+ Bye for now!
24
+ ```
Original file line number Diff line number Diff line change
1
+ module Main
2
+
3
+ main : IO ()
4
+ main = putStrLn " Hello world"
Original file line number Diff line number Diff line change
1
+ package hello
2
+ -- version =
3
+ -- authors =
4
+ -- maintainers =
5
+ -- license =
6
+ -- brief =
7
+ -- readme =
8
+ -- homepage =
9
+ -- sourceloc =
10
+ -- bugtracker =
11
+
12
+ -- the Idris2 version required (e.g. langversion >= 0.5.1)
13
+ -- langversion
14
+
15
+ -- packages to add to search path
16
+ -- depends =
17
+
18
+ -- modules to install
19
+ modules = README
20
+
21
+ -- main file (i.e. file to load at REPL)
22
+ -- main =
23
+
24
+ -- name of executable
25
+ -- executable =
26
+ -- opts =
27
+ -- sourcedir =
28
+ -- builddir =
29
+ -- outputdir =
30
+
31
+ -- script to run before building
32
+ -- prebuild =
33
+
34
+ -- script to run after building
35
+ -- postbuild =
36
+
37
+ -- script to run after building, before installing
38
+ -- preinstall =
39
+
40
+ -- script to run after installing
41
+ -- postinstall =
42
+
43
+ -- script to run before cleaning
44
+ -- preclean =
45
+
46
+ -- script to run after cleaning
47
+ -- postclean =
You can’t perform that action at this time.
0 commit comments