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/5f68266c-6603-4d2f-8be5-07950754d7b8n%40googlegroups.com.
tapeunifbound.json
Description: application/json
