Idris2
Idris2 copied to clipboard
CLI option to stop at codegen/translation and output further instructions
Summary
Currently, the command idris2 can only compile programs as executable objects.
However, this is not useful, since in some cases we want to generate libraries in another programming languages from Idris code.
Motivation
The desire to write code with a good type system, and use it with other languages too.
The proposal
For refc backend, there should be a flag like --gen-only (should be shorter) that only translate Idris2 code to C code, and emit some instructions on further compilation like compile_commands.json. This compile_commands.json can then be used by other build tools.
For other backends, the behaviour should be similar.
Technical implementation
The implementation should be simple. Instead of invoking an external C compiler, print the commands.
Alternatives considered
- Build an Idris2 program to only translate idris2 code to C