Add tracing kernel

[digama0]

• Depends on Add more primitive proof rules #1308
• Depends on https://github.com/digama0/polyml/compare/exportSmall

Adds a new kernel type, --trknl. This is mostly the same as the standard kernel, but it uses the OT kernel for the Thm type. There is also one additional step during the export_theory command, in which the export data is pickled directly into a byte blob (preserving sharing) and written out. The result is postprocessed with gzip to avoid the traces from getting too large.

This depends on my fork of PolyML for the exportSmall function, which was added for a very similar use case in Isabelle.

[mn200]

Your tracing/{yes, no} directories should include Tracing.sig and Tracing.sml files (separating out the structure and signature declarations), and don't need Holmakefiles (what you've declared there is the default behaviour).

Note how the Moscow ML build fails. You can get Moscow ML to work with complicated mixtures of functors, structures and signatures all in the one file, but it’s unnecessary work in cases like this.

[digama0]

Is there a way to make tracing/yes/Tracing.sig and tracing/no/Tracing.sig be the same file? They have the same signature after all.

[digama0]

Hm, I'm not really sure how to do the ifdef in this situation. I would like to have a function which is enabled only for polyml+trknl, and which is not assumed to compile on any other combination. It is unclear to me why references to the PolyML module from other files (such as tracing/yes/Tracing.sml) does not work.

[mn200]

There's an example of this sort of dance in the way src/portable/Arbint is able to use PolyML's built-in support for arbitrary ints but the Moscow ML code uses its own implementation. You could also just dispense with the signature entirely in both cases and just make sure the structure doesn't open anything into its exported namespace:

  structure Tracing = struct
      local open stuff in 
      fun trace ... = ...
      end
  end

Moscow ML is happy with this "style".