HOL4 decompile run and sync

[lsf37]

Might be small enough to work on GitHub runners, might not.

@mbrcknl do you know how much memory a decompile-only run needs?

[mbrcknl]

I've not paid a lot of attention to that, so I'll run a test to find out. My guess is that it should be within a GitHub runner's resources.

[mbrcknl]

I guessed wrong. :-(

Peak memory usage was about 12Gb, towards the end of the decompilation. The whole process, including building PolyML and HOL4, took about 2 and a half hours.

AFAICT, that was not using PolyML's 64-in-32 mode. I'll see if I can retest with that enabled, but I guess it's still likely to be over the limit.

[lsf37]

With 12GB there's still a chance. If 32bit roughly halves it, then it fits within the 7GB the GitHub runners have. Time is less of an issue.

[mbrcknl]

Interesting. I had previously thought that PolyML's 32-in-64 mode (not 64-in-32 as I wrote above) only reduced the size of pointers in the runtime implementation. But it looks like it also reduces the size of integer types in the SML language.

HOL4 itself built ok with 32-in-64, but the decompiler implementation assumes 64-bit integer types in some places. I tried one round of fixing that, but it goes a little deeper than I have time for right now.

In any case, this, along with the rest of BV, was already on my to-do list, and I'm happy for it to stay there. It might take me some time to get through it, though. Some parts of BV will require non-GitHub runners, at least until we can build distributed execution into the proof search procedures.

[lsf37]

Ok, no worries. Let's just put it on the list of things that need more powerful runners for now.

[lsf37]

AWS runners are now available and working for standard l4v. We can even tweak number of CPUs/memory requirements for this as we need (as long as money lasts ;-)).

It looks like we can just port over the Bamboo plan as is, or did you have further changes in mind before we do that?

[lsf37]

This is now done.