idris-lang/Idris2

A plea for improved Gambit support for bare metal

flintwinters opened this issue · 9 comments

flintwinters commented

A plea for improved Gambit support for bare metal

  • I have read CONTRIBUTING.md.
  • I have checked that there is no existing PR/issue about my proposal.

Summary

The Gambit backend has the potential to be very powerful, but support seems to have fallen by the wayside.

Motivation

From this page: https://idris2.readthedocs.io/en/latest/faq/faq.html
"one of [Idris'] longer term goals is to be able to write efficient and verified low level code such as device drivers and network infrastructure."

Being able to run executable code on a given platform without a runtime is imperative in achieving this goal.
The gambit bare metal backend is not only a vital stepping stone, but it is also capable of compiling to numerous other platforms. From the website:
Targets C, JavaScript, Python, and more. Runs in web browsers and has run on Nintendo DS, routers, and FPGAs.

The proposal

Examples

I've been told the resulting code is unusually slow.

Technical implementation

Alternatives considered

Unfortunately I don't know enough to answer these.

Conclusion

flintwinters commented

UPDATE: Seems I had compiled the requisite gambit 4.9.5, but neglected to swap it out for the out-of-date 4.9.3 in my path.
I had previously listed the resulting errors in the original post, but removed them.
I'll leave this issue up since I've been talking with several people in the discord about the gambit support being problematic.

Below is the error message for searching:

│idris2 -q --cg gambit --directive C test.idr --exec main
│build/exec/_tmpgambit: 2: Syntax error: ";" unexpected

And setting export GAMBIT_GSC_BACKEND= to anything results in errors like:

│*** WARNING -- Unknown or improperly placed -cc option

and

s2_support.a"@3.1 -- Illegal character: #\null
Error: INTERNAL ERROR: compileExpr returned Nothing
stefan-hoeck commented

Maintenance of the gambit backend has stalled because a) it cause lots of issues during testing in CI (it was horribly slow), and b) noone stepped in to take care of the backend and fix these issues. I see two ways forward: Either someone commits themselves to take care and maintain this backend as part of the main Idris project, or it should be moved to a community repository. Either way, it should be maintained by someone who is actually using it regularily. Nobody seems to be currently doing that.

GunpowderGuy commented

I want to add that besides chez, gambit is the other scheme implementation with excellent performance. The author continues to add new optimizations and idris2 could benefit from this

andrevidela commented

I think the gambit backend should be treated as a third party backend rather than live within the idris repo. Maybe we could extract it to idris-community ?

  • 👍3
dunhamsteve commented

I can do small bits of fixing here and there, but I am not actually using it at all. And I agree with stefan that it would best be maintained by someone who uses it. Moving it to a separate repository might also serve as an example on how to make a new backend - it would leverage all of the common scheme bits, but at least it could show some of the project structure. I'm not volunteering to extract it at this time.

Two issues for this bug report:

  • "Gambit after version v4.9.3" in the docs caused some confusion. I'm going to change it to "Gambit version 4.9.4 or newer". And I'll remove the instruction to compile from source, since 4.9.5 is widely available pre-built.
  • There is some confusion above around --directive C. It generates a .c file, which is not executable. I'll tweak the docs to make this clearer and also replace --codegen chez with --codegen gambit in the example invocation.
MeanSquaredError commented

The LLVM backend for Idris 2 is under active development and it is almost fully functional. Judging from the README, the only thing that it lacks at the moment is concurrency. Once concurrency is implemented it should be possible to adjust its runtime and make it work on bare metal without OS support. I would imagine that the adjustment of the runtime would mean mostly implementing the missing GLIBC functions that are used by the runtime.

Disclaimer: I am not affiliated with the Idris2 LLVM backend in any way. I just keep an eye on it development waiting until it becomes fully usable.

  • 👍1
eayus commented

Not directly related to the gambit backend, but I've been doing my PhD on compiling functional languages without using a heap or garbage collector, with the aim of making functional languages more suitable for bare metal. I haven't published the work yet, but when I do, maybe I'll have a go at implementing an Idris backend.

In summary, I've been using partial evaluation to eliminate parts of the program which use high-level features such as higher-order functions and type classes. I make some type system modifications which ensure that the partial evaluator can eliminate all high-level features - this rules out some programs, but still leaves a language which is practical to program with. If anyone is interested, let me know and I'd be happy to explain what I'm doing in more detail.

  • 👍2
GunpowderGuy commented

@eayus Your work seems highly related to the feature available in F* that allows a subset of the language to be compiled to highly perfomant c code. I would be interested in having such a feature for idris2, as i am working on the GRIN backend. A highly optimizying backend that shares some similarities with said F* code extraction tecnique, and would benefit from having its RTS written in a functional language. Please contact me trough the email in my profile or in the idris2 server ( i have the same username )