-
Notifications
You must be signed in to change notification settings - Fork 18
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Use compression to shorten URLs #36
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -7,6 +7,7 @@ import { Menu } from './Navigation' | |
import { PreferencesContext } from './Popups/Settings' | ||
import { useWindowDimensions } from './utils/window_width' | ||
import LeanLogo from './assets/logo.svg' | ||
import LZString from 'lz-string'; | ||
|
||
import CodeMirror, { EditorView } from '@uiw/react-codemirror' | ||
|
||
|
@@ -26,6 +27,7 @@ interface UrlArgs { | |
project: string | null | ||
url: string | null | ||
code: string | null | ||
codez: string | null | ||
} | ||
|
||
/** | ||
|
@@ -286,7 +288,11 @@ function App() { | |
if (args.code) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The "code" argument is still supported so that old URLs continue to work. Loading a URL like that will cause the URL to be immediately replaced in the address bar with a codez URL (if the code is compressible -- see below.) There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I will update the docs after I merged your PR; the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Oh, that's cool! |
||
let _code = decodeURIComponent(args.code) | ||
setContent(_code) | ||
} else if (args.codez) { | ||
let _code = LZString.decompressFromBase64(args.codez); | ||
setContent(_code); | ||
} | ||
|
||
if (args.url) {setUrl(decodeURIComponent(args.url))} | ||
if (args.project && args.project != project) { | ||
console.log(`[Lean4web] setting project to ${args.project}`) | ||
|
@@ -320,18 +326,24 @@ function App() { | |
let _project = (project == 'mathlib-demo' ? null : project) | ||
if (code === contentFromUrl) { | ||
if (url !== null) { | ||
let args = {project: _project, url: encodeURIComponent(url), code: null} | ||
let args = {project: _project, url: encodeURIComponent(url), code: null, codez: null} | ||
history.replaceState(undefined, undefined!, formatArgs(args)) | ||
} else { | ||
let args = {project: _project, url: null, code: null} | ||
let args = {project: _project, url: null, code: null, codez: null} | ||
history.replaceState(undefined, undefined!, formatArgs(args)) | ||
} | ||
} else if (code === "") { | ||
let args = {project: _project, url: null, code: null} | ||
let args = {project: _project, url: null, code: null, codez: null} | ||
history.replaceState(undefined, undefined!, formatArgs(args)) | ||
} else { | ||
let args = {project: _project, url: null, code: fixedEncodeURIComponent(code)} | ||
history.replaceState(undefined, undefined!, formatArgs(args)) | ||
const compressed = LZString.compressToBase64(code).replace(/=*$/, ''); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Trimming trailing |
||
if(compressed.length < code.length) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I made this only use compression if its actually a win (see charts in PR description). For very small character counts it isn't always a win, although it also doesn't really matter anyway. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We talked in DM; the check here is biased against compression because There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Fixed in fa4342d |
||
let args = {project: _project, url: null, code: null, codez: compressed} | ||
history.replaceState(undefined, undefined!, formatArgs(args)) | ||
} else { | ||
let args = {project: _project, url: null, code: fixedEncodeURIComponent(code), codez: null} | ||
history.replaceState(undefined, undefined!, formatArgs(args)) | ||
} | ||
} | ||
}, [editor, project, code, contentFromUrl]) | ||
|
||
|
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This library has the MIT license.
I considered using
CompressionStream
with gzip but it only became supported in Safari last year. I figured it would be bad if some live URLs (generated by people with modern browsers) didn't work on browsers that have a non-trivial amount of users left.I came across lz-stream because it's used in sharplab.io, a C# REPL : https://github.com/ashmind/SharpLab/blob/078c4e2c5a790f6b7203401c2ec63de22913c0d1/source/WebApp/app/features/persistent-state/handlers/url.ts#L1
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Aside: sharplab does an extra thing it calls "pre-compression" where it replaces some common substrings with shorter ones (
@3
,@7
etc.) before sending it to this library: https://github.com/ashmind/SharpLab/blob/main/source/WebApp/app/features/persistent-state/handlers/url/precompressor.tsI did some quick checks and it wasn't a big deal. If you're interested I could get some actual data using the benchmark process I described in the PR description. The trade-off is extra complexity/.js size for a much smaller reduction in URL size.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you want to further optimise the algorithm, please feel free to do so, I'd happily merge it :)