provide doc files under CC-BY-SA-4.0

convert license headers to SPDX

Run HOL4/bin/build in Makefile; document.

The HOL4 INSTALL file suggests that the user should run the HOL4/bin/build
script to finish the HOL4 install process. This was the slowest of the steps
done during the setup phase. This change suggests that the user not run build
manually and calls it from the Makefile, thus moving the CPU time into the
batch phase.

Improve documentation and output.

Better document SMT/.solverlist issues.

Raf found a couple of common misunderstandings, so I've been a lot
more explicit about which solvers are needed/useful and what to expect.

Slight documentation improvement, I think.

Example target for testing seL4 build.

This should be useable for building the seL4 binary verification
problem.