search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

Add tracing kernel #1309

Open digama0 opened 2 months ago

digama0 commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

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".

mn200 commented 1 week ago

Is there an easy fix for the regression here? Would be nice to resolve the PR if possible.

digama0 commented 1 week ago

This project has gone to the backburner for me but I think I might be better equipped to understand the issues and get it to build now.