New verifiers/parsers/community projects

137 views
Skip to first unread message

Thierry Arnoux

unread,
May 31, 2022, 1:17:29 AM5/31/22
to meta...@googlegroups.com

Hi all,

I notice there are several independent Metamath parser/verifiers in the making these days:

  • Anthony Barlett recently announced his Typescript verifier `checkmm-ts`,
  • Glauco is writing a Typescript program / VsCode extension,
  • Benoît is writing a lexer/parser,
  • Mario and I have been working for a while on `metamath-knife`, and I'm working on a VsCode extension for Metamath.
  • There are laudable efforts to maintain and extend `metamath-exe` (Wolf) and `mmverify.py` (Benoît)

On one hand that's a sign of a vibrant community and that's very good. On the other hand these are fragmented efforts (to paraphrase Mario) and we might achieve more if we were all working on a single project.

There is of course a cost for team work, as we need to agree on a direction and design choices, and coordinate efforts. This also means sometimes making concessions, which is never easy. GitHub is a wonderful tool which can help a lot here.

Personally I know the time I can spend on Metamath is limited, so I want to make it count - and like everyone I also want to have fun!

My questions to the community are:

  • Does anyone else wish to join forces and work more together on a common project rather on "competing" ones?
  • What would the right direction be for that? Which steps shall we take?
  • I followed Mario's call to work in Rust, I think technically it's a good choice. That language is growing in popularity, however it is still not as popular as e.g. Python, JS/TS, C++ or java, which pretty much every programmer touched. Did that choice exclude too many?
  • What was the rationale for you guys to start a new project rather than join an existing one? Are those existing project not well-documented enough? Is it too daunting to learn about the existing code base? Are you missing some clear "good first task" as GitHub calls them? Are the working environment of other projects not welcoming enough? Do you think they are not going to the right direction? Are there no other projects advanced enough to have a critical mass worth joining? Or is simply the challenge to do things alone stronger and more appealing?


As far as the project I've chosen to work on, the goal with `metamath-knife` and the Metamath VsCode Extension would be to provide a feature-rich proof assistant in VsCode just like Lean or MMJ2, or at least provide in VsCode the functionalities I had in my Eclipse plugin (I made a video about that). I've learned Rust as it was the programming language suggested by Mario and because `metamath-knife` was seen as a "new community verifier".

All work-in-progress is in GitHub and external contributions are of course welcome, though only Mario and I are contributing.

I'd love to learn more about other projects (Benoît, Glauco) even though we discussed a bit directly: what are your goals/aspirations? Would you welcome external contributions?

BR,
_
Thierry


Benoit

unread,
May 31, 2022, 6:52:53 AM5/31/22
to Metamath
Hi Thierry,

Thanks for this summary.  I agree with your remarks, I'll try to answer some of your questions in my case, and I'd be glad to hear others' answers too.

I remember I was pretty frustrated myself, a year ago or two, when seeing independent efforts in different directions, while, as a user, I would have prefered everyone to work on mmj2 (the most promising project at the time) to improve it.  As for me, I could diffcultly make useful contributions in large programs written in C/C++, Java or Rust, since I'm not proficient enough in these languages, at least of the moment.  My in-progress verifier (it does verify proofs, now!) is in OCaml, and one of its goals is also for my own learning (I remember I had mentioned OCaml in the "community verifier" thread, but it didn't catch on, and that's fine).  I also recently improved mmverify.py (type annotations, 4x speedup from which every CI run in metamath/set.mm now benefits) in Python (thanks for your reviews!) to try and contribute to the community.

All in all, I think it is important to have our most seasoned programmers focus on the most promising tool, which is metamath-knife (and your VSCode extension).  So I'm glad to see you and Mario work on it, and I recommend every experienced programmer to join you.  When I feel more confident in Rust, I'll try and contribute too.  I think that having begun with a smaller verifier in a language I'm more confident with did not waste my time but on the contrary is helping me reach that goal.

In the meantime, having smaller projects in other languages can generate new ideas (I'm mostly thinking of frontend ideas here: interfaces and visualization, search tools...).  What is important, is that, even if these are independent projects, they are not "competing" and they should share ideas as much as possible, and ideally also share their code.  As for me, I hope to be able to put my project soon on Github, and to share ideas with another project in OCaml by Philip White (https://groups.google.com/g/metamath/c/qIHf2h0fxbA), and beyond.

Benoît

Mario Carneiro

unread,
May 31, 2022, 7:01:28 AM5/31/22
to metamath
I think metamath-knife has shown itself to be pretty good for metamath-related data exploration, it is a lot easier to use as a library than anything else right now (usually you would have to take a verifier and modify it if you wanted to get information out). metamath-exe has probably historically been the way to do data exploration but all such exploration has been done purely through expanding the code itself and almost exclusively by Norm.

If you would prefer to do your data exploration in another language, I think we should try to set up bindings for mm-knife to OCaml et al. From what I can tell it's technically not too difficult, it just needs a place to live and a bit of maintenance.

It would also be good to start collecting ideas for what kind of data exploration is interesting and make it easier to do those things in rust as well.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b29a801b-a1b7-480b-b348-7c67ae5ca456n%40googlegroups.com.

Glauco

unread,
May 31, 2022, 12:50:52 PM5/31/22
to Metamath
Hi Thierry,

thanks for this useful thread.

As Benoit wrote, I would have also preferred everyone to work on mmj2. But when I myself tried to contribute, I always run into some dependency / "java version" issue.

When it became clear that a Language Server was the way to go, I settled on TypeScript for a number of reasons:

- I would have not been able to contribute to the Rust project, because I didn't have a good enough theoretical background: I've always been kind of a "mmj2 user", it simply was a tool for me to write bulletproof proofs (I once read an "old" version of the Metamath book, but back then I was a complete newbie and I didn't get lots of details)

- now that I've written my own parsers, verifiers, generator for theory specific grammars, unifiers (well... still working out this last one...) I can at least understand what you are doing with metamath-knife :-)

- my first attempt was with dotnet (the framework I prefer), and the parser / verifier was pretty good and fast, but as soon as I tried to work on the Language Server, as always, I stumbled against version conflicts between the Language Server SDKs I found on examples and the current dotnet version

- then I checked the list of existing Language Server Implementations
https://microsoft.github.io/language-server-protocol/implementors/servers/
and (if I remember well) there were 49 TypeScript implementations, (dotnet was the second most popular) and 3 Rust implementations
Then I looked at the LSP SDKs:
https://microsoft.github.io/language-server-protocol/implementors/sdks/
If you compare the TypeScript LSP SDK
https://github.com/Microsoft/vscode-languageserver-node
to the SDKs for the other platforms, you get an idea of how well maintained the TypeScript LSP SDK is.
And the TypeScript's SDK is used (for examples) in the LSP spec

- I did not want additional dependencies. If you use VSCode, you already have Node.js installed, and you don't need to install (the right version of) anything else. When I tried Thierry's metamath-vspa (it's supercool!) I immediately run into a RUST language server version issue (I'm sure the final version will not have this kind of problems, for the final user; but for contributors I guess it will always be a problem)

I'm not sure TypeScript will have the speed needed to be a smart enough Proof Assistant.
If my little LS settles down, I'll be more than happy to share ideas / features with the Rust LS Repo and contribute to the Community Verifier (as I wrote, now I have a better understanding of the underlying framework).

The flip side, is that in the last few months I had no more time to spend on new proofs and my mmj2 muscle memory is a bit rusty. I hope it pays out in the long run.

BR
Glauco

Antony Bartlett

unread,
May 31, 2022, 1:14:16 PM5/31/22
to meta...@googlegroups.com

Thierry writes:
> Anthony Barlett recently announced his Typescript verifier `checkmm-ts`,
> Does anyone else wish to join forces and work more together on a common project rather on "competing" ones?

I ported checkmm.cpp to TypeScript, yes.  I think it's important to make a distinction between a port and a new verifier, for reasons both good and bad.  A port is good because it doesn't add to the pile of fragmented efforts, and bad because it doesn't add to our overall confidence in Metamath which is in part derived from having multiple heterogeneous verifiers.  It's a pity it probably can't be counted as my having "joined forces" with the original author, Eric Schmidt.

Now that I have what I wanted, which is a verifier that runs on the JavaScript platform which I understand and find fun to hack around with, I'll probably be doing that for a while.  I am definitely up for other JavaScript platform code I can hack around with and potentially contribute to.  As such I am looking forward to seeing Glauco's verifier project.

It's no secret I have also played around with WASM builds of both metamath.exe and metamath-knife.  I think I drifted away from it because I'm afraid it feels more like "work" than "fun" to interact with two different programming languages and the interface between them.  Sorry to whoever that may disappoint.  Maybe if others have success there I'll follow their example eventually.

    Best regards,

        Antony



--
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 metamath+u...@googlegroups.com.

Philip White

unread,
May 31, 2022, 5:40:51 PM5/31/22
to meta...@googlegroups.com
I also have been working on a verifier, which is at
https://git.sr.ht/~philipwhite/mmweb, if anyone is interested. The
implementation includes a CLI for verifying files, but the main point
of the parser/verifier is to power a web UI, which I am currently
hosting at https://trailingwhite.space/proofs/ if you want to take a
look (it downloads set.mm on page load, which takes several seconds on
my connection, but it gets cached by the browser so that future page
loads are faster). All the design decisions are aimed at enabling the
web UI to be as good as possible.

One reason I starting working on my own verifier instead of
contributing to a different one is that I thought it would be a fun
project with a limited enough scope that I could finish it pretty
quickly. I picked OCaml because that is that language I like best; the
goal wasn't to make the version that everyone should use.

After I got to the point where the verifier worked well enough, I
started thinking about interesting things that I could do with such a
library, and the idea of an interesting web UI came up. At this point,
I have to answer the question, "why not switch to using a more hardcore
and battle-tested library like metamath-knife?" I can think of a lot
answers to this:

- Using a thing that I wrote and that nobody depends on means that I
can change it to fit my needs whenever I want, and without asking
anyone else.
- It wouldn't at all surprise me if a general-purpose API is difficult
to make suitable for web user interfaces, and in particular that type
of user interface code that I write. Bonsai, the library I am using,
combine both the virtual-dom approach popularized by React, and also
a library called incremental, which preserves work from previous
frames whenever it can. To make the incremental library happy, it's a
good thing to use persistent data structures and make updates in a
way that shares as much memory structure as possible, since that will
allow the incremental library to short-circuit computations that it
has already done. However, this approach seems awful if your goal is
to make a verifier that goes as fast as possible over the entire file.
- My build can be all in one language, and I don't have to worry about
how to link Rust and OCaml together. Maybe it's not that hard to "get
it to work", but polyglot systems are always at least a little less
convenient; for instance, you only get to support the intersection of
the systems that all the languages support. In my case, I think
binding OCaml to Rust and making it work in the browser seems like a
not fun situation.

I admit it would be a shame if lots of people did a bunch of redundant
work, and then we end up with a bunch of different verifiers with the
same feature-set. However, if what's happening is that if a bunch of
people are writing verifiers so that they can then explore some
interesting ideas on top of it, that seems like a great situation to
me.

Haskell was the result of lots of people focusing their efforts
together to do research on lazy functional programming (I think). This
seems like a big win because decent programming languages take a while
to build, so it helps a lot if researchers have an already built
language as a starting point.

In comparison, metamath verifiers are stupid easy to write. (I don't
mean your stupid if you can't make one, but that it's much much easier
to make one than to make a programming language compiler). In my
estimation, at this point, if everybody exploring interesting ideas
were working on the same codebase, it could be rather inefficient.
Eventually, once ideas mature, it makes sense to me to think about how
to combine them all into one system, but now feels too early.

To clarify, what I really mean is that if you like Rust and
metamath-knife matches closely enough with a thing your working on,
then that's a good project to work with. However, if, like me, you
don't really like Rust (it's fine, I just don't really want do
low-level programming), or you're building a system that has
incompatible goals, then go off and do your own thing (or maybe
collaborate with people who are going in the same direction).
> >> - Anthony Barlett recently announced his Typescript verifier
> >> `checkmm-ts`,
> >> - Glauco is writing a Typescript program / VsCode extension,
> >> - Benoît is writing a lexer/parser,
> >> - Mario and I have been working for a while on
> >> `metamath-knife`, and I'm working on a VsCode extension for
> >> Metamath.
> >> - There are laudable efforts to maintain and extend
> >> `metamath-exe` (Wolf) and `mmverify.py` (Benoît)
> >>
> >> On one hand that's a sign of a vibrant community and that's very
> >> good. On the other hand these are fragmented efforts (to
> >> paraphrase Mario) and we might achieve more if we were all working
> >> on a single project.
> >>
> >> There is of course a cost for team work, as we need to agree on a
> >> direction and design choices, and coordinate efforts. This also
> >> means sometimes making concessions, which is never easy. GitHub is
> >> a wonderful tool which can help a lot here.
> >>
> >> Personally I know the time I can spend on Metamath is limited, so
> >> I want to make it count - and like everyone I also want to have
> >> fun!
> >>
> >> My questions to the community are:
> >>
> >> - Does anyone else wish to join forces and work more together
> >> on a common project rather on "competing" ones?
> >> - What would the right direction be for that? Which steps shall
> >> we take?
> >> - I followed Mario's call to work in Rust, I think technically
> >> it's a good choice. That language is growing in popularity,
> >> however it is still not as popular as e.g. Python, JS/TS, C++ or
> >> java, which pretty much every programmer touched. Did that choice
> >> exclude too many?
> >> - What was the rationale for you guys to start a new project
> > <https://groups.google.com/d/msgid/metamath/b29a801b-a1b7-480b-b348-7c67ae5ca456n%40googlegroups.com?utm_medium=email&utm_source=footer>
> > .
> >
>

Mario Carneiro

unread,
May 31, 2022, 6:32:10 PM5/31/22
to metamath
On Tue, May 31, 2022 at 5:40 PM 'Philip White' via Metamath <meta...@googlegroups.com> wrote:
I also have been working on a verifier, which is at
https://git.sr.ht/~philipwhite/mmweb, if anyone is interested. The
implementation includes a CLI for verifying files, but the main point
of the parser/verifier is to power a web UI, which I am currently
hosting at https://trailingwhite.space/proofs/ if you want to take a
look (it downloads set.mm on page load, which takes several seconds on
my connection, but it gets cached by the browser so that future page
loads are faster). All the design decisions are aimed at enabling the
web UI to be as good as possible.

FYI: I tried loading the page, I get "Loaded N" where N rapidly counts up to 42869 and then nothing happens. This happens even after a reload, set.txt is cached so that doesn't seem to be the issue.

One reason I starting working on my own verifier instead of
contributing to a different one is that I thought it would be a fun
project with a limited enough scope that I could finish it pretty
quickly. I picked OCaml because that is that language I like best; the
goal wasn't to make the version that everyone should use.

After I got to the point where the verifier worked well enough, I
started thinking about interesting things that I could do with such a
library, and the idea of an interesting web UI came up. At this point,
I have to answer the question, "why not switch to using a more hardcore
and battle-tested library like metamath-knife?" I can think of a lot
answers to this:

- Using a thing that I wrote and that nobody depends on means that I
  can change it to fit my needs whenever I want, and without asking
  anyone else.

This kind of approach is fine for toy projects but for 'real' projects that you want to be used by the community this is not-invented-here syndrome. Even if you don't want to write rust code, one thing you can do is document your implementation strategy and feature set so that the code can be ported by others.
 
- It wouldn't at all surprise me if a general-purpose API is difficult
  to make suitable for web user interfaces, and in particular that type
  of user interface code that I write. Bonsai, the library I am using,
  combine both the virtual-dom approach popularized by React, and also
  a library called incremental, which preserves work from previous
  frames whenever it can. To make the incremental library happy, it's a
  good thing to use persistent data structures and make updates in a
  way that shares as much memory structure as possible, since that will
  allow the incremental library to short-circuit computations that it
  has already done. However, this approach seems awful if your goal is
  to make a verifier that goes as fast as possible over the entire file.

I think this opinion is formed from an incorrect guess of how things are done in mm-knife, if you are talking about that. Verifiers are generally written as you say, but proof assistants have to have a more incremental view of things, and mm-knife is the only proof assistant that actually has incrementality built in (even mmj2 and MM-PA don't really support incremental updates).

- My build can be all in one language, and I don't have to worry about
  how to link Rust and OCaml together. Maybe it's not that hard to "get
  it to work", but polyglot systems are always at least a little less
  convenient; for instance, you only get to support the intersection of
  the systems that all the languages support.

If you are compiling to web assembly, I don't think the system support really matters, you are ultimately constrained by the browser in the end. Besides, I don't think target support is an issue these days no matter what language you choose.
 
In my case, I think
  binding OCaml to Rust and making it work in the browser seems like a
  not fun situation.

Interestingly, if you are using web assembly (EDIT: or compiling to javascript, if the *.bc.js files are any indication), you might not even need to link them together directly, since they can both just separately talk to javascript.
 
I admit it would be a shame if lots of people did a bunch of redundant
work, and then we end up with a bunch of different verifiers with the
same feature-set.

Yes, that is exactly the trend I'm worried about. An mm-knife web UI is definitely coming; I think sorear had a proof of concept of this way back when smm3 was first introduced.
 
However, if what's happening is that if a bunch of
people are writing verifiers so that they can then explore some
interesting ideas on top of it, that seems like a great situation to
me.

There is a big difference between proof of concept and production tool. I *strongly* recommend centralizing efforts for the latter, and while it's fine to do the former in any language / project, I think that it is easy to start dreaming bigger and planning for more users, adding more features, and sinking a ton of time into something that ultimately leads to fragmentation.
 
Haskell was the result of lots of people focusing their efforts
together to do research on lazy functional programming (I think). This
seems like a big win because decent programming languages take a while
to build, so it helps a lot if researchers have an already built
language as a starting point.

In comparison, metamath verifiers are stupid easy to write. (I don't
mean your stupid if you can't make one, but that it's much much easier
to make one than to make a programming language compiler).

Metamath *verifiers* are easy to write, but metamath *proof assistants* not so much. I think the need for centralizing our fairly small pool of manpower is because the proof assistant-styled features are not nearly powerful enough in any system except to some extent mmj2 and MM-PA, both of which are severely hampered by losing their principal architect / maintainer.
 
In my
estimation, at this point, if everybody exploring interesting ideas
were working on the same codebase, it could be rather inefficient.
Eventually, once ideas mature, it makes sense to me to think about how
to combine them all into one system, but now feels too early.

To clarify, what I really mean is that if you like Rust and
metamath-knife matches closely enough with a thing your working on,
then that's a good project to work with. However, if, like me, you
don't really like Rust (it's fine, I just don't really want do
low-level programming),

I shouldn't get into this too much, but Rust is not really that low level. It is actually pretty comparable to OCaml in its feature set (it was literally derived from OCaml, among other things, and the original rust compiler was written in OCaml) .

But language wars are bound to happen no matter what choice you make. There aren't too many language choices that are fast enough for doing set.mm-scale work quickly enough and also aren't too low level so that "user code" can be written on top for things like proof automation and UI work.

Mario

Philip White

unread,
May 31, 2022, 7:43:27 PM5/31/22
to meta...@googlegroups.com
> FYI: I tried loading the page, I get "Loaded N" where N rapidly
> counts up to 42869 and then nothing happens. This happens even after
> a reload, set.txt is cached so that doesn't seem to be the issue.

Yup. The text above the loading count gives you the keyboard shortcuts
for doing anything. I know it's a terribly undiscoverable UI at the
moment. The description wasn't there until an hour or two ago when I
added that so it would meet the bare minimum of sharability. Anyway, if
the description doesn't help, just press the forward slash key, and
a fuzzy-finder window should pop up that you can search through all the
assertion labels that have been loaded.

> This kind of approach is fine for toy projects but for 'real'
> projects that you want to be used by the community this is
> not-invented-here syndrome. Even if you don't want to write rust
> code, one thing you can do is document your implementation strategy
> and feature set so that the code can be ported by others.

I agree that it's a good idea to document the interesting parts of the
project so that other efforts can benefit as well. Some of my
motivation is intentionally NIH, since making things helps me learn how
they work and I also find using libraries that I've written more fun
than using libraries other people have written. I disagree that
building a new library when one already exists is always bad idea; if
you don't think that either, than maybe we only disagree on the
criteria of when to do it. Anyway, that's a much larger debate that
doesn't need to be settled here. I'm just answering the original
question of why I would work on a new project instead of contributing
to an existing one.

Maybe worth mentioning is that I haven't built *everything* from
scratch. I'm using a lot of existing OCaml libraries that I'm not that
interested in building myself (or else I already have and concluded
that my version was worse than the existing one).

> I think this opinion is formed from an incorrect guess of how things
> are done in mm-knife, if you are talking about that. Verifiers are
> generally written as you say, but proof assistants have to have a
> more incremental view of things, and mm-knife is the only proof
> assistant that actually has incrementality built in (even mmj2 and
> MM-PA don't really support incremental updates).

Interesting, sounds like I'm mistaken. The incrementality I'm taking
about is pretty pervasive. If you can figure out how the demo I linked
works, then you'll be able to step forward and backward through proofs
and see the stack and heap growing and shrinking as the steps are
executed. The stack and heap are represented with immutable maps that
share most of their structure between each step so that you can you
step forward with minimal recomputation of the virtual-dom tree; that
is, you only need to compute the newly added items to the stack,
instead of recomputing the whole page again.

Does mm-knife have incrementality during the execution of a single
proof? I could be wrong, but my approach sounds like it would not
achieve the lightning speeds that I've heard mm-knife is capable of. In
contrast, my verifier takes about 13 seconds to verify set.mm.

There's an argument to be made that virtual-dom + persistent data
structures + all these other incrementality abstractions +
js_of_ocaml's slow compilation scheme are making my program more
complicated and slow. Maybe if I were to just do DOM manipulations it
would be faster and less code. Maybe, but I'm skeptical, and I also
don't think I would enjoy working on it as much, and I would probably
write more bugs.

> If you are compiling to web assembly, I don't think the system support
> really matters, you are ultimately constrained by the browser in the
> end. Besides, I don't think target support is an issue these days no
> matter what language you choose.
>
> Interestingly, if you are using web assembly (EDIT: or compiling to
> javascript, if the *.bc.js files are any indication), you might not
> even need to link them together directly, since they can both just
> separately talk to javascript.

Yeah, that's right. I'm using js_of_ocaml, which translates the bytecode
output of the ocaml compiler into javascript. I'm sure you're right
that it could be done. I would still contend that having bindings is
inconvenient because you have to think about how your language's
runtime will think about different pieces of data. Like, you probably
can't define a variant type in Rust and have it be translated to a
variant type in OCaml (unless you write that marshalling code yourself).

> There is a big difference between proof of concept and production
> tool. I *strongly* recommend centralizing efforts for the latter, and
> while it's fine to do the former in any language / project, I think
> that it is easy to start dreaming bigger and planning for more users,
> adding more features, and sinking a ton of time into something that
> ultimately leads to fragmentation.

I agree with this, mostly. I think what I am saying is that proof of
concepts are a fine reason for fragmentation, and then at some point a
"rebalance" operation should happen where the ideas get put into one
tool. Obviously it's great if those ideas get put into the same tool
from the beginning, but I could also see that slowing down projects
where the author wants more freedom to experiment than the project
provides.

> Metamath *verifiers* are easy to write, but metamath *proof
> assistants* not so much. I think the need for centralizing our fairly
> small pool of manpower is because the proof assistant-styled features
> are not nearly powerful enough in any system except to some extent
> mmj2 and MM-PA, both of which are severely hampered by losing their
> principal architect / maintainer.

Fair point, although all the "fracturing" that's been mentioned seems
to be about the proliferation of verifiers, and not proof assistants.
My experiment is currently just in the direction of an interface for
visualization and exploration, which I *think* is orthogonal to
building a proof assistant? I do eventually want to build a proof
assistant into this, though.

> Rust vs. OCaml

As fun as language wars are...no need.

- Philip

Mario Carneiro

unread,
May 31, 2022, 8:34:25 PM5/31/22
to metamath
On Tue, May 31, 2022 at 7:43 PM 'Philip White' via Metamath <meta...@googlegroups.com> wrote:
> FYI: I tried loading the page, I get "Loaded N" where N rapidly
> counts up to 42869 and then nothing happens. This happens even after
> a reload, set.txt is cached so that doesn't seem to be the issue.

Yup. The text above the loading count gives you the keyboard shortcuts
for doing anything. I know it's a terribly undiscoverable UI at the
moment. The description wasn't there until an hour or two ago when I
added that so it would meet the bare minimum of sharability. Anyway, if
the description doesn't help, just press the forward slash key, and
a fuzzy-finder window should pop up that you can search through all the
assertion labels that have been loaded.

Thanks, I got the basic functionality working. A few more bug reports: I haven't been able to figure out any conditions under which the (shift-)hjkl buttons do anything; and the fuzzy finder does not prioritize exact matches which makes it difficult to jump to specific theorems.
 
> This kind of approach is fine for toy projects but for 'real'
> projects that you want to be used by the community this is
> not-invented-here syndrome. Even if you don't want to write rust
> code, one thing you can do is document your implementation strategy
> and feature set so that the code can be ported by others.

I agree that it's a good idea to document the interesting parts of the
project so that other efforts can benefit as well. Some of my
motivation is intentionally NIH, since making things helps me learn how
they work and I also find using libraries that I've written more fun
than using libraries other people have written. I disagree that
building a new library when one already exists is always bad idea; if
you don't think that either, than maybe we only disagree on the
criteria of when to do it.

Right, I have nothing against writing something new just so that you can understand it (I do that all the time). But you do have to watch out for potential long term time sinks because if it becomes a proper project that multiple people put time into then we collectively just end up getting half as much done with respect to the big league proof assistants.
 
Interesting, sounds like I'm mistaken. The incrementality I'm taking
about is pretty pervasive. If you can figure out how the demo I linked
works, then you'll be able to step forward and backward through proofs
and see the stack and heap growing and shrinking as the steps are
executed. The stack and heap are represented with immutable maps that
share most of their structure between each step so that you can you
step forward with minimal recomputation of the virtual-dom tree; that
is, you only need to compute the newly added items to the stack,
instead of recomputing the whole page again.

Does mm-knife have incrementality during the execution of a single
proof? I could be wrong, but my approach sounds like it would not
achieve the lightning speeds that I've heard mm-knife is capable of. In
contrast, my verifier takes about 13 seconds to verify set.mm.

You need to choose some clever data structures in order to support both very fast verification and incremental updates, but it does actually have this. (By the way, I don't know if your "rust is low level" impression might have been caused by reading the mm-knife code base, but there are some tricks in there that are pretty low level performance optimizations based on actual profiling. Rust code doesn't have to look like that and luckily it is confined to just a few core data structures and mostly hidden behind an API barrier for "regular" code not on the verification hot path.)

Regarding incrementality during execution of a single proof, that's up to you. The way you step through a proof is actually user-(of-library)-configurable, and I would generally expect a UI to implement its own data structures which support the required stepping operations without moving a lot of data.

Personally, I wouldn't try to do this with a UI framework at all. General purpose virtual-dom diffing is just objectively worse from a performance standpoint. I would just have stepping send change events that push and pop things from the stack and/or heap. (But also, this is not at all the bottleneck - you can do pretty much anything you want in this space and your debugger will be performant enough.)
 
There's an argument to be made that virtual-dom + persistent data
structures + all these other incrementality abstractions +
js_of_ocaml's slow compilation scheme are making my program more
complicated and slow. Maybe if I were to just do DOM manipulations it
would be faster and less code. Maybe, but I'm skeptical, and I also
don't think I would enjoy working on it as much, and I would probably
write more bugs.

There's nothing wrong with trying out alternative ideas to see if they work. It sucks when you put a bunch of effort into a performance optimization only to find out after profiling that it is a negative win. (I've been there.) In your setting (OCaml + js_of_ocaml + virtual-dom), it might very well be that incrementality and persistent data structures is cheaper than not, and I can certainly believe that it's easier to get correct, especially if the virtual dom implementation is outsourced to a good library. All I can say is, don't forget to actually measure.
 
> If you are compiling to web assembly, I don't think the system support
> really matters, you are ultimately constrained by the browser in the
> end. Besides, I don't think target support is an issue these days no
> matter what language you choose.
>
> Interestingly, if you are using web assembly (EDIT: or compiling to
> javascript, if the *.bc.js files are any indication), you might not
> even need to link them together directly, since they can both just
> separately talk to javascript.

Yeah, that's right. I'm using js_of_ocaml, which translates the bytecode
output of the ocaml compiler into javascript. I'm sure you're right
that it could be done. I would still contend that having bindings is
inconvenient because you have to think about how your language's
runtime will think about different pieces of data. Like, you probably
can't define a variant type in Rust and have it be translated to a
variant type in OCaml (unless you write that marshalling code yourself).

Actually you can: I haven't used the 'ocaml' rust crate but it seems to have some pretty great support for marshalling complex types, including variant types: https://docs.rs/ocaml-interop/0.8.8/ocaml_interop/macro.impl_to_ocaml_variant.html . The usual way would be to put a #[derive(FromValue, ToValue)] attribute on the type definition, like shown in the first example here: https://docs.rs/ocaml/latest/ocaml/index.html .

If the communication was indirect via webassembly it probably wouldn't be as nice as this though, since you would have to marshal your types into JS and from there to rust (so it would be using a WASM <-> Rust bindgen instead). Still, you could probably encode variant types to JSON and get essentially fully automatic FFI for complex types, as long as both ends have the same conventions for encoding (and I know the rust deserializer is configurable to other conventions even then).

The worst part is really not the communication itself (these bridges are pretty well developed) but rather the overhead of all the conversions. It's best if you can avoid sending large data across languages, and keeping things in one house eliminates that cost.

> Metamath *verifiers* are easy to write, but metamath *proof
> assistants* not so much. I think the need for centralizing our fairly
> small pool of manpower is because the proof assistant-styled features
> are not nearly powerful enough in any system except to some extent
> mmj2 and MM-PA, both of which are severely hampered by losing their
> principal architect / maintainer.

Fair point, although all the "fracturing" that's been mentioned seems
to be about the proliferation of verifiers, and not proof assistants.

I don't think proliferation of verifiers is a problem at all. I would like to see metamath verifiers on Rosetta Code and written in 200 languages. It's a weekend project so it doesn't have the same risks unless you want to start adding fancy features like math parsing or markup rendering, or anything that is not just read-only on the mm file.

My experiment is currently just in the direction of an interface for
visualization and exploration, which I *think* is orthogonal to
building a proof assistant?

Having seen what the program does now, and assuming that the debugger thing is the end goal and not just one part of a complex interface (which is probably the direction you are thinking ATM), I think it would be interesting to try implementing it in a way so that it could fit on top of the usual HTML theorem presentation, and in particular without having the entirety of set.mm loaded. I would probably do that by implementing the debugger in JS (possibly compiled from another language), and then putting the data required for that one theorem on the page and a precompiled data structure with the formatting information in a separate file.

Mario

Jim Kingdon

unread,
Jun 1, 2022, 1:15:53 AM6/1/22
to meta...@googlegroups.com
On 5/31/22 17:34, Mario Carneiro wrote:

> I don't think proliferation of verifiers is a problem at all. I would
> like to see metamath verifiers on Rosetta Code and written in 200
> languages. It's a weekend project so it doesn't have the same risks
> unless you want to start adding fancy features like math parsing or
> markup rendering, or anything that is not just read-only on the mm file.

Hmm, by that criteria a second implementation of the definition checker
would seem to be "fancy".

Which is too bad, in the sense that it is (at least to my way of
thinking) part of the "kernel" in the sense of being needed to confirm
soundness.

I suppose this is another case of "we won't run out of projects to work on".

Mario Carneiro

unread,
Jun 1, 2022, 1:19:03 AM6/1/22
to metamath
On Wed, Jun 1, 2022 at 1:15 AM Jim Kingdon <kin...@panix.com> wrote:
On 5/31/22 17:34, Mario Carneiro wrote:

> I don't think proliferation of verifiers is a problem at all. I would
> like to see metamath verifiers on Rosetta Code and written in 200
> languages. It's a weekend project so it doesn't have the same risks
> unless you want to start adding fancy features like math parsing or
> markup rendering, or anything that is not just read-only on the mm file.

Hmm, by that criteria a second implementation of the definition checker
would seem to be "fancy".

Which is too bad, in the sense that it is (at least to my way of
thinking) part of the "kernel" in the sense of being needed to confirm
soundness.

It is fancy, and it is too bad that this is the case. If you recall this is one of the reasons I started working on MM0, the definition checker is way too important to be bolted on the side like it is in metamath.

Mario

Raph Levien

unread,
Jun 1, 2022, 1:25:02 AM6/1/22
to Metamath Mailing List
I'm sure you meant to say, "this is one of the reasons Raph started working on Ghilbert, then I shamelessly copied that approach for MM0."

:)

R


--
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 metamath+u...@googlegroups.com.

Philip White

unread,
Jun 1, 2022, 5:32:18 PM6/1/22
to meta...@googlegroups.com
> Thanks, I got the basic functionality working. A few more bug
> reports: I haven't been able to figure out any conditions under which
> the (shift-)hjkl buttons do anything; and the fuzzy finder does not
> prioritize exact matches which makes it difficult to jump to specific
> theorems.

You have to add more than one assertion to the workspace before any of
the window manipulation commands do anything. This is because the
windows are arranged in a row of columns, and not in arbitrary
positions determined by the user. h and l move back forth through the
columns, and j and k move up and down in a particular column.

Prioritizing exact match is a good idea. The current sort is
alphabetical, but it would be great to use the actual FZF algorithm. I
also would like to add more information to the search box so that the
user doesn't just have to search through the mnemonics, which are to
brief to know what something is before selecting it. It would be nice to
search for "Axiom of Choice" and have the system show "ax-ac" at the
top. Maybe this could be accomplished by including the first sentence
of the attached comment?

> Regarding incrementality during execution of a single proof, that's
> up to you. The way you step through a proof is actually
> user-(of-library)-configurable, and I would generally expect a UI to
> implement its own data structures which support the required stepping
> operations without moving a lot of data.

Oh, that's quite interesting. I suppose I should actually look at the
mm-knife API at some point.

> Personally, I wouldn't try to do this with a UI framework at all.
> General purpose virtual-dom diffing is just objectively worse from a
> performance standpoint. I would just have stepping send change events
> that push and pop things from the stack and/or heap. (But also, this
> is not at all the bottleneck - you can do pretty much anything you
> want in this space and your debugger will be performant enough.)

The virtual-dom approach is slower than doing direct DOM manipulation
of the exact things that need to be changed, but I think it clearly
wins if you want to take the "compute your view with a pure function"
approach, since it will minimize the number of DOM mutations. That is,
I like the "view is a pure function" approach because it is pleasant
and seems to yield fewer bugs, so I also use a virtual-dom library
because it makes that approach feasible.

> Actually you can: I haven't used the 'ocaml' rust crate but it seems
> to have some pretty great support for marshalling complex types,
> including variant types:
> https://docs.rs/ocaml-interop/0.8.8/ocaml_interop/macro.impl_to_ocaml_variant.html
> . The usual way would be to put a #[derive(FromValue, ToValue)]
> attribute on the type definition, like shown in the first example
> here: https://docs.rs/ocaml/latest/ocaml/index.html .
>
> If the communication was indirect via webassembly it probably
> wouldn't be as nice as this though, since you would have to marshal
> your types into JS and from there to rust (so it would be using a
> WASM <-> Rust bindgen instead). Still, you could probably encode
> variant types to JSON and get essentially fully automatic FFI for
> complex types, as long as both ends have the same conventions for
> encoding (and I know the rust deserializer is configurable to other
> conventions even then).

That's pretty cool.

To elaborate a bit on the "Rust is too low-level for me" comment: what
I mean is that there is some syntactic overhead related to memory
management. My impression of Rust is driven by using it, actually; I
don't hate it, and I would 100% use it instead of C or C++. I'm aware
of some of the things that Rust has to make manual memory management
less error-prone and more convenient, but it doesn't make those
concerns go as close to zero as a GC.

Jon P

unread,
Jun 2, 2022, 7:13:35 AM6/2/22
to Metamath
Nice discussion. Three things I wanted to contribute if they're at all useful:

1. If anyone needs beta testing on a system then I'd be happy to play around with it and give, rather non-expert, feedback. I tried your system a little Philip, it was really cool to be able to see the stack and heap while the proof was in progress, that's new to me which is nice.

2. At some point I'd like to make a mini course for getting people into metamath, a few videos of explanation with some worksheets of problems to try to help newcomers find their way. Maybe when mm-knife has a VSCode extension would be a nice time to do this. I think making it smoother to get into the community can help with growth.

3. I used to work on an open source game called Thrive. We would put up posts (for free on places like reddit) showing off the game and asking if anyone wanted to contribute (again for free, as open source) and we would get a reasonable number of people. Is it worth appealing to Rust programmers, for example, who might not know so much about the metamath side but might be keen to help and be able to work on UI, web stuff, cross compatibility etc? If that's helpful I don't mind doing the legwork of writing the posts and finding appropriate places to put them (you have to be sensitive to subreddit posting rules etc).

Jim Kingdon

unread,
Jun 2, 2022, 9:52:53 AM6/2/22
to Jon P, Metamath


On June 2, 2022 4:13:35 AM PDT, Jon P <drjonp...@gmail.com> wrote:
>
>If that's helpful I don't mind doing the legwork of
>writing the posts and finding appropriate places to put them (you have to
>be sensitive to subreddit posting rules etc).

Well I love the idea and it sounds like you have some ideas for how to make it sound appealing (which is perhaps not as self evident as a game but which seems potentially doable for a group which is some flavor of technical).

Jon P

unread,
Jun 6, 2022, 6:00:56 PM6/6/22
to Metamath
Yeah so this is the sort of thing I would imagine, for perhaps the rust subreddit https://www.reddit.com/r/rust/ (after asking the mods if it's ok.) Not sure if it's a good idea, it's an example.

-----------

Hello Rustacians! 

metamath [link] is a project for creating computer checkable maths proofs. The means taking old fashioned pen and paper mathematical proofs and encoding them in such a way that they can be verified by machine, as some classic examples we have Pythagoras' theorem [link] and the irrationality of the square root of 2 [ink]. There are over 40,000 proofs in the database so far and growing, hopefully one day it can cover all of known mathematics.

There have also been some interesting projects to use AI to generate maths proofs, such as Open AIs gpt-f [link] and this AI assisted mathematics may well be the future.

Anyway what does this have to do with you? Our community is working on a new verifier and proof assistant called metamath-knife [link] and it's written in Rust. And there's a lot of Rust based stuff which we could really do some help with working on, for instance [not exactly sure what should go here?] creating a good web UI for it, implementing a VSCode extension and ...

The verifier is open source and we're an all volunteer community, so no money is involved. And so yeah if you're either interested in learning about the mathematical aspects or would be interested in poking around with the code and helping with some of the programming stuff come and say hi at our google group [link] or check out the github repo [link]. We have people who are very strong on the mathematical side so if you are only familiar with Rust that's still useful to us.

Computer readable / formally verified mathematics is extremely powerful and is a very young a promising field which has a lot to explore for anyone curious about the future of mathematics.

Thanks :)

Jim Kingdon

unread,
Jun 7, 2022, 3:37:21 PM6/7/22
to Jon P, Metamath
Seems sensible to me. I'm not sure I have any more insight than anyone else about whether it is a good idea, but I'm certainly in favor of encouraging new contributions as best we can.
Reply all
Reply to author
Forward
0 new messages