`jscoq.js` is needed.

In scratchpad only.
Closes #326.

Instead of `.cjs`; enough with this nonsense.

This is not perfect but it works (and it is much faster).

For some reason I couldn't make `fflate-unzip` work with ESBuild, so
I've placed a copy and tweaked the exports.

We reorganize jsCoq's source code as to be more modular, in particular
we start to place backend files under the `backend` directoy, and
frontend files under `frontend`.

Code as it now does work, note however that still quite a bit of work
is needed. In particular, the headless frontend should get its own
directory, the coq-jslib directory should go away, use more types,
etc...

In `type="module"`, this has to be done explicitly.

Need to pass `backend` and `is_npm` properly now.

Need to pass `backend` and `is_npm` properly now.

Still, both don't fully work, needs more research as to witness what's
broken.

To avoid confusion, `ui-js/jscoq.js` has been renamed.
Also, a legacy-mode `jscoq-loader.js` that emulates the old behavior.

`JsCoq.load` should not return before the document is ready. Because then
the CSSs have not been applied yet.

So that it can be `import`ed.

Maybe we should squash the loader fixes to the previous commits.

Well not quite, the `dsp` dependency needs to be resolved.

MathJax added as an NPM dependency instead of using CDN.
(Because same-origin policy stuff.)

Allows for using Zulip playgrounds, a feature which redirects code
snippets to an online repl.

And immediately employed this feature in the sqrt_2 example.
The example now contains some hand-crafted prologue followed by the
coqdoc content.

`<kbd>` formatting and a hint for newcomers to look at the scratchpad icon.

`<kbd>` formatting and a hint for newcomers to look at the scratchpad icon.

Also generated symbols for the examples.

Filled in the links in the navbar, etc.
Added hover action to quick-start reference.

Added meaningful names to comparison lemmas.
Renamed module to `sqrt_2` so the import looks nicer on the landing page.

It is longer, yes, but perhaps easier to understand in prose.
Fixed indentation.

Allows multiple jobs to invoke the SDK in parallel. If the SDK is not installed,
the first to lock the file will carry out the install.

A bind-mount is too slow.
`sudo` is required to copy onto the volume.
The implementation is currently non-reentrant, so `-j1` is needed.

As subcommand `jscoq sdk`.

Included `index.html` and a `package.json` to show how to load
and run the resulting package.

Also added `playful.html`. (Which is a bit unrelated.)

Currently separate from the main cli, but for no good reason.
Should be a sub-command.

Made the example a little bit smaller by removing some unneeded
boilerplate.
(Possible thanks to Dune 3's `glob_files_rec`.)

Also, the example now showcases `group-theory` instead of Coqoban.
Mainly because we already have Coqoban as an addon.