Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

A plea for improved Gambit support for bare metal #3387

Open
2 tasks done
flintwinters opened this issue Sep 16, 2024 · 9 comments
Open
2 tasks done

A plea for improved Gambit support for bare metal #3387

flintwinters opened this issue Sep 16, 2024 · 9 comments

Comments

@flintwinters
Copy link

flintwinters commented Sep 16, 2024

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
Copy link
Author

flintwinters commented Sep 16, 2024

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
Copy link
Contributor

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
Copy link

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
Copy link
Collaborator

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 ?

@dunhamsteve
Copy link
Contributor

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
Copy link

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.

@srghma

This comment was marked as abuse.

@eayus
Copy link
Contributor

eayus commented Nov 14, 2024

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.

@GunpowderGuy
Copy link

GunpowderGuy commented Nov 14, 2024

@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 )

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

8 participants