In January 2020 I had a case where ~idi was *not* removed after minimize 
had finished, see Github issue #1426. 
<https://github.com/metamath/set.mm/issues/1426>I performed minimize again 
today, and it seems that the new version 0.181 12-Feb-2020 of metamath.exe 
does not add ~idi anymore! Let's wait for the end of the current global 
minimization action if new cases come up.

Actually, there are currently 12 proofs in set.mm using ~idi (~dummylink is 
not used at all), but all of them are in mathboxes. They should be removed 
by our global minimization, shouldn't they?

On Saturday, February 15, 2020 at 3:37:39 AM UTC+1, Mario Carneiro wrote:
>
> It may minimize with the statement, then later minimize the statement 
> away. I wouldn't be worried unless "idi" appears in the minimized proof.
>
> On Fri, Feb 14, 2020 at 6:27 PM David A. Wheeler <dwhe...@dwheeler.com 
> <javascript:>> wrote:
>
>> I just took a quick look at job144.log as posted on:
>> https://dwheeler.com/temp/job144.log
>>
>> I noticed these... oddities:
>> Proof of "fourierdlem48" decreased from 18892 to 18864 bytes using 
>> "dummylink".
>> Proof of "fourierdlem48" decreased from 18864 to 18848 bytes using "idi".
>>
>> I didn't expect that. This is using Metamath Version 0.181 12-Feb-2020.
>> Is this expected behavior (and if so, why)?
>>
>> --- 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 meta...@googlegroups.com <javascript:>.
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/metamath/E1j2nAt-0005ZC-6n%40rmmprod07.runbox
>> .
>>
>

-- 
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/67fc66c7-33fc-452c-a0c7-e3b7ea6d1490%40googlegroups.com.

Reply via email to