search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.51k stars 374 forks source link

Weird bug with IDRIS2_INC_CGS #2565

Open iacore opened 2 years ago

iacore commented 2 years ago

Steps to Reproduce

Compile the following code

%foreign "javascript:xyz"
prim__run_next_tick : IO a -> IO a
  1. set -x IDRIS2_INC_CGS chez or export IDRIS2_INC_CGS=chez
  2. idris2 --cg javascript --wp callcc.idr
> :r
1/1: Building callcc (callcc.idr)
Error: The given specifier '["javascript:conth"]' was not accepted by any backend. Available backends:
  chez, chez-sep, racket, node, javascript, refc, gambit, vmcode-interp
Some backends have additional specifier rules, refer to their documentation.
  1. modify file to be %foreign "javascript:lambda:(f)=>f()"
  2. Main> :r
Main> :r
1/1: Building callcc (callcc.idr)
Error: The given specifier '["javascript:lambda:(f)=>f()"]' was not accepted by any backend. Available backends:
  chez, chez-sep, racket, node, javascript, refc, gambit, vmcode-interp
Some backends have additional specifier rules, refer to their documentation.

Expected Behavior

%foreign "javascript:lambda:(f)=>f()" should be accepted as valid code.

Observed Behavior

See above

dunhamsteve commented 2 years ago

The IDRIS2_INC_CGS environment variable asks Idris to build the .so files for all listed codegens whenever it builds the .ttc files. Internally, the .ttc files contain a list of incremental backends for which they have incremental support.

Technically this is consistent with the documentation at IncrementalCodeGeneration, but I don't think it's clear from that documentation that the binary code is produced regardless of the target codegen. I only know this because I saw it in the code:

https://github.com/idris-lang/Idris2/blob/e5802204b644258235552b443fb1029e05dc1e4c/src/Idris/ProcessIdr.idr#L421-L429

If an existing ttc doesn't support an incremental back end (has no .so file) during an incremental build, the compiler tries to switch to whole program (but there is a bug, #2557, that causes incremental to be reenabled, generating a broken executable).

Having IDRIS2_INC_CGS defined also globally disables an optimization in Inline.idr.