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 <[email protected] > <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 [email protected] <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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/67fc66c7-33fc-452c-a0c7-e3b7ea6d1490%40googlegroups.com.
