`Holmake: Exception: Subscript` when building HOL with -j12 or greater (but not -j11 or lower)

[someplaceguy]

`Holmake: Exception: Subscript` when building HOL with -j12 or greater (but not -j11 or lower)

[mn200]

Fascinating. Does it reproduce with --stdknl instead of --expk? (I'll be super-surprised if it doesn't.)

I guess there's an error still lurking in the way Holmake prints its little display of running processes to the screen (see an earlier one at b51b4f1). If you run with a smaller -j number but a narrower terminal screen can you also reproduce?

[mn200]

I can confirm that it reproduces on --stdknl. It will also fail faster if you build with -t because the degree of parallelisation possible in tools/Holmake/tests/parallel_tests is enough to prompt the problem.

[mn200]

The problem is definitely with the display: if you run

build -t --stdknl -j12 | tee logit

the pretty displaying doesn't happen because it doesn't think it's writing to a terminal and the build goes fine.

[someplaceguy]

I tried to build HOL with a terminal 1/3rd as wide (with -j12) and it also failed, but I'm not sure if that's actually doing anything because there are many layers of abstraction in-between the build and the actual terminal.

To be more precise, I'm running the build inside of a local tmux session, and furthermore the build is going through a local daemon (nix-daemon), which connects over ssh to another nix-daemon on a remote machine, which actually does the build inside a sandbox and captures the output log of the build (and in this specific case, it also sends it in real-time to my terminal).

So I heavily suspect that my actual terminal size has no effect on the build behavior and I would be slightly disappointed if it did (since it would interfere with all the efforts that NixOS has made to make builds as reproducible as possible, even though it still has countless limitations).

EDIT: sorry, I misread your question. I will try reproducing with a narrower terminal and with -j11.

EDIT 2: I can now confirm that in my setup, it succeeds with a terminal 1/3rd as wide and with -j11. In other words, the terminal width doesn't seem to have a difference in my environment.

But as I mentioned before, that's probably to be expected given my setup. So the bug might still be related to the terminal width, it's just that it seems that I have no easy way of changing it due to how the build is being done.

[mn200]

Holmake explicitly makes shell calls to stty size and tput cols to try to figure out its "terminal" width (after first determining if the output stream is a tty at all). [I appreciate that this is gross.]

If you can resize your terminal so as to affect the numbers it gets out of those calls (it tries stty first and then falls back to tput), you might reproduce with a smaller -j. Of course, the error may well be quite dependent on things like width % j too, so simply making it narrower may mask the bug we're seeing at 80 columns.

It's still clearly a bug, and I think/hope it should be easy to fix.