> On Sun, Feb 19, 2023 at 2:19 PM David A. Wheeler
> wrote:
> My first choice when building a website, where it's easily achieved, is
> static rendering (statically-generated pages) where the most important data
> is visible without client-side JavaScript. Those are easily understood,
>
That's very much on my roadmap, but I had to start with .mm because I don't
believe the code for generating .mmp files exists on the JavaScript
platform yet. (Glauco's Yamma doesn't have it yet, and Igor's proof
assistant doesn't use them or save any intermediate format I'm aware of).
The
On Sun, Feb 19, 2023 at 1:05 PM Mario Carneiro wrote:
> I don't see those as competing goals at all. They play different roles:
> for browsing you would ideally have some server supplying only the required
> information to render a specific proof, and for a proof assistant (and to
> some extent
On Sun, Feb 19, 2023 at 2:19 PM David A. Wheeler
wrote:
> > While yes I agree that this would be much better done with
> metamath-knife than metamath-exe, I don't think there is a major concern
> here, or at least we can mostly mitigate the issues since this flow is
> extremely light on input
FYI: Our discussion topic seems to have broadened to discussing potential
future directions for the website, so I've changed the subject line to "Future
website directions". Its subject line was previously: "Re: [Metamath] Idea:
Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML
Oops, that was the wrong link, I meant to point to
https://www.mediawiki.org/wiki/Page_Previews . (I investigated how this
feature is implemented a while ago, with an eye for doing something similar
for theorem references.)
On Sun, Feb 19, 2023 at 1:05 PM Mario Carneiro wrote:
> I don't see
I don't see those as competing goals at all. They play different roles: for
browsing you would ideally have some server supplying only the required
information to render a specific proof, and for a proof assistant (and to
some extent a search tool as well) you want to have the whole database
On Sat, Feb 18, 2023 at 11:04 PM Mario Carneiro wrote:
> Even if you have a highly optimized mm verifier, you can't get around the
> fact that you need to send some 30 MB over the wire before you can do
> anything.
>
Just to recap a few things from other threads, back in November, Samuel
Goto
