Use idris-jvm in the repl?

mpdairy commented 5 years ago

Is it possible to use idris-jvm in the repl with an IDE? I'd like to do interactive development with other jvm libs in my emacs repl.

mmhelloworld commented 5 years ago

Currently in Idris REPL, we can only execute native code but we can still use the REPL with JVM types and functions. I am working on compiling Blodwen to JVM so once it is ready, we should be able to execute JVM code as well with that.

PhilAndrew commented 4 years ago

When I am in the Atom editor and I CTRL-ALT-R to type check then it sas

didn't load (my path)/src/main/idris/Main.idr

Can't find import IdrisJvm/FFI

How to fix this so I can do interactive editing?

mmhelloworld commented 4 years ago

You need to have an ipkg file like this:

module helloworld

pkgs = idrisjvmffi

modules = Main

PhilAndrew commented 4 years ago

Ahh thanks, what I had to do was open that folder with the ipkg in the root of the project, before I was opening a parent folder and drilling down to the sub-folder which contained the ipjkg which was wrong.

mmhelloworld commented 2 years ago

Now that we have Idris 2 on the JVM, compiler and REPL can run on the JVM. Here is a small example.

module Main

import System.FFI

namespace LocalDateTime
    data LocalDateTime : Type where [external]

    %foreign "jvm:now(java/lang/Object java/time/LocalDateTime),java/time/LocalDateTime"
    prim_now : PrimIO LocalDateTime

    %foreign jvm' "java/time/LocalDateTime" ".toString" "java/time/LocalDateTime" "String"
    prim_toString : LocalDateTime -> PrimIO String

    export
    now : IO LocalDateTime
    now = primIO prim_now

    export
    toString : LocalDateTime -> IO String
    toString = primIO . prim_toString

main : IO ()
main = do
    currentDateTime <- LocalDateTime.now
    printLn !(toString currentDateTime)

$ rlwrap idris2 Main.idr
     ____    __     _         ___                                           
    /  _/___/ /____(_)____   |__ \                                          
    / // __  / ___/ / ___/   __/ /     Version 0.5.1-98e399195
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
 /___/\__,_/_/  /_/____/   /____/      Type :? for help                     

Welcome to Idris 2.  Enjoy yourself!
Main> :exec main
"2022-01-02T22:27:09.945"
Main>

mmhelloworld / idris-jvm

Use idris-jvm in the repl? #95