Building Idris 2 with new backends
The way to extend Idris 2 with new backends is to use it as
a library. The module Idris.Driver
exports the function
mainWithCodegens
, that takes a list of (String, Codegen)
,
starting idris with these codegens in addition to the built-in ones. The first
codegen in the list will be set as the default codegen.
Getting started
To use Idris 2 as a library you need a self-hosting installation and then install the idris2api library (at the top level of the Idris2 repo)
make install-api
Now create a file containing
module Main
import Core.Context
import Compiler.Common
import Idris.Driver
import Idris.Syntax
compile :
Ref Ctxt Defs -> Ref Syn SyntaxInfo ->
(tmpDir : String) -> (execDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile syn defs tmp dir term file
= do coreLift $ putStrLn "I'd rather not."
pure Nothing
execute :
Ref Ctxt Defs -> Ref Syn SyntaxInfo ->
(execDir : String) -> ClosedTerm -> Core ()
execute defs syn dir term = do coreLift $ putStrLn "Maybe in an hour."
lazyCodegen : Codegen
lazyCodegen = MkCG compile execute Nothing Nothing
main : IO ()
main = mainWithCodegens [("lazy", lazyCodegen)]
Build it with
$ idris2 -p idris2 -p contrib -p network Lazy.idr -o lazy-idris2
Now you have an idris2 with an added backend.
$ ./build/exec/lazy-idris2
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.2.0-bd9498c00
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
With codegen for: lazy
Main>
It will not be overly eager to actually compile any code with the new backend though
$ ./build/exec/lazy-idris2 --cg lazy Hello.idr -o hello
I'd rather not.
$
About the directories
The code generator can assume that both tmpDir
and outputDir
exist. tmpDir
is intended for temporary files, while outputDir
is the location to put the desired
output files. By default, tmpDir
and outputDir
point to the same directory
(build/exec
). The directories can be set from the package description (See Section
Packages) or via command line options (Listed in idris2 --help
).