The occasional temporary use of dummylink and idi during a 'minimize' run is normal, but they should always disappear from the proof by the end of the run.
I just responded to this on the issue page, which breaks down step by step what is going on and shows how to debug this. Sorry for the delay in answering the issue. I had a large number of emails that day and somehow this got overlooked. Norm On Saturday, February 15, 2020 at 2:31:38 AM UTC-5, Alexander van der Vekens wrote: > > 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]> >> 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]. >>> 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/0d7195ab-23cc-418e-92c1-d3b1436a618a%40googlegroups.com.
