Skip to content
<awesome-gh-repos>
vic

mmhelloworld/idris-jvm

JVM bytecode back end for Idris
Source code at GitHub https://github.com/mmhelloworld/idris-jvm
mmhelloworld/idris-jvm.json
{
  "createdAt": "2016-07-17T07:06:57Z",
  "defaultBranch": "main",
  "description": "JVM bytecode back end for Idris",
  "fullName": "mmhelloworld/idris-jvm",
  "homepage": "",
  "language": "Idris",
  "name": "idris-jvm",
  "pushedAt": "2025-07-27T04:26:01Z",
  "stargazersCount": 475,
  "topics": [
    "idris",
    "java",
    "jvm"
  ],
  "updatedAt": "2025-09-24T20:57:30Z",
  "url": "https://github.com/mmhelloworld/idris-jvm"
}

Idris 2 for JVM

Section titled “Idris 2 for JVM”

Build Status

Idris 2 is a purely functional programming language with first class types. This repository provides Idris 2 compiler targeting JVM bytecode so that Idris 2 compiler and Idris 2 programs can run on the JVM.

Alt

Install

Section titled “Install”
  • Download the latest Idris 2 JVM release from releases page.
  • Extract the archive and add idris2 launcher script directory <EXTRACTED_DIRECTORY_ROOT>/exec to PATH.
  • Create an environment variable IDRIS2_PREFIX pointing to <EXTRACTED_DIRECTORY_ROOT>/env

Example

Section titled “Example”

helloworld.idr

Section titled “helloworld.idr”
    module Main


    data Tree a = Leaf
                | Node (Tree a) a (Tree a)


    inorder : Tree a -> List a
    inorder Leaf = []
    inorder (Node left a right) = inorder left ++ [a] ++ inorder right


    tree : Tree String
    tree = Node
            (Node
              (Node Leaf "3" Leaf)
              "+"
              (Node Leaf "7" Leaf))
            "/"
            (Node Leaf "2" Leaf)


    main : IO ()
    main = printLn $ inorder tree

Compile

Section titled “Compile”

idris2 helloworld.idr -o main

Run

Section titled “Run”
Terminal window
% build/exec/main
["3", "+", "7", "/", "2"]

Documentation

Section titled “Documentation”

License

Section titled “License”

This repository extends idris-lang/Idris2 repository with JVM backend. Files from idris-lang/Idris2 are covered by that repository’s license. All other files from this repository are covered by BSD-3-Clause License. See [LICENSE]!(LICENSE).