Stream: Isabelle/ML

Topic: Sail RISC-C Isabelle build

Changyang Zeng (Apr 17 2026 at 07:02):

Hi users of Isabelle,

I am building Isabelle theories from the Sail RISC-V model here: https://github.com/riscv/sail-riscv.

It seems to cause memory leak when building this file: Rc64d.thy, which has more than 158k lines of code, 3232 definitions. The build on this file has been running for almost two days on an AMD EPYC 7542 32-Core Processor.
Current resource usage:

• CPU: 468% (~4.7 cores busy)
• Memory: 384,135,076 KB RSS (~366.3 GiB)
• Virtual memory: 404,424,516 KB VSZ (~385.7 GiB)
• Percent of RAM: 72.7%
• Elapsed time: 200,264s (~55.6 hours)
• Start time: Tue Apr 14 16:04:14 2026

Machine-wide memory state at the same check:

• Total RAM: 503 GiB
• Used: 441 GiB
• Free: 1.6 GiB
• Available: 62 GiB
• Swap used: 257 GiB of 511 GiB

A simple build on the first few definitions shows that loading this Rv64d_types.thy could take really long time that I can't predict.

Does anyone have experiences on the Sail RISC-V to Isabelle build? Or why Poly/ML is consuming so much memory?

Thanks,
Changyang

Kevin Kappelmann (Apr 17 2026 at 08:47):

I think the authors of the project will likely have experience building the project and be able to answer your question - did you contact them?

Changyang Zeng (Apr 17 2026 at 19:42):

Not yet, I will reach out to them, thanks!

Last updated: Apr 29 2026 at 06:25 UTC