search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
12 stars 5 forks source link

Generate shorter URLs (low priority) #109

Open david-a-wheeler opened 1 year ago

david-a-wheeler commented 1 year ago

The generated URLs for even simple proofs are long. I suspect there will be some system limit we eventually hit.

They shouldn't be so long. I suspect the problem is that they're not getting compressed before being converted. It also suspect the algorithm is really conservative on the symbols it generates for the URL.

It could add EditorCompressedState=... with a more compressed format.

expln commented 1 year ago

It is limited by GitHub. I found it experimentally - only about 5K characters in the editor state (description + vars + disjoints + all steps) may be shared via URLs without problems.

Additional info about encoding currently used in the URL (JFYI): Such URLs contain a Base64 encoded editor state. It may be decoded with many online Base64 decoders if for some reason a URL is not opened by mm-lamp but it is needed to see its content.

I agree the ability to compress editor state before encoding should be implemented too.

expln commented 1 year ago

I think the ability to download an editor state from some URL similarly how MM databases can be downloaded now may be useful either. In that case you will be able to store the editor state on, for example, Git Hub, and only put its URL inside of mm-lamp URL like editorStateUrl=...

david-a-wheeler commented 1 year ago

The ability to refer to an external URL would be very very awesome. It'd certainly make "click on this link" from within the guide easy to pull off.

That said, it's also awesome to be able to have the whole state embedded in the URL. It's especially useful when you're sharing partial state with someone.