> Please make sure you are using the latest version <https://expln.github.io/lamp/v31/index.html> for the moment.
I did not know there were multiple! Version 31 is indeed much faster than version 24 had been. (Is there a changelog somewhere, by any chance?) Thanks! - Ender пятница, 28 ноября 2025 г. в 23:43:23 UTC+3, [email protected]: > Hi Ender, > > *> It was also rough in Metamath Lamp online, which took around a > half-minute to unify statements on any change.* > > I imported that proof into mm-lamp and unification of all steps took about > 1 second for me. I thought maybe you changed the “Parentheses” setting on > the settings tab, because mm-lamp counts parentheses to make unification > faster. But even if I erase everything in the “Parentheses” setting, > unification takes not more than 3 seconds. So, I am not sure what is the > reason why mm-lamp works slow for you. If you are still using mm-lamp, can > you try to click “Restore default settings” on the Settings tab, then click > the “Apply changes” button, and then try to edit and unify the proof? Are > there any performance improvements after that? If you made some custom > intentional updates in the settings, you can use the incognito mode for > this experiment so as not to overwrite your custom updates in the settings. > In case you have only the mmp file with the proof, I attached a json file > with the same proof which you can import to mm-lamp. Please make sure you > are using the latest version <https://expln.github.io/lamp/v31/index.html> > for > the moment. Also, don’t you mind if I create an issue in mm-lamp’s github > repository and attach your proof there? > > Hi Marlo, > > Sorry for bringing up mm-lamp in the mmt1 thread. I haven't had a chance > to try mmt1 yet, because I'm not working with metamath proofs at the > moment, but I appreciate the work you're doing on it, and I'm looking > forward to seeing new features you add. > > - > Igor > > On Friday, November 28, 2025 at 2:26:48 PM UTC+1 Ender Ting wrote: > >> > I don't quite understand what you mean by that, could you elaborate >> further? >> >> Compressed proof references the prior theorems it uses; they are arranged >> to fill the line exactly (knapsack problem) whenever possible, and mmt1 >> does not do that. >> >> lamberte $p |- _e R 1 $= >> ( vy ceu c1 wbr cc cv ce cfv cmul co wceq wa wtru wb 1ex crp mpbir >> biimpi >> cmpt ccnv wcel copab epr elexi eqcom ax-1cn eqeltrrdi adantr simpr >> rpssre >> df-e ax-resscn sstri sselii eqeltrri mullidi eqtr4i oveq12d eqtr3id >> eqtrd >> cr fveq2d jca tbtru sylib eqid braba df-mpt breqi brcnv ) >> EFBGEFAHAIZVNJK >> See that all the lines have same length. >> >> > What kind of hardware are you running mmt1 on? >> >> Laptop, Linux, CPU: 6-core i5-11400H @ 2.70GHz, RAM: 40 GB. (There was >> plenty free RAM as well.) >> You may examine the file in question, attached to this email. (I've been >> revisiting that theorem-to-be for like a year, and haven't yet managed to >> plug in the last step. It was also rough in Metamath Lamp online, which >> took around a half-minute to unify statements on any change, thus my >> interest in mmt1.) >> >> Best wishes, >> Ender Ting >> пятница, 21 ноября 2025 г. в 22:25:47 UTC+3, [email protected]: >> >>> Hi Ender, >>> >>> On Saturday, November 15, 2025 at 6:03:33 PM UTC+1 Ender Ting wrote: >>> >>> as prev-theorem references are sorted in wrong order >>> >>> >>> I don't quite understand what you mean by that, could you elaborate >>> further? >>> >>> Using it with my proof-in-progress longer than 360 lines, though, is >>> rougher. Even text selection lags somehow (to the point it is faster to >>> delete individual characters instead of selecting a line and deleting it at >>> once). >>> >>> >>> That is strange. So far I haven't been able to get mmt1 to lag on my >>> machine. If you don't mind me asking: What kind of hardware are you running >>> mmt1 on? mmt1 shouldn't affect text selection in any way, so the only >>> reason I can come up with is that mmt1 might be using too much RAM. Is that >>> the case? And if you have VSCode installed: Does opening the same file in >>> VSCode also produce lag? Answering these questions should help me pin down >>> your performance issues. >>> >>> Best regards, >>> Marlo Bruder >>> >> -- 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 visit https://groups.google.com/d/msgid/metamath/bf457256-3be6-4317-9ceb-8fd941ba1693n%40googlegroups.com.
