asciilifeform: note that rockchip boxen cannot use the kvm, they have no kbd or display
asciilifeform: if anyone needs the kvm, plz page BingoBoingo to plug it in, and asciilifeform to show how to connect to it
asciilifeform: also obtained and set up a 2nd GB switch in rack; and a 220v mains distributor; and a ip kvm ( which annoyingly requires... java on the remote control end, but 'with torch in daylight' to this very day i cannot find ANY ipkvm that does not commit this type of warcrime )
asciilifeform: delivered, moorings hammered back into shape , enracked, (where applicable) en-disked, en-os'd, powered, sshkeyed, tested.
asciilifeform: at a total cost of ~2k ( i'ma do a proper rundown tomorrow ) usd.
asciilifeform: spyked: it'll happen. tho i am aiming for folx to end up answering 'this did not need sparkism, it is evidently correct to naked eyes'
asciilifeform: spyked: i dun have anything against mechanical proof per se; but it is NOT a substitute for fits-in-head, because there is nor cannot be any such substitute. and the mass of the theorem-verifier is to be included with the mass of the program, for the purpose of 'is this head-fittable'. but possibly i repeat old thread.
asciilifeform: spyked: sorta how it is ~impossible to write a prolog proggy without several times ending up asking machine np-hard question.