How to process dummylink?

55 views
Skip to first unread message

Marko Grdinic

unread,
Dec 3, 2019, 8:49:26 AM12/3/19
to Metamath
I am working on my own verifier and am in the debugging stage. I can verify demo0.mm, but I've encountered a strange issue while trying to verify set.mm.

    dummylink $p |- ph $=
      (  ) C $.

I am not sure what C is here, but ( and ) should definitely be constants. This surprised me. I might have missed it while reading the manual, but I had not expected that constants could just be placed on the stack. Am I wrong here?

Marko Grdinic

unread,
Dec 3, 2019, 9:03:57 AM12/3/19
to Metamath
Sorry about this, as soon as I posted I realized that I had completely forgotten about compressed proofs.

Marko Grdinic

unread,
Dec 3, 2019, 9:32:07 AM12/3/19
to Metamath
Well, at any rate as I've been working on this for 9 days now I'll stop here. I do not feel like going those last few extra miles just to implement proof decompression and test it thoroughly on the big library. I am not sure how stringent the criteria for inclusion on that list of verifiers in other languages are, but it might be good enough for consideration anyway even in its current form.

I am impatient to start studying set theory so I'll get to that. That was what attracted me to Metamath in the first place. Doing this toy implementation was a side quest.

Antony Bartlett

unread,
Dec 3, 2019, 10:18:22 AM12/3/19
to meta...@googlegroups.com
Uncompressing the entire set.mm database was last discussed here



    Best regards,

        Antony


On Tue, Dec 3, 2019 at 2:32 PM Marko Grdinic <mra...@gmail.com> wrote:
Well, at any rate as I've been working on this for 9 days now I'll stop here. I do not feel like going those last few extra miles just to implement proof decompression and test it thoroughly on the big library. I am not sure how stringent the criteria for inclusion on that list of verifiers in other languages are, but it might be good enough for consideration anyway even in its current form.

I am impatient to start studying set theory so I'll get to that. That was what attracted me to Metamath in the first place. Doing this toy implementation was a side quest.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fbd4651b-9429-4ecb-96ae-db8ebbaa7431%40googlegroups.com.

Marko Grdinic

unread,
Dec 3, 2019, 10:31:52 AM12/3/19
to Metamath
Yeah, it works fine on demo0.mm. I did some examples by hand to make sure that disjointment constraints are verified properly as well.


Dana utorak, 3. prosinca 2019. u 16:18:22 UTC+1, korisnik Antony Bartlett napisao je:
Uncompressing the entire set.mm database was last discussed here



    Best regards,

        Antony


On Tue, Dec 3, 2019 at 2:32 PM Marko Grdinic <mra...@gmail.com> wrote:
Well, at any rate as I've been working on this for 9 days now I'll stop here. I do not feel like going those last few extra miles just to implement proof decompression and test it thoroughly on the big library. I am not sure how stringent the criteria for inclusion on that list of verifiers in other languages are, but it might be good enough for consideration anyway even in its current form.

I am impatient to start studying set theory so I'll get to that. That was what attracted me to Metamath in the first place. Doing this toy implementation was a side quest.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to meta...@googlegroups.com.

David A. Wheeler

unread,
Dec 3, 2019, 5:52:34 PM12/3/19
to metamath, Metamath
On Tue, 3 Dec 2019 06:32:07 -0800 (PST), Marko Grdinic <mra...@gmail.com> wrote:
> Well, at any rate as I've been working on this for 9 days now I'll stop
> here. I do not feel like going those last few extra miles just to implement
> proof decompression and test it thoroughly on the big library. I am not
> sure how stringent the criteria for inclusion on that list of verifiers in
> other languages are, but it might be good enough for consideration anyway
> even in its current form.

You can use Metamath.exe to decompress proofs and
then run your tool if you'd like to. You can see that discussion here:

https://groups.google.com/forum/#!msg/metamath/Hey2L9f1ULk/vXMWVcI5DwAJ

--- David A. Wheeler

Tony

unread,
Dec 5, 2019, 12:10:50 PM12/5/19
to Metamath
I found proof decompression to be easier to implement than I thought it would be. The hardest part was just understanding how it works.

Mario Carneiro

unread,
Dec 5, 2019, 12:48:15 PM12/5/19
to metamath
I agree; I think implementing compressed proof reading is worth the effort, particularly because of the exponential speedup over uncompressed proofs (in the worst case). The scheme is pretty simple to work with. Be sure to read appendix C of the metamath book, which lays it all out clearly.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c40d837c-6e17-4030-93c7-d72b35e817f5%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages