start a loggable kernel whose theorems have proofs attached

originally these commit messages:
--
start work on a liberally logging kernel

The idea is to log HOL4's primitive (including derivable) inferences as
they happen, and then deal with converting this log to one using only
Opentheory primitives later. One advantage might be that it should
require less extensive changes to the HOL4 kernel.

This commit is a minor preparatory step: split the OpenTheoryMap into
two parts, one that will happen prekernel (so that Thm can see the
Opentheory names to log) and the other that happens after Theory (so it
can use LoadableThyData). Of course, Thm should only ever look at the
map well after various later theories have populated it (with
side-effects) using the second interface.
--
Actually, better to keep logging after the kernel

Which is possible if we store logging information in the form of
"proofs" attached to the theorems. The only visible change is that the
proof type and functions like get_proof, delete_proof etc. will be
visible in Thm, but that appears to be fine (so it's a superset of
FinalThm rather than matching exactly). This is the way Joe logs
HOL-Light proofs - I intend to emulate fairly closely.

The main reason to do it this way is that not every theorem produced
needs to be logged. Indeed logging facility will probably have a log_thm
: thm -> unit, which could be linked to save_thm (at the expense of
touching Theory).

Thm doesn't need to know whether logging is happening or not. But it may
pay to let it know (e.g. via a flag in Globals) later if storing proofs
all the time is too memory-intensive.
start work on logging facility (that will use the logging kernel)

Putting it in a separate directory, because this code will want Thm to
have an extended signature, so won't work on the non-logging kernels.
But we can keep this directory out of the normal build sequence.
Merge branch 'master' into logging
logging facility work in progress (terms, but not yet theorems)
start work on log_thm

Contrary to the initial plan of having an intermediate extended article
file format, it seems feasible to do the compilation to the OpenTheory
virtual machine on the fly. Being outside of the kernel (and thus in the
scope of boolTheory, Drule, etc.) makes this possible. However, we must
be careful to avoid implementing an inference rule in terms of itself
(and thus sending log_thm into a loop).

SUBST is the first rule to pose a challenge (and probably won't be
the last), so I've left it for now. Next step is probably to get rid of
TODO_prf (by adding proof cases for the remaining rules in Thm).
Implement SUBST for the OpenTheory kernel

As with everything else in src/opentheory/logging at the moment, the
only tests that have been run are syntax- and type-checking.
Implement 10 more inference rules on OpenTheory kernel

Also rewrite MP, because previous code was likely to loop.
20 rules to go.
Merge branch 'master' into logging
Implement all but definitional inference rules in OpenTheory

Plenty taken from bool.ml in HOL Light.
Now only prim_type_definition, prim_constant_definition, and
prim_specification remain unloggable to an opentheory article.
Merge branch 'master' into logging
make proofs deletable

premature optimization for freeing memory
implement constant definitions

the simplest of the definitional principles, since the OpenTheory kernel
uses the exact same rule.
Implementing prim_new_specification for opentheory

Taken from the implementation of new_specification in HOL Light.

Also, expose the ability to create a ("MK_THM"-tagged) theorem with a
given proof object, to fake a prim_define_constant theorem after the
constant has already been defined (so as not to retire the name).
implement prim_type_definition for opentheory

Currently uses backward proof to generate the theorem the virtual
machine should produce. Could probably be replaced with a proforma
theorem (as in many other commands) if that would be beneficial.

We only make definitions (of types or constants) on the virtual machine
if the theorems generated by prim_type_definition or
prim_constant_definition get used in the logging of an explicitly
exported theorem. This might be good enough, but it might also be nice
to allow a user to explicitly log a definition without actually using
those theorems (maybe the user doesn't know when they're getting used).
(Easy to implement: just log the theorem without calling "thm" (i.e.
without saving it as an article export) at the end.)
use a proforma theorem for type definitions on opentheory

The forward proof is still pretty long. Feel free to improve it. I think
there is an advantage to having a proforma theorem, though. Namely, that
if more than one type definition is made during logging, the virtual
machine has to do fewer inferences (prove the pth once, instantiate
twice, versus do a similar amount of proving twice).
make export_thm return the theorem rather than unit
fix identifiers-out-of-scope errors in Logging
bugfixes
actually update the dict for hash-consing
bugfix: was creating the wrong thm for a GEN_prf

not sure, though, because GEN is still possibly causing problems (there
is a cyclic dependency somewhere)