Small runtimes

Stream: Real-time Systems

[Alex J. Best]

@Joe Hendrix Nice blog post! As for the issue of gmp in the runtime, do you think it is possible to compile against mini-gmp https://gmplib.org/repo/gmp-6.2/file/tip/mini-gmp or even something like https://www.arduino.cc/reference/en/libraries/gmp-ino/. I haven't tried using leanc myself so I have no idea if this is possible even, just a thought that came to mind when reading the post :smile:

[Joe Hendrix]

@Alex J. Best That's an interesting idea. The bigger problem if I recall correctly is that for technical reasons currently every constant in the Lean compiler/interpreter gets included in the Lean standard library. I think a fix will need to be developed when the compiler is ported from C++ to Lean.

[Joe Hendrix]

But once that's done, then linking against a mini-gmp seems like a good idea.

[Sebastian Ullrich]

The stdlib would probably have to be recompiled against mini-gmp, but as long as all of the operations it uses are included, I think this could work right now.

[Sebastian Ullrich]

@Joe Hendrix If we fixed the compiler, I assume it would be feasible that your code would not depend on GMP at all?

[Joe Hendrix]

@Sebastian Ullrich I think so. There are a few Nat values right now, but those could easily be changed into UInt values.

[Mario Carneiro]

How much of GMP is actually needed? It should be possible to write a pure-C small replacement for GMP if you don't have to worry about getting the absolute best performance

[Mario Carneiro]

er, I guess that's mini-gmp?