Announcing Idris 2 Bootstrap Compiler on the JVM with a JVM Backend

[mmhell...@gmail.com]

Hello all,

I am excited to announce that Idris 2 bootstrap compiler can now run on the JVM along with a JVM backend. Here is a REPL session:

$ idris2
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.1.1-786152de1
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help

[BOOTSTRAP VERSION: No longer developed, except as a bootstrapping step.]
Welcome to Idris 2 on the JVM (Private Build OpenJDK 64-Bit Server VM, 1.8.0_275). Enjoy yourself!
Main> "hello world"
"hello world"
Main> take 10 [25..]
[25, 26, 27, 28, 29, 30, 31, 32, 33, 34]
Main> :t map
Prelude.map : Functor f => (a -> b) -> f a -> f b
Main> :exec printLn "Hello Idris 2 on the JVM - this is printed from executing JVM bytecode from memory"
"Hello Idris 2 on the JVM - this is printed from executing JVM bytecode from memory"
Main>

Since the compiler itself runs on the JVM, the last `:exec` command above can directly interpret the generated bytecode on the compiler JVM, and the generated bytecode is loaded from memory without any file system footprint.

To try it out

Prerequisite: Java 8 or above

• Extract the zip from here
• Add `idris2-boot-jvm/bin` from extracted directory to `PATH`
• Run `idris2`. That's all!

Features

• Eliminate tail recursion using JVM's GOTO
• Trampoline non-self tail calls
• Support file, directory, array, IORef and buffer primitives.
• Analyse function dependencies to generate bytecode for only used functions from `main`
• Limited type inference on Idris IR to avoid boxing and typecasting in the generated bytecode
• Static and instance Java FFI method calls.
• Debug information (Idris source file and line numbers) in the bytecode from Idris IR

Currently the goal for this bootstrap compiler is to be able to compile current Idris 2 so the items here could definitely be improved a lot and other features may be added to support the absolute minimum for building Idris 2. Next step would be to use this bootstrap version to compile current Idris 2 and then porting the JVM backend from here which is on Idris 1 to Idris 2 so there are some interesting things ahead to work on. Meanwhile, if anyone gets a chance to use this boostrap JVM version, please share any feedback or any issues here that can help while I try to compile mainstream Idris 2 for the JVM. I have added more details about the features here. 

- Marimuthu Madasamy

[alru...@gmail.com]

Impressive stuff. Has there been any progress on getting the Idris2 frontend working on top of this? I got the Idris2-0.2.1 release compiling with idris-boot-jvm, but there are no Idris2 JVM primitives implemented (if I'm not missing anything), right?

[mmhell...@gmail.com]

Hi,

I had been working on compiling Idris 2 (starting with 0.2.1 version) with the initial JVM bootstrap version and pushing the changes here https://github.com/mmhelloworld/Idris2-boot. Recent status is that when compiling large codebase like Idris 2, some functions generate huge case trees which exceed JVM method size limit so I was working on optimizing that. I couldn't spend much time on it recently but I will be picking it up again soon in the next few days and hopefully soon we should be able to have Idris 2 0.2.1 running on the JVM.

[Stefan Höck]

Thanks for the great work! I'm really looking forward to Idris2 on the
JVM.

Best regards

Stefan

> >> - Extract the zip from here
> >> <https://github.com/mmhelloworld/Idris2-boot/releases/tag/v0.2.0>
> >> - Add `idris2-boot-jvm/bin` from extracted directory to `PATH`
> >> - Run `idris2`. That's all!
> >>
> >>
> >> Features
> >>
> >> - Eliminate tail recursion using JVM's GOTO
> >> - Trampoline non-self tail calls
> >> - Support file, directory, array, IORef and buffer primitives.
> >> - Analyse function dependencies to generate bytecode for only used
> >> functions from `main`
> >> - Limited type inference on Idris IR to avoid boxing and typecasting
> >> in the generated bytecode
> >> - Static and instance Java FFI method calls.
> >> - Debug information (Idris source file and line numbers) in the

> >> bytecode from Idris IR
> >>
> >>
> >> Currently the goal for this bootstrap compiler is to be able to compile

> >> current Idris 2 <https://github.com/idris-lang/Idris2> so the items here

> >> could definitely be improved a lot and other features may be added to
> >> support the absolute minimum for building Idris 2. Next step would be to
> >> use this bootstrap version to compile current Idris 2

> >> <https://github.com/idris-lang/Idris2> and then porting the JVM backend

> >> from here which is on Idris 1 to Idris 2 so there are some interesting
> >> things ahead to work on. Meanwhile, if anyone gets a chance to use this
> >> boostrap JVM version, please share any feedback or any issues here

> >> <https://github.com/mmhelloworld/idris-jvm/discussions> that can help

> >> while I try to compile mainstream Idris 2 for the JVM. I have added more
> >> details about the features here

> >> <http://mmhelloworld.github.io/blog/2020/12/30/idris-2-bootstrap-compiler-on-the-jvm-with-a-jvm-backend/>
> >> .
> >>
> >> - Marimuthu Madasamy
> >>
> >
>
> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/3d60e2b5-30fb-4431-b3ca-e335e500bdfcn%40googlegroups.com.