Re: [Metamath] Re: How to process dummylink?

[Mario Carneiro]

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.

On Thu, Dec 5, 2019 at 12:10 PM Tony  wrote:

> I found proof decompression to be easier to implement than I thought it
> would be. The hardest part was just understanding how it works.
>
> On Tuesday, December 3, 2019 at 3:32:07 PM UTC+1, Marko Grdinic 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+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/c40d837c-6e17-4030-93c7-d72b35e817f5%40googlegroups.com
> 
> .
>

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CAFXXJSsQyQfWNdj%3DJQSD-f6g_yV5YaiO1cEMiedpyfH5Fe2RwA%40mail.gmail.com.

Re: [Metamath] Re: How to process dummylink?

[David A. Wheeler]

On Tue, 3 Dec 2019 06:32:07 -0800 (PST), Marko Grdinic  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

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/E1icH20-0001ZO-6b%40rmmprod07.runbox.

Re: [Metamath] Re: How to process dummylink?

[Marko Grdinic]

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
>
> https://groups.google.com/forum/#!msg/metamath/Hey2L9f1ULk/vXMWVcI5DwAJ
>
> Can your verifier check demo0.mm yet? (
> https://github.com/david-a-wheeler/metamath-test/blob/master/demo0.mm)
>
> Best regards,
>
> Antony
>
>
> On Tue, Dec 3, 2019 at 2:32 PM Marko Grdinic  > 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 .
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/metamath/fbd4651b-9429-4ecb-96ae-db8ebbaa7431%40googlegroups.com
>>  
>> 
>> .
>>
>

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/a299c546-ecc3-4020-a199-139d2c00a2a7%40googlegroups.com.

Re: [Metamath] Re: How to process dummylink?

[Antony Bartlett]

Uncompressing the entire set.mm database was last discussed here

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

Can your verifier check demo0.mm yet? (
https://github.com/david-a-wheeler/metamath-test/blob/master/demo0.mm)

Best regards,

Antony


On Tue, Dec 3, 2019 at 2:32 PM Marko Grdinic  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+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/fbd4651b-9429-4ecb-96ae-db8ebbaa7431%40googlegroups.com
> 
> .
>

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CAJ48g%2BAJN4v1YnW%3DDxLB8dtLK_20%3DwgjBfXGcnhJHJ0_ro_rag%40mail.gmail.com.