Idris2
Idris2 copied to clipboard
idris-lang
chez bootstrap requires large amount of memory
I am trying to build on a system with 6GB of ram, and I'm consistently OOM on the bootstrapping step for building Idris2-boot from Idris2-boot.so. Is there some way to reduce the memory bottleneck here, maybe forcing a single-threaded compile, or is this where it ends
6GB should be just enough, but obviously if you're seeing it be killed, that's a problem. What system are you trying to do this on? Apple Silicon? x86_64? ARM? And is there anything running in the background or is your terminal the only process? : )
My personal experience (on x86_64) is that it takes a max of ~4GB of memory to bootstrap, although other people have reported that WSL with 8GB was not enough.
All is not lost: you could try bootstrapping via Racket instead of Chez. They have different strategies and configurations, especially for garbage collection and other memory things, so you might have more luck with that? The process is slightly different, but it's detailed in the README : )
If that doesn't work, you could try setting up a swap-file of 4GB. Which will likely make it work, but now you're looking at half-a-day timescale rather than 5-10 minutes : /
For me, when running in an x86 Linux VM with insufficient memory, it would die at the last step of building idris. The idris compiler was using a lot of memory and had written out the .ss file and had forked a chez subprocess to compile it. The sum of the two processes in memory at the same time was the issue.
The last step is scheme --script compileChez in build/exec/idris2_app. On an M1 Mac with the latest racket port of chez, this process by itself uses 2.6GB of memory - on top of what idris is using. Oddly, changing the optimization level to 0 uses more memory and takes more time. (I swear that wasn't the case last time I tried.)
If you have enough memory for just that you could run the scheme manually, but I wouldn't know how to make the makefile handle that. (Maybe change it to ignore the return value from idris and rerun the scheme build.)
The last step of a build for the racket backend (IDRIS2_CG=racket) only uses 898 MB of memory for the raco exe -o idris2 idris2.rkt. If you can get racket installed on the device and compile for racket, you might have better luck with racket.
Edit to add - there is also incremental building, IDRIS2_INC_CGS=chez - but I think there might be an issue bootstrapping with that turned on.
It's android with racket chez fork, no root
On mobile, that's cool! :eyes: IIRC, @Z-snails had success with that? : )
I tried a racket build but it failed when compiling one of the Idris libraries (Data.Description.Regular)
I had an idea to do an incremental build on another machine, copy the build tree, have chez rebuild all of the .so files, and do a make install. I've scripted it, but then learned that incremental builds don't work with racket chez. The idris2.ss that is being generated is not including the modules in the right order and racket chez is fussy about that. (Libraries-Text-Literate.so depends on Libraries-Text-Lexer.so, but is listed first.)
I'd like to add that my machine has 12gb of RAM and I'm using WSL2 (so at most 6GB) and the jump from 0.6.0 to 0.7.0 is quite vast. I had no problem bootstrapping 0.4.0 and building normally to 0.5.1 and then 0.6.0. I'm stuck on 0.6.0 because 0.7.0 fails to build the executable, most likely due to lack of memory.
Edit: I attempted to install Idris2 on native windows. After lots of trial and error, I got it to work! Specifically, on an older laptop with 4gb of RAM and using MSYS2, I bootstrapped using v0.2.2 and then building incrementally upwards up to 0.7.0. This last version took 4 hours to complete. I also had to manipulate the PATH variables because Chez Scheme automatically installs in 'Program Files' and Idris2 doesn't like directories with spaces in the name.
