Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add tracing kernel #1309

Open
wants to merge 4 commits into
base: develop
Choose a base branch
from
Open

Add tracing kernel #1309

wants to merge 4 commits into from

Conversation

digama0
Copy link
Contributor

@digama0 digama0 commented Sep 21, 2024

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
Copy link
Member

mn200 commented Sep 23, 2024

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
Copy link
Contributor Author

digama0 commented Sep 23, 2024

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
Copy link
Contributor Author

digama0 commented Sep 23, 2024

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
Copy link
Member

mn200 commented Sep 24, 2024

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
Copy link
Member

mn200 commented Nov 17, 2024

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

@digama0
Copy link
Contributor Author

digama0 commented Nov 17, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants