Zulip Chat Archive

Stream: Real-time Systems

Topic: Small runtimes


Alex J. Best (Mar 30 2021 at 23:53):

@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 (Mar 30 2021 at 23:56):

@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 (Mar 30 2021 at 23:57):

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

Sebastian Ullrich (Mar 31 2021 at 07:47):

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 (Mar 31 2021 at 07:48):

@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 (Mar 31 2021 at 16:55):

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

Mario Carneiro (Mar 31 2021 at 17:05):

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 (Mar 31 2021 at 17:06):

er, I guess that's mini-gmp?


Last updated: Dec 20 2023 at 11:08 UTC