HOL-Light: Avoid manual patchup of byte code and disassembly in proof scripts

[hanno-becker]

Currently, the *.ML HOL-Light proof scripts embed the byte code and disassembly of the target object file. Both have to be updated manually upon changes to the code such as re-running SLOTHY. This is tedious and unnecessary, seeing that all proofs are agnostic to specific instruction ordering.

Task: Either remove the embedding of the byte code in the *.ML file, or extend autogen to generate it automatically using print_literal_from_elf from within the HOL-Light shell.

[hanno-becker]

On first sight, it should be possible to:

• Add delimiters to the *.ML proof scripts which mark the region where the byte code + disassembly should be inserted.
• Autogenerate this as part of autogen, by opening a HOL-Light shell with hol.sh and running print_literal_from_elf.

First obstacle here is that hol.sh fails when run straight from the nix develop .#hol_light shell. @mkannwischer @potsrevennil Do you happen to know offhand why? Of course, the proofs are being checked in CI, so the setup is complete, but the proofs are being invoked through build_proof.sh which is rather indirect.

[hanno-becker]

@mkannwischer @potsrevennil Ping.

[hanno-becker]

Nevermind, I figured something out. Will have a PR open soon.