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

proof-extra with data rather than strings #607

Merged
merged 3 commits into from
Sep 28, 2024
Merged

Conversation

MichaelRawson
Copy link
Contributor

We have started to receive interest in more proof outputs (e.g. Dedukti @anjapetkovic, Metamath @digama0) and these require a greater degree of granularity in proofs as they are machine-checked.

We already have --proof_extra, but it's stringly-typed and hard to use for this purpose. Make explicit objects recording information about the proof for downstream use.

While we're at it:

  1. Include resolution, demodulation, and equality resolution in the extra'd inferences. Not (equality) factoring as they're painful to adapt at the moment - more later.
  2. Only on/off "proof extra" flag, I couldn't find much use for the halfway FREE option. Happy to be persuaded.
  3. Change the format and data stored slightly. In my view this makes more sense.

@digama0
Copy link

digama0 commented Sep 20, 2024

This will conflict with some of the changes I've made, but that's my fault for sitting on the s-expr PR for too long. I'll rebase it on top of this, I don't think the version of InferenceExtra I implemented is too different from this.

@MichaelRawson
Copy link
Contributor Author

Ah, you actually did something already! That's my fault, I should have communicated what I was doing - I just had a spare few hours today by some miracle. If it's easy to rebase go ahead, if not lmk and we can figure out what to do with it.

@quickbeam123 quickbeam123 merged commit a327cc6 into master Sep 28, 2024
1 check passed
@quickbeam123 quickbeam123 deleted the michael-proof-extra branch September 28, 2024 12:49
@MichaelRawson
Copy link
Contributor Author

MichaelRawson commented Oct 2, 2024

@digama0 - I was quite pleased with this design until today, when we tried to use it and were told we can't static_cast from an InferenceExtra * to a derived class. This is because of annoying technical reasons related to virtual inheritance.

@anjapetkovic and I will likely fix it together ("composition over inheritance" is the way to go, I expect) in the next few days so we can make progress on Dedukti. Let us know if you need something.

@digama0
Copy link

digama0 commented Oct 2, 2024

I'll try to make a PR with my version of this thing. (I didn't use subtyping, I just had a discriminated union for InferenceExtra.) Sorry for the delay, my time for this is more limited than it was a few weeks ago.

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.

3 participants