mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
Add test
It takes a long time to run, but it is basically all the testing we need of the API, if this works it's unlikely to be broken. It requires a change in the build system, so don't enable it for now.
This commit is contained in:
parent
2ec923d4f3
commit
e32700cff8
2
tests/idris2/api001/Hello.idr
Normal file
2
tests/idris2/api001/Hello.idr
Normal file
@ -0,0 +1,2 @@
|
||||
main : IO ()
|
||||
main = putStrLn "Hello"
|
19
tests/idris2/api001/LazyCodegen.idr
Normal file
19
tests/idris2/api001/LazyCodegen.idr
Normal file
@ -0,0 +1,19 @@
|
||||
module Main
|
||||
|
||||
import Core.Context
|
||||
import Compiler.Common
|
||||
import Idris.Driver
|
||||
|
||||
compile : Ref Ctxt Defs -> (execDir : String) ->
|
||||
ClosedTerm -> (outfile : String) -> Core (Maybe String)
|
||||
compile defs dir term file = do coreLift $ putStrLn "I'd rather not."
|
||||
pure $ Nothing
|
||||
|
||||
execute : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
|
||||
execute defs dir term = do coreLift $ putStrLn "Maybe in an hour."
|
||||
|
||||
lazyCodegen : Codegen
|
||||
lazyCodegen = MkCG compile execute
|
||||
|
||||
main : IO ()
|
||||
main = mainWithCodegens [("lazy", lazyCodegen)]
|
1
tests/idris2/api001/expected
Normal file
1
tests/idris2/api001/expected
Normal file
@ -0,0 +1 @@
|
||||
I'd rather not.
|
3
tests/idris2/api001/run
Normal file
3
tests/idris2/api001/run
Normal file
@ -0,0 +1,3 @@
|
||||
$1 --no-banner -p idris2 -p contrib -p network LazyCodegen.idr -o lazy-idris2 > /dev/null
|
||||
./build/exec/lazy-idris2 --no-banner --cg lazy Hello.idr -o hello
|
||||
rm -rf build
|
Loading…
Reference in New Issue
Block a user