edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Adding variable to compileExpr in Chicken CG stops chicken from produing binaries #351

Closed mokshasoft closed 4 years ago

mokshasoft commented 4 years ago

https://github.com/mokshasoft/Idris2/tree/bug is a minimal change to Idris2 that produce this bug.

Steps to Reproduce

  1. Enable Chicken CG.
  2. Add a dummy variable to compileExpr in ./src/Compiler/Scheme/Chicken.idr.
  3. Compile Idris2
  4. Compile hello world example with Idris2.
  5. No binary is produced.

Expected Behavior

Compiling hello world should produce a binary.

Observed Behavior

[Idris2]$ git diff HEAD^
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
index 08c9157..f928736 100644
--- a/src/Idris/REPL.idr
+++ b/src/Idris/REPL.idr
@@ -1,7 +1,7 @@
 module Idris.REPL

 import Compiler.Scheme.Chez
--- import Compiler.Scheme.Chicken
+import Compiler.Scheme.Chicken
 import Compiler.Scheme.Racket
 import Compiler.Common

@@ -238,8 +238,7 @@ findCG
     = do defs <- get Ctxt
          case codegen (session (options defs)) of
               Chez => pure codegenChez
-              Chicken => throw (InternalError "Chicken CG not available")
-                         -- pure codegenChicken
+              Chicken => pure codegenChicken
               Racket => pure codegenRacket

 anyAt : (FC -> Bool) -> FC -> a -> Bool
[Idris2]$ make idris2
...
[Idris2]$ ls hellobin
ls: cannot access 'hellobin': No such file or directory
[Idris2]$ strace -f -e trace=execve ./idris2 --cg chicken hello.idr -o hellobin 2>&1 | grep "execve.*csc.*= 0$"
[pid  8695] execve("/bin/sh", ["sh", "-c", "/usr/bin/env -S csc /tmp/fileib8"...], 0x7ffcd7c86320 /* 59 vars */) = 0
[pid  8695] execve("/usr/bin/env", ["/usr/bin/env", "-S", "csc", "/tmp/fileib8uxA.scm", "-o", "hellobin"], 0x558ff12a4d70 /* 59 vars */) = 0
[pid  8695] execve("/usr/bin/csc", ["csc", "/tmp/fileib8uxA.scm", "-o", "hellobin"], 0x7ffc7d0fda20 /* 59 vars */) = 0
[Idris2]$ ls hellobin
hellobin
[Idris2]$ rm hellobin 
[Idris2]$ # Update src/Compiler/Scheme/Chicken.idr
[Idris2]$ git diff
diff --git a/src/Compiler/Scheme/Chicken.idr b/src/Compiler/Scheme/Chicken.idr
index 59c11df..cc96a47 100644
--- a/src/Compiler/Scheme/Chicken.idr
+++ b/src/Compiler/Scheme/Chicken.idr
@@ -87,9 +87,9 @@ compileToSCM c tm outfile
          coreLift $ chmod outfile 0o755
          pure ()

-compileExpr : Ref Ctxt Defs -> (execDir : String) ->
+compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
               ClosedTerm -> (outfile : String) -> Core (Maybe String)
-compileExpr c execDir tm outfile
+compileExpr dummy c execDir tm outfile
     = do tmp <- coreLift $ tmpName
          let outn = tmp ++ ".scm"
          compileToSCM c tm outn
@@ -110,6 +110,6 @@ executeExpr c execDir tm

 export
 codegenChicken : Codegen
-codegenChicken = MkCG compileExpr executeExpr
+codegenChicken = MkCG (compileExpr False) executeExpr
[Idris2]$ make idris2
...
[Idris2]$ strace -f -e trace=execve ./idris2 --cg chicken hello.idr -o hellobin 2>&1 | grep "execve.*csc.*= 0$"
[Idris2]$ ls hellobin
ls: cannot access 'hellobin': No such file or directory
edwinb commented 4 years ago

I haven't been maintaining the Chicken CG, and, to be honest, probably won't again - there's enough to maintain as it is - so I might just remove the code. However, executables are put in build/exec now, so it might be there. Other things may have changed since I disabled it too, though.

mokshasoft commented 4 years ago

This issue was not really about the Chicken backend, it was merely the context where I encountered an unexpected behavior. Adding a dummy variable to compileExpr, that isn't used, changed the runtime behavior of the generated idris2 binary. It may be me not understanding something correctly, or an error in Idris1, or only an error in the Chicken backend. I don't know. The reason that I was looking into the Chicken backend was because it was the only backend that supported transcompilation to C as far as I could see, which I think would be the easiest way to port the FreeRTOS Idris1 port to Idris2.

abdelq commented 4 years ago

@mokshasoft When #317 is merged, you could maybe use that instead to compile to C.

mokshasoft commented 4 years ago

Thanks! That looks promising.

edwinb commented 4 years ago

I've merged the gambit back end now. I think it has the same advantages as chicken (native code, fast startup of the interpreter), but seems to be a better fit with the kind of code that Idris 2 is throwing at it, so I'll remove chicken.

The error itself is a bit strange, and might indicate a problem somewhere in Idris 1, but I should probably prioritise other things given that Chicken isn't used (and, strangely, it doesn't happen with other back ends that behave this way)

mokshasoft commented 4 years ago

Closing, since Chicken backend is removed.