Compiling Blodwen
Closed this issue · 16 comments
Hi @mmhelloworld,
you probably already have seen edwinb's Blodwen repo which is a potential candidate for Idris 2.
The interesting thing is that the Blodwen compiler is written in Idris, so that might allow one to compile it to the JVM using your project.
Blodwen uses some functions that were added only in 1.3.1, so I'm wondering if you have already considered updating to that version?
If I find the time, I'll tinker a little bit with it myself, but it'll take some time to get familiar with the code base.
Hi,
Thank you for checking on this. I have been trying to build Blodwen as well with idris-jvm for the past few weeks and I have been getting some compilation errors. I tried few days ago so I already have idris-jvm compiled with Idris 1.3.1. I will publish a release either today or tomorrow.
Thanks for the release!
Is there currently a way to check if all FFI functions from the Idris standard lib are implemented?
Blodwen uses a currentDir method that was introduced in 1.3.1 (idris-lang/Idris-dev@d026c4e) so that would need to be implemented in idris-jvm as well, potentially also others.
Should be a low hanging fruit, I could give it a try next week 😃
Except for searching the source, there is no other way currently to check for JVM FFI functions. As you noticed, we need to add JVM FFI functions for Blodwen. I have been trying to do that but Blodwen for me currently doesn't even compile and fails with errors like below. It would be great if we could get past these errors and compile Blodwen with idris-jvm.
./Core/Typecheck.idr:23:9:
|
23 | chk : Env Term vars -> Raw -> Either (Error annot) (Term vars, Term vars)
| ^
When checking type of Core.Typecheck.chk:
Can't disambiguate name: FFI_C.Raw, Language.Reflection.Raw, Core.TT.Raw
Can you explain what you did to build Blodwen with idris-jvm? Did you modify the makefile, the individual ipkg files or something completely different?
I added --portable-codegen jvm to both the Makefile and the opts in the ipkg files and I'm getting the following error
make
idris --build ttimp.ipkg --portable-codegen jvm
Entering directory `./src'
Type checking ./Text/Token.idr
Type checking ./Text/Quantity.idr
Type checking ./Control/Delayed.idr
Type checking ./Data/Bool/Extra.idr
Type checking ./Text/Lexer/Core.idr
Type checking ./Text/Lexer.idr
Type checking ./Parser/Lexer.idr
Type checking ./Text/Parser/Core.idr
Type checking ./Text/Parser.idr
Type checking ./Core/Name.idr
Type checking ./Data/CMap.idr
Type checking ./Data/CSet.idr
Type checking ./Core/TT.idr
Type checking ./Parser/Support.idr
Type checking ./Data/StringMap.idr
Type checking ./Core/CaseTree.idr
Type checking ./Core/Core.idr
Type checking ./Utils/Binary.idr
Type checking ./Core/CompileExpr.idr
Type checking ./Core/TTC.idr
Type checking ./Core/Options.idr
Type checking ./Core/Hash.idr
Type checking ./Core/Context.idr
Type checking ./Core/Primitives.idr
Type checking ./Core/Normalise.idr
Type checking ./Core/UnifyState.idr
Type checking ./Core/Binary.idr
Type checking ./TTImp/TTImp.idr
Type checking ./Core/Typecheck.idr
Type checking ./Core/CaseBuilder.idr
Type checking ./Core/RawContext.idr
Type checking ./Parser/RawImp.idr
Type checking ./Parser/REPL.idr
Type checking ./Control/Monad/StateE.idr
Type checking ./Interfaces/FileIO.idr
Type checking ./Core/GetType.idr
Type checking ./Core/Unify.idr
Type checking ./Core/Reflect.idr
Type checking ./TTImp/Reflect.idr
Type checking ./Core/Metadata.idr
Type checking ./Core/AutoSearch.idr
Type checking ./TTImp/Elab/State.idr
Type checking ./TTImp/Elab/Rewrite.idr
Type checking ./TTImp/Elab/Delayed.idr
Type checking ./TTImp/Elab/Ambiguity.idr
Type checking ./TTImp/Elab/Term.idr
Type checking ./Core/LinearCheck.idr
Type checking ./Compiler/CompileExpr.idr
Type checking ./TTImp/Elab.idr
Type checking ./TTImp/ProcessType.idr
Type checking ./TTImp/ProcessDef.idr
Type checking ./TTImp/RunElab.idr
Type checking ./TTImp/ProcessData.idr
Type checking ./TTImp/ProcessTTImp.idr
Type checking ./TTImp/REPL.idr
Type checking ./Parser/Raw.idr
Type checking ./Core/ProcessTT.idr
Type checking ./Core/InitPrimitives.idr
Type checking ./Core/Directory.idr
Type checking ./TTImp/Main.idr
Exception in thread "main" java.lang.RuntimeException: Unsupported descriptor: FStr(idris_newRef), returns: FApp(C_Any, [FApp(ImpState, [FCon(Unit)])]), args: [(FApp(C_Any, [FApp(ImpState, [FCon(Unit)])]), Loc 8)]
at io.github.mmhelloworld.idrisjvm.codegen.launcher.IdrisJvmCodegenLauncher.send(IdrisJvmCodegenLauncher.java:104)
at io.github.mmhelloworld.idrisjvm.codegen.launcher.IdrisJvmCodegenLauncher.run(IdrisJvmCodegenLauncher.java:57)
at io.github.mmhelloworld.idrisjvm.codegen.launcher.IdrisJvmCodegenLauncher.main(IdrisJvmCodegenLauncher.java:48)
FAILURE: "idris-codegen-jvm" ["/tmp/idris-cg32061-0.json","-o","/home/martin/Workspaces/idris/Blodwen/ttimp"]
Leaving directory `./src'
echo 'module BlodwenPaths; export bprefix : String; bprefix = "/home/martin/.blodwen"' > src/BlodwenPaths.idr
idris --build blodwen.ipkg --portable-codegen jvm
Entering directory `./src'
Type checking ./BlodwenPaths.idr
Type checking ./Idris/Syntax.idr
Type checking ./TTImp/Utils.idr
Type checking ./TTImp/Elab/Unelab.idr
Type checking ./TTImp/MakeLemma.idr
Type checking ./TTImp/CaseSplit.idr
Type checking ./TTImp/ExprSearch.idr
Type checking ./TTImp/GenerateDef.idr
Type checking ./Idris/REPLOpts.idr
Type checking ./Idris/IDEMode/Commands.idr
Type checking ./Idris/Resugar.idr
Type checking ./Idris/Error.idr
Type checking ./Idris/REPLCommon.idr
Type checking ./Idris/Parser.idr
Type checking ./Utils/Shunting.idr
Type checking ./Idris/BindImplicits.idr
Type checking ./Idris/Elab/Interface.idr
Type checking ./Idris/Elab/Implementation.idr
Type checking ./Idris/Desugar.idr
Type checking ./Idris/ProcessIdr.idr
Type checking ./Idris/ModTree.idr
Type checking ./Idris/IDEMode/TokenLine.idr
Type checking ./Idris/IDEMode/CaseSplit.idr
Type checking ./Compiler/Inline.idr
Type checking ./Compiler/Common.idr
Type checking ./Compiler/Scheme/Common.idr
Type checking ./Compiler/Scheme/Racket.idr
Type checking ./Compiler/Scheme/Chicken.idr
Type checking ./Compiler/Scheme/Chez.idr
Type checking ./Idris/REPL.idr
Type checking ./Idris/CommandLine.idr
Type checking ./Idris/SetOptions.idr
Type checking ./Idris/Package.idr
Type checking ./Idris/IDEMode/Parser.idr
Type checking ./Idris/IDEMode/REPL.idr
Type checking ./Idris/Main.idr
Exception in thread "main" java.lang.RuntimeException: Unsupported descriptor: FStr(idris_newRef), returns: FApp(C_Any, [FApp(ImpState, [FCon(FC)])]), args: [(FApp(C_Any, [FApp(ImpState, [FCon(FC)])]), Loc 8)]
at io.github.mmhelloworld.idrisjvm.codegen.launcher.IdrisJvmCodegenLauncher.send(IdrisJvmCodegenLauncher.java:104)
at io.github.mmhelloworld.idrisjvm.codegen.launcher.IdrisJvmCodegenLauncher.run(IdrisJvmCodegenLauncher.java:57)
at io.github.mmhelloworld.idrisjvm.codegen.launcher.IdrisJvmCodegenLauncher.main(IdrisJvmCodegenLauncher.java:48)
FAILURE: "idris-codegen-jvm" ["/tmp/idris-cg32391-0.json","-o","/home/martin/Workspaces/idris/Blodwen/blodwen"]
Leaving directory `./src'
make -C prelude BLODWEN=../blodwen
make[1]: Entering directory '/home/martin/Workspaces/idris/Blodwen/prelude'
../blodwen --build prelude.ipkg
make[1]: ../blodwen: Command not found
make[1]: *** [Makefile:2: all] Error 127
make[1]: Leaving directory '/home/martin/Workspaces/idris/Blodwen/prelude'
make: *** [Makefile:19: prelude] Error 2I guess the C_Any tells me that it's trying to use C FFI where it should use the JVM.
This line seems to match the problematic one:
https://github.com/edwinb/Blodwen/blob/master/src/TTImp/ProcessTTImp.idr#L77
Your build seems to be way ahead of mine. For me, just running as it is without making any change for JVM produces the following errors:
$ make
idris --build ttimp.ipkg
Entering directory `./src'
Type checking ./Parser/Lexer.idr
Type checking ./Core/Name.idr
Type checking ./Data/CMap.idr
Type checking ./Data/CSet.idr
Type checking ./Core/TT.idr
Type checking ./Parser/Support.idr
Type checking ./Core/CaseTree.idr
Type checking ./Core/Core.idr
Type checking ./Utils/Binary.idr
Type checking ./Core/CompileExpr.idr
Type checking ./Core/TTC.idr
Type checking ./Core/Options.idr
Type checking ./Core/Hash.idr
Type checking ./Core/Context.idr
Type checking ./Core/Primitives.idr
Type checking ./Core/Normalise.idr
Type checking ./Core/UnifyState.idr
Type checking ./Core/Binary.idr
Type checking ./TTImp/TTImp.idr
Type checking ./Core/Typecheck.idr
./Core/Typecheck.idr:23:9:
|
23 | chk : Env Term vars -> Raw -> Either (Error annot) (Term vars, Term vars)
| ^
When checking type of Core.Typecheck.chk:
Can't disambiguate name: FFI_C.Raw, Language.Reflection.Raw, Core.TT.Raw
./Core/Typecheck.idr:55:15:
|
55 | chkBinder : Env Term vars -> Binder Raw ->
| ^
When checking type of Core.Typecheck.chkBinder:
Can't disambiguate name: Language.Reflection.Binder, Core.TT.Binder
./Core/Typecheck.idr:86:15:
|
86 | discharge : (nm : Name) -> Binder (Term vars) -> Term vars ->
| ^
When checking type of Core.Typecheck.discharge:
Can't disambiguate name: Language.Reflection.Binder, Core.TT.Binder
./Core/Typecheck.idr:24:5-38:69:
|
24 | chk env (RVar x)
| ~~~~~~~~~~~~~~~~~ ...
No type declaration for Core.Typecheck.chk
./Core/Typecheck.idr:57:5-60:36:
|
57 | chkBinder env (Lam c x ty)
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
No type declaration for Core.Typecheck.chkBinder
./Core/Typecheck.idr:89:5-90:68:
|
89 | discharge nm (Lam c x ty) bindty scope scopety
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
No type declaration for Core.Typecheck.discharge
./Core/Typecheck.idr:118:10:
|
118 | checkHas : annot -> (gam : Defs) -> Env Term vars ->
| ^
When checking type of Core.Typecheck.checkHas:
Can't disambiguate name: FFI_C.Raw, Language.Reflection.Raw, Core.TT.Raw
Makefile:10: recipe for target 'ttimp' failed
make: *** [ttimp] Error 1
I'm on Arch Linux and used the pre-built Idris package. How did you (compile and?) install Idris?
I created a Dockerfile PR for Blodwen based on Arch, if you want, you could use the first half of the Dockerfile to get a Docker image that is able to build Blodwen:
edwinb/Blodwen#9
Hi @nightscape ,
I fixed my errors and now I am getting the same errors as you. I had to make few changes in idris-jvm and in Blodwen as well. For the current IORef error, I think we have to add JVM_IO implementation for HasReference. I will continue to look into this.
Update:
I have finally got an initial success running Blodwen on the JVM :)
$ java -jar blodwen.jar
Welcome to Blodwen. Good luck.
Main> "hello " ++ "world"
"hello world"
Main> reverse <$> Just "Idris"
Just "sirdI"
Main> :q
Bye for now!
Congratulations!!!
This requires your patched version of Blodwen, right?
I've been reading up on how one could make this compatible with both C and JVM FFI. The recommended way seems to be algebraic effect types (see section 4.4 here and the corresponding section in the official documentation).
I think I understand the basic principles, so this might be something where I could contribute.
If that is ok from your side, I would write an issue in the Blodwen repo and ask if algebraic effects are indeed the right approach and if so give it a go.
Thank you! Yes, it requires my patches which are mainly about changing IO to JVM_IO. It would be awesome if we can parameterize the FFI descriptor in Blodwen so that it compiles without any changes on the JVM given the corresponding implementations in JVM backend.
Btw, this would be a nice announcement in the much to silent Reddit community 😃
Done :)
I think we can close this now as we have been able to compile Blodwen for JVM for a while. I pushed some new updates recently to my fork of Blodwen here to support latest upstream changes. I will keep that fork up to date with latest Blodwen. If there is any new repository for Idris 2, we will then create a new issue to support that for JVM.