Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

CLI option to stop at codegen/translation and output further instructions

Open iacore opened this issue 3 years ago • 0 comments

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

iacore avatar May 07 '22 20:05 iacore