> *Is there a changelog somewhere, by any chance?* Yes - https://github.com/expln/metamath-lamp/blob/develop/CHANGELOG.md
On Saturday, November 29, 2025 at 3:03:57 AM UTC+1 Ender Ting wrote: > > 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/c9ea38a5-5f49-4a9f-8863-b6e115d9304en%40googlegroups.com.
