I haven't used it beyond just trying it out once or twice. But a "hello world" application in the Idris2 language compiles to a 17kb racket file (the default ba

I haven't used it beyond just trying it out once or twice. But a "hello world" application in the Idris2 language compiles to a 17kb racket file (the default backend is chez, but it also does racket and javascript). If I run `raco exe` on this, I get a 57MB file. On mac, it's only linking system libraries. (For Idris2 programs, there is an Idris support library that is dynamically loaded.) I haven't tested transporting it to another system (my test was on an arm mac, so I don't have another system to test that on).