> 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/b1405a43-cefe-4148-9de0-eee6ebc0cb9dn%40googlegroups.com.
tapeunifbound.mmp
Description: Binary data
