Mario, do you have some more detail about this project to write (I'm quoting you from github) "a verifier that would satisfy all the constraints of the CI system in terms of capabilities: checking all the typesetting stuff, definition checking, and full verification as efficiently as possible"?Thanks in advance.Benoît
Whoa! And I'm already spoiled by what Leo is doing with Lean 4. The so small core language and vastly extensible parser with an entire automation library for building and proving formal systems using incremental compilation with plans for interactive compiler guidance are mind blowing. That's taking aside your own exciting MM0 work. And I only have that much time to learn about lots of things. I'm torn already :(
--
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/dc7550eb-9c0b-4953-93b5-1c9640b0ffd9n%40googlegroups.com.
Regarding writing an editor. I agree it's a big task and hard to do right. That said, it's also something I'm interested in. I know there's at least one other editor project on Druid (not my own), and we also have interest in unbundling our (Druid's) multiline text widget so it's possible to integrate other functionality on top of it.
If you want help on specifically the Druid parts, you might be able to come by the #druid channel on xi.zulipchat.com and stir up some interest.Raph--On Fri, Nov 20, 2020 at 2:31 PM vvs <vvs...@gmail.com> wrote:Whoa! And I'm already spoiled by what Leo is doing with Lean 4. The so small core language and vastly extensible parser with an entire automation library for building and proving formal systems using incremental compilation with plans for interactive compiler guidance are mind blowing. That's taking aside your own exciting MM0 work. And I only have that much time to learn about lots of things. I'm torn already :(
--
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/dc7550eb-9c0b-4953-93b5-1c9640b0ffd9n%40googlegroups.com.
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/CADBEgNPr7K5F10F0A8OVjk%2BFvdaZL6w5Q4o5KzTZB%2B4oaVaCOQ%40mail.gmail.com.
Relocated from https://groups.google.com/g/metamath/c/NMZA_JRkU4U/m/ccP9bXZlAQAJ:On Fri, Nov 20, 2020 at 9:37 AM Benoit <benoit...@gmail.com> wrote:Mario, do you have some more detail about this project to write (I'm quoting you from github) "a verifier that would satisfy all the constraints of the CI system in terms of capabilities: checking all the typesetting stuff, definition checking, and full verification as efficiently as possible"?Thanks in advance.BenoîtThe plan is to start a new "community verifier" and build it with those tasks in mind. I think there has been too much fragmentation in verifier land; this makes it very hard for newcomers, especially those that are not especially computer literate such as traditional mathematicians. mmj2 is pretty good, but it's also quite old and the architecture isn't something I really want to continue to build on. MM1 builds a lot of lean-esque features into a metamath-like foundation, and I would say as a proof assistant it's a smashing success, in usability if perhaps not in users. I've been spoiled by lean to an extent and don't really see current metamath tools as up to par by comparison, and building mm0-rs has been enough to convince me that it is feasible to do the same thing for metamath.I value metamath's many verifiers; it's a great thing that a new verifier can be done as an afternoon project. But a proper proof assistant needs a lot more infrastructure to provide a high quality user experience, and the community is small enough as it is without additional fragmentation. We've managed to successfully collaborate on the set.mm github repo, but to date no verifier has received significant attention from >2 contributors, except mmj2 which has a couple drive-by contributions beyond the work by myself and Mel O'Cat (and I'm not actively developing the project anymore). There is no metamath verifier I would say is in a particularly healthy state of development.
As a starting point, I would like to replicate the main functions of metamath.exe, at least for one-shot tasks. That means reading and verifying a database, but also parsing it in such a way that edits can be applied, comments re-wrapped, and semantic information like document structure is available. Generating the web pages would also be a target. (This is quite difficult, as metamath.exe is a ball of hacks right now and I would like to start from a cleaner baseline.)
For the more advanced tasks, one design question that comes up early is whether to support "ungrammatical" databases. On the one hand, the metamath spec considers such databases valid, so they can't be rejected (unless the database contains the $j command asserting that it is grammatical). On the other hand, grammaticality enables an asymptotically more efficient structural storage (trees instead of strings), and also makes it possible to perform HTML construction in a saner way, where expressions are properly grouped rather than just appending tokens and hoping it looks well formed at the end. (This is where a lot of the hacks in metamath.exe come from.) Note that set.mm and iset.mm are grammatical, as well as most but not all of the smaller example databases. (I think miu.mm and lof.mm are the main counterexamples.) Perhaps we can degrade to a simpler verifier-only version in case the DB is not grammatical.
As far as language choice goes, I would recommend Rust. Beyond being well suited for the speed and architectural requirements of a verifier / proof assistant, both myself and Raph Levien (if I can interest him in this project) are involved in the rust ecosystem; maybe we can use the Druid UI framework for the front end. (I want to put in a word of caution though: one thing I learned from mmj2 is that it's a bad idea to write a text editor unless that's the main goal. This is not a trivial task and will suck up all your research time. Outsourcing the editor work for MM1 to VSCode made so many things easier.)
But really, the choice is not only up to me, as community buy-in for this project would be important. The ultimate goal is to become the de-facto standard proof assistant for metamath, put all our best ideas in it, and finally get over the popular conception of metamath as not practical for real mathematicians unless you have a high tolerance for manual labor
I've tried a couple of times to set up Eclipse for mmj2, but got stuck when trying to stepdebug the code after a ctrl+u: a few threads are thrown and the debugger doesn't "attach" to at least one of them. I'm sure it depends on having the right Java / Eclipse environment, but I love to write proofs, so I've never even asked Mario / David any help about setting up the right "environment" in order to help with the mmj2 development.I'm currently using a Mel O'Cat release that's not available anymore online, because he improved the search page in that release. I believe it's good enough to write long and complex proof.I've always been of the opinion that the most effective strategy would have been to improve mmj2, rather than starting new projects.I'd be really excited If we can come up with a better PA. I don't know anything about RUST, but I'm confident I can learn it. I hope we will set up a well-defined/isolated IDE: IMHO, the biggest problem with mmj2 is that it depends too heavily on the jvm version, the Eclipse version, the Eclipse project version.Recently, I tried to download the current mmj2 version but I wasn't able to run it, neither in Win10, nor in Ubuntu. I got runtime errors probably due to jvm version conflicts. I'm sure I could have fixed them, but I gave up and went back to my Mel O'Cat "special edition" :-)Consider that I spend hours every day in mmj2, I can't imagine a newcomer facing this kind of problems.
I completely agree with the "don't build the text editor" approach. I hope we can work on this new PA together. My main concern is that it will take a long time before being comparable to mmj2 and until then nobody will use it for "real" work and this will slow down its development.
On Nov 20, 2020, at 3:02 PM, Mario Carneiro <di....@gmail.com> wrote:
I value metamath's many verifiers; it's a great thing that a new verifier can be done as an afternoon project. But a proper proof assistant needs a lot more infrastructure to provide a high quality user experience, and the community is small enough as it is without additional fragmentation. We've managed to successfully collaborate on the set.mm github repo, but to date no verifier has received significant attention from >2 contributors, except mmj2 which has a couple drive-by contributions beyond the work by myself and Mel O'Cat (and I'm not actively developing the project anymore). There is no metamath verifier I would say is in a particularly healthy state of development.
Quick nit: I would distinguish “verifier” from “proof assistant” (as we already often do). I also value Metamath’s many verifiers. I don’t think the *verifiers* are in a bad state, they work just fine... but that’s mostly because our exceptions for verifiers are limited.
Some of the hackishness in Metamath-exe’s web page generation is because C is *terrible* at string handling. Metamath-exe is also relatively slow because it’s single threaded; if we could run the generators in parallel we could *dramatically* reduce HTML generation time.
For the more advanced tasks, one design question that comes up early is whether to support "ungrammatical" databases. On the one hand, the metamath spec considers such databases valid, so they can't be rejected (unless the database contains the $j command asserting that it is grammatical). On the other hand, grammaticality enables an asymptotically more efficient structural storage (trees instead of strings), and also makes it possible to perform HTML construction in a saner way, where expressions are properly grouped rather than just appending tokens and hoping it looks well formed at the end. (This is where a lot of the hacks in metamath.exe come from.) Note that set.mm and iset.mm are grammatical, as well as most but not all of the smaller example databases. (I think miu.mm and lof.mm are the main counterexamples.) Perhaps we can degrade to a simpler verifier-only version in case the DB is not grammatical.
I think only supporting trees is quite reasonable for a proof assistant. Almost all real metamath work uses the “grammatical” databases (is there a better term?). Degrading to a “verifier-only” version is a fine long-term plan. Supporting that could even be long delayed because there are many verifiers that can already handle “non-grammatical” databases; we don’t really need another one right now.
Here are some traits I’d like to see in a better Metamath proof assistant:1. Easily usable as a programmatic *library* from other languages. I should be able to import the library from most any other language, then use it to load databases, do queries, etc. The higher-level capabilities should implemented by calling that interface & ideally callable as well. That would make it much easier to build other things.
2. Implemented in a memory-safe language, and preferably statically typed. I like the confidence this could provide.
3. Has a small kernel implementing “legal actions”, which is distinguished from the many tactics it includes that allow trying things out without producing an invalid state as long as the tactic obeys simple static rules (the state may be *useless* but not *wrong*).
4. Support for forwards *and* backwards reasoning at least, and ideally middle-out, in its proof assistant. Some proof assistants can only go backwards; I really appreciate mmj2’s ability to do forwards, backwards, and even middle-out.
5. Lots of automation (eventually).
6. Ideally, it should include he ability to easily call out to other components written in other languages to help automation, e.g., the ability to call out to a machine learning module or some such. There are existing tools that can prove some claims; if they could be called, and then inject their proofs in a Metamath database, that’d be awesome.
7. Optional/lower importance: Perhaps enable simpler handling of parentheses within the human UI. It’d be nice to be able to use parens without surrounding each one with whitespace. I don’t think supporting precedence is important (it might even be undesirable), but it would be nice to simplify handling many parens. That may be challenging, since there are a number of constants with ( or ) in their name in set.mm such as (/) and (,).
Rust is an interesting choice. It’s really easy to create a library others can call with Rust (#1), it’s memory-safe & static (#2), and it’d be easy to implement a small kernel (#3). It’s blazingly fast & easy to parallelize. If the goal is to implement something that can automatically do a lot, that’d a good start.I’ve played with Rust but not tried to build a proof assistant system with it. Would that be excessively hard? It’s true that Rust has lots of nice functional language syntactic sugar that makes some constructs easy. However, Rust doesn’t have a built-in garbage collector; its borrow system often makes that unnecessary, and that’s one reason why it plays nicely with other languages, but would we have to fight Rust too much because of that? Or is that not really an issue? Rust doesn’t natively like graphs very much (unless you disable its safeties); is that not a real problem in this case, or do alternatives such as using indices (e.g., https://smallcultfollowing.com/babysteps/blog/2015/04/06/modeling-graphs-in-rust-using-vector-indices/ ) resolve that concern?
One problem with Rust is that there’s no built-in REPL. If it’s accessible via an easily imported library that may be a non-problem (e.g., make it easy to import into Python and use Python’s REPL).
I might be willing to help out if it’s Rust. But I have only fiddled with Rust, not used it is seriously for this kind of application, so it might be useful to hear if it’s a decent map for the purpose. To be honest, I’ve been looking for an excuse to delve further into Rust, and this might be a good excuse :-). You’ve inspired me, I think I’ll go de-rust my Rust in case this goes anywhere.However: Let’s imagine that the implementation is complete. What would interacting with it look like? What is its human UI? What is an example of a rough-draft library API?
" MM1 builds a lot of lean-esque features into a metamath-like foundation, and I would say as a proof assistant it's a smashing success, in usability if perhaps not in users. "
One question re this, would some tutorials for helping people use MM1 accomplish quite a lot? How hard is it to transfer work done in MM1 to a classic mm proof? I mean if there is already a PA which you are happy with there then it feels a bit like others could just learn to use that.
David's tutorials for mmj2 were super helpful for me for getting into using it, something similar might be cool.
I should add that I think it’d be valuable if a proof verifier/proof assistant was invokable through just a web browser. It doesn’t need to be full speed, but one you can try out can be really helpful.
If Rust is used, there’s an obvious way to do that: WebAssembly. Compile the Rust library into WebAssembly, then invoke it from JavaScript. That would mean that a single library could be used in different circumstances.
Still, much like how it's better to outsource text editing to an existing editor, it's better not to start from scratch if we can help it. So if Rust is really the language we decide to use, I'd recommend building off of the existing Rust verifier if possible. I assume that https://github.com/sorear/smetamath-rs is the Rust verifier that's been mentioned?
Improving Metamath tooling is something I definitely want to do. I was already working a towards improving MMJ2, in my personal fork I fixed all the linter warnings, ported some of the old batch file unit tests, and also started porting the macros to use the Rhino javascript engine (in preparation for Nashorn's removal).
No one seems to be explicitly saying that they will start this project. I'm not sure I can take the lead, because I don't know much yet about how to implement a proof assistant, and because this is meant to be a community project but I haven't participated much in the community. Still, I've used Rust before, and as a first step, I could try to translate MMJ2's LRParser to smetamath-rs, and report on my progress here in a few weeks.
Rust isn't a functional programming language, but the first implementation of MM1 was in Haskell and it had some memory usage and speed issues that would have required some significant concessions to imperative style to fix.
Rust isn't a functional programming language, but the first implementation of MM1 was in Haskell and it had some memory usage and speed issues that would have required some significant concessions to imperative style to fix.Too bad for Haskell I'd guess. I don't think that there is no solution, here's how Lean 4 deals with similar problem: https://arxiv.org/abs/2003.01685
> On Nov 21, 2020, at 6:22 PM, Mario Carneiro <di....@gmail.com> wrote:
> If there is enough interest from others that I'm not the only one on the project, I don't mind taking the lead here. If it incorporates common code from mm0-rs then that will be a good excuse for me to split it off to a new project (the MM0 monorepo is getting pretty hefty) and maybe also expose a library (depending on whether this new verifier is literally mm0-rs under some settings or a separate executable that just links against a library with common code from mm0-rs).
>
> That said, I am nearing the end of my PhD and probably shouldn't be devoting large quantities of time to something that doesn't move my thesis forward. :P
:-). If there’s a way to combine them that’d be great.
> In that case, a good first goal would be to determine what the features of mmj2 *are*. Specifically, what features are actually used by people? There are a lot of dead relics. The main ones that come to mind are:
> * unification (kind of a requirement for any proof assistant),
> * filling in a step given all the type info (and also showing all matches in case some unification is possible),
> * as well as the more recent "auto step" proof search, which applies any theorem matching some descent criterion (and not on a blacklist).
> Anything else? There are a bunch of options in the RunParms that do stuff but I don't think any of them are really important (the definition checker excepted but that's already on the todo list). There is some documentation as well but it's a mixture of old stuff and new stuff and not very well organized. This is probably something even the less technically minded could help with.
Unification with past/next steps, and unification given the name of an existing theorem/axiom, are definitely minimums, but they’re also not too challenging to implement. Those are the keys for me. That includes, when specifying something, immediately creating its hypotheses & supporting work variables (or something like them for identifying “don’t know yet”).
Important item: quietly reordering rules when the proposed order cannot be unified but another order can be. The simple automation done by leading “!” Is really helpful. The “replace this step by that step” e.g., “d1::#1” is not used often but is very helpful when needed.
Being able to double-click on any step & show what *could* be unified (and what that would produce) is useful. I don’t use it as much as much you might think.
The runParms are mostly a pain, partly because it’s a nonstandard way to do things. Usually you just pass a filename of the file to edit. Optionally you use options lie -? Or --long_name, and/or an init file.
> Actually, even if we branch off to a different editor mode, maybe it would be good to support something roughly like mmj2 for "backward compatibility" / getting people to use it earlier so they can speed up development.
I think that *would* be a good idea, especially if as much as possible it were built on calls to a library. At least that would provide a familiar alternative, and a reason to use it instead. Hopefully it would use a text editor that can help pair parens :-).
On Sat, Nov 21, 2020 at 12:47 PM vvs <vvs...@gmail.com> wrote:I sense some confusion here. Let's define our dictionary first.IDE is just a text editor with UI for syntax highlighting, autocompletion, code and documentation searching and integrating other stuff. It also has to be fast and robust. Verifier should just check soundness of definitions, wellformedness of terms and correctness of proofs. Working incrementally is a big advantage. Proof assistant should enable automated synthesis of proofs by inferring missing information, automatically coercing terms, filling in gaps and making good suggestions (according to Andrej Bauer).mmj2 has a very basic IDE with integrated verifier. It's also a very rudimentary PA as it has only a simple unification tool for synthesis. Granted, there are some basic tactics written in JS but it isn't suited at all to be programmed by an average user. It's also buggy, slow and monolithic, it can't be easily used from other projects. I believe that's what prompted Mario to start this thread in a first place, right? There is also an established tradition to write PA in a functional programming language.I completely agree with this. Building a good IDE is a hard and time consuming problem that we *should not* attempt. The major gains to be had are in the "proof assistant" parts. I want to call out the MM1 "tactic language" at this point, which I think is much better integrated than the JS macro language in mmj2. MM1 uses a scheme-like programming language inside "do" blocks, where you can just write stuff and they get evaluated on the spot as you type. This makes it usable for querying the system, i.e. show me the declaration/proof of "foo", what does this depend on, search for theorems matching this string, etc. Proofs are also scheme expressions, and while a lot of proofs are just big quoted literals containing the proof, you can always just start writing a program that generates the proof literal instead, or call a function that will be given the context and produces the proof. So for example the arithmetic evaluator "norm_num" is defined here ( https://github.com/digama0/mm0/blob/d07e5d64e68510095044f1eb12988f3b775c95ec/examples/peano_hex.mm1#L596-L601 ), and you can see on the succeeding lines how it is being applied to prove a bunch of basic theorems.The downside of a scripting language like this is that they tend to be slower than native code, although I got my MM1 CI set up yesterday and the entire library still compiles in under 2 seconds so it's tolerable (and still way better than lean, which has a similar front end design to MM1).Rust isn't a functional programming language, but the first implementation of MM1 was in Haskell and it had some memory usage and speed issues that would have required some significant concessions to imperative style to fix. I think Rust actually gets the important things right when it comes to the problems that FP languages solve, from a modeling and reasoning standpoint. I guess scheme is a lisp which is FP? It's not a particularly pure FP: at least my implementation uses references for metavariables so they get used fairly heavily.
Here are some traits I’d like to see in a better Metamath proof assistant:1. Easily usable as a programmatic *library* from other languages. I should be able to import the library from most any other language, then use it to load databases, do queries, etc. The higher-level capabilities should implemented by calling that interface & ideally callable as well. That would make it much easier to build other things.I like this idea. Rust makes it easy to expose libraries to other programs via crates.io, and I've considered doing this for mm0-rs, although I don't have a particularly clear conception of what the most useful hooks would be. Perhaps this can be tacked as the project gets going.
2. Implemented in a memory-safe language, and preferably statically typed. I like the confidence this could provide.I think this is the main reason it's best to write in something like C++ or its better cousin Rust - it's a big project so you want static types, modules, namespaces and all that jazz, but it's also performance sensitive so you want as much native code as you can get. (Java is okay in this regime, but these days I don't really see any reason to pick it over alternatives.)
3. Has a small kernel implementing “legal actions”, which is distinguished from the many tactics it includes that allow trying things out without producing an invalid state as long as the tactic obeys simple static rules (the state may be *useless* but not *wrong*).In MM1 this is mostly implemented through functions on the "Environment" (the set of all proven theorems so far), which only does this work at the unit of entire theorems. Tactics are permitted to construct arbitrary proof terms and are expected to only produce well formed proof terms but you get a runtime error if not. Unlike lean and other LCF-style provers, I don't make any significant attempt to isolate the "kernel", because the source of truth is an external verifier. (If this verifier / proof assistant is to be a proper, trustworthy verifier, the verifier part should probably be isolated from the rest of the system.)
...
5. Lots of automation (eventually).I think the best way to get automation is to have a language that lets end users write the automation.
I’ve played with Rust but not tried to build a proof assistant system with it. Would that be excessively hard? ...
Obviously as the author of mm0-rs I can speak to the effectiveness of Rust for writing proof assistants. For storing terms, I usually opt for a recursive struct using reference-counted pointers; this limits you to acyclic data structures but that's usually not a problem for a proof language. To store a "baked" proof that is not being manipulated and is fully deduplicated, I use a combination: the expression is really a tuple (Vec<Node>, Node) where Node is a recursive struct with Arcs as mentioned, but with a constructor Ref(i) that can be used to refer to a node on the "heap" (the Vec<Node>), and elements in the heap can similarly refer to earlier vectors on the heap. (See https://github.com/digama0/mm0/blob/d07e5d64e68510095044f1eb12988f3b775c95ec/mm0-rs/src/elab/environment.rs#L135-L158 .)
This is useful to explicitly represent subterm sharing, so that you can have a highly redundant proof (for example if each step i+1 refers to step i twice then the unshared proof will be exponential size) that you can still perform operations on (unification, type checking, etc) in linear time. It's possible to do the same thing with just Arcs, but you have to keep a hash table of visited nodes and if you forget and just recurse naturally then the entire system will grind to a halt. A lot of proof assistants suffer from this problem (including metamath.exe!)
One problem with Rust is that there’s no built-in REPL. If it’s accessible via an easily imported library that may be a non-problem (e.g., make it easy to import into Python and use Python’s REPL).As much as I like rust I don't think it lends itself well to a REPL, in the sense that the rust language shouldn't be typed line by line, it benefits a lot from scoping. MM1 uses Scheme instead for the REPL stuff, but all the heavy lifting is done in Rust.
I might be willing to help out if it’s Rust. But I have only fiddled with Rust, not used it is seriously for this kind of application, so it might be useful to hear if it’s a decent map for the purpose. To be honest, I’ve been looking for an excuse to delve further into Rust, and this might be a good excuse :-). You’ve inspired me, I think I’ll go de-rust my Rust in case this goes anywhere.However: Let’s imagine that the implementation is complete. What would interacting with it look like? What is its human UI? What is an example of a rough-draft library API?Since most of my experience in this area is coming from MM1 and the mm0-rs implementation, that would be my default answer to such questions, unless others object. You interact through vscode or another LSP-enabled editor, with a relatively small file (not set.mm) containing "code" in some TBD language that I will assume looks like MM1 :) .
The server runs in the background and provides point info and diagnostics. By typing directives in a do block you can use it like a REPL. At the top of the file is likely "import "set.mm";" which says to preload set.mm and base the current development on it. (Perhaps it should instead be something like "altering "set.mm";" if the goal of the file is to construct an alteration to set.mm that may involve inserting theorems in places, renaming things and other such stuff.) The user can add lines to adjust set.mm notation to their preference, and the language can come with some presets that can be included so that we can collect an approved set of alterations for set.mm.If you want to add a new theorem, you can declare one in the file, with a notation like MM1's but possibly with some modifications to support DV conditions that are not expressible in MM0 (for example if two set variables are not necessarily disjoint). You can write a literal expression if the proof is simple enough, or you can call a tactic, or you can pop open a (focus) block as in MM1 to enter tactic mode where you evolve a goal state through the use of imperative commands like applying theorems, switching between goals, calling automation and so on.At the end of the day, you get a file that represents an alteration to set.mm, or a new .mm file. There is some command in the editor, or you can use the console version of the program such as "mm0-rs compile foo.mm1", and it will construct a new mm file as requested, making minimal formatting changes to the file and otherwise adding your new MM theorems, making some attempt to format things the way they would be formatted in a by hand edit. The user can then make their own formatting tweaks if they want and PR to set.mm repo.
For a library API, I think we should expose the main data structures, with programmatic versions of the things I've mentioned. In MM1 there are two main data structures: the Environment and the Elaborator. The Elaborator is the state that changes in the course of processing an .mm1 file, while the Environment is the "proof" content of the file; the elaborator is discarded once the file is finished and the "result" is the final Environment. The Elaborator stores things like the current status of file-local settings, the errors we need to report, and the file AST. I think most of the elaborator functions, corresponding to individual directives, tactics, and statements in the file, can be exposed as API methods on the Environment to external code. That way external code can say things like "add this notation", "add this theorem", "check this theorem" and so on. Additionally some proof state specific stuff should also be exposed so that external programs can act on a given proof state, allowing for sledgehammer-like tools.
One issue is that MM1 is a proof assistant for MM0, it doesn't currently support MM. One way I would like to support this is to be able to "import "foo.mm";" in an MM1 file, which will convert the MM theorems into MM1 and import them into the current file; this will make it easy to build on set.mm from within an MM0 development, but it doesn't "give back" to the MM database, it is a one way conversion (at least so far), and even if the reverse conversion were added it would probably not be the inverse map, resulting in ugly proofs after round-tripping.I think that it may well be possible to extend mm0-rs to allow swapping out the back end so that it is actually working with MM, and then most of the additions mentioned here are incremental changes on that baseline. The main goal with this new verifier is to attempt to address the needs of metamath users / set.mm contributors and not rock the boat so much by replacing the foundations as is done with MM0, but I agree that this could be incorporated as a sub-mode of mm0-rs usage.
David's tutorials for mmj2 were super helpful for me for getting into using it, something similar might be cool.There are currently no tutorials for MM1, only a few scattered demos and a spec document (https://github.com/digama0/mm0/blob/master/mm0-hs/mm1.md). It's starting to get to a relatively stable place, so I don't mind moving to a more professional packaging if people are interested. There are probably a number of glaring problems for people who are not me that need to be addressed though, so I would encourage folks to try it out, get hopelessly stuck and then report your experience as a basis for documentation and improvements.
Providing a Scheme-like interface is a reasonable approach. It’s easy to implement & provides a lot of flexibility. The big problem is that MANY people hate their syntax, e.g., “lots of irritating silly parentheses”. As you know, I think it’d be *much* better if it supported neoteric syntax (at least), so that you can use syntax like f(5) and {2 + 3}, as that eliminates the main complaint about Lisps while retaining all their benefits.
If you’re picky about types, you could even trivially implement a preprocessor to convert the Scheme-like language into Rust, and then compile it into the result. Then, once you’re happy with something, you could “freeze” into a faster Rust implementation.
I like this idea. Rust makes it easy to expose libraries to other programs via crates.io, and I've considered doing this for mm0-rs, although I don't have a particularly clear conception of what the most useful hooks would be. Perhaps this can be tacked as the project gets going.I expect that’s the only way to tackle it. The key is to agree early on that “this is a library, with a minimal UI on top”. If you can change the UI without changing what’s underneath, then that’s a big success.
2. Implemented in a memory-safe language, and preferably statically typed. I like the confidence this could provide.I think this is the main reason it's best to write in something like C++ or its better cousin Rust - it's a big project so you want static types, modules, namespaces and all that jazz, but it's also performance sensitive so you want as much native code as you can get. (Java is okay in this regime, but these days I don't really see any reason to pick it over alternatives.)Neither C nor C++ are memory-safe. I’d prefer to work in memory-safe land.
Java has garbage collection & semantics that are very familiar to many (e.g., object orientation & references).
3. Has a small kernel implementing “legal actions”, which is distinguished from the many tactics it includes that allow trying things out without producing an invalid state as long as the tactic obeys simple static rules (the state may be *useless* but not *wrong*).In MM1 this is mostly implemented through functions on the "Environment" (the set of all proven theorems so far), which only does this work at the unit of entire theorems. Tactics are permitted to construct arbitrary proof terms and are expected to only produce well formed proof terms but you get a runtime error if not. Unlike lean and other LCF-style provers, I don't make any significant attempt to isolate the "kernel", because the source of truth is an external verifier. (If this verifier / proof assistant is to be a proper, trustworthy verifier, the verifier part should probably be isolated from the rest of the system.)That’s definitely different than an LCF-style prover. Using a separate trustworthy verifier instead does make sense, though wouldn’t that delay detection of problems?Are there really advantages to *not* having a kernel? I really do want to know.
For a library API, I think we should expose the main data structures, with programmatic versions of the things I've mentioned. In MM1 there are two main data structures: the Environment and the Elaborator. The Elaborator is the state that changes in the course of processing an .mm1 file, while the Environment is the "proof" content of the file; the elaborator is discarded once the file is finished and the "result" is the final Environment. The Elaborator stores things like the current status of file-local settings, the errors we need to report, and the file AST. I think most of the elaborator functions, corresponding to individual directives, tactics, and statements in the file, can be exposed as API methods on the Environment to external code. That way external code can say things like "add this notation", "add this theorem", "check this theorem" and so on. Additionally some proof state specific stuff should also be exposed so that external programs can act on a given proof state, allowing for sledgehammer-like tools.There might need to be some work so that the data structures are easy-to-navigate & not fragile. I wonder if methods would be useful (e.g., what appear to be “values” are really computed). I would hope a REPL could query their state, and in some cases change them (though maybe only in specific ways).
Mario Carneiro wrote:
> If there is enough interest from others that I'm not the only one on the project, I don't mind taking the lead here.
I suppose this is the time to express interest or lack of interest. I
will express a small amount of interest. In terms of the value of the
concept, the interest comes from the idea that I can think of various
things (new features, cleaning up various rough edges, fixing buggy or
odd behaviors, etc) we might want which aren't in metamath.exe or mmj2 .
And that those two codebases - for all their usefulness - are I suspect
hitting a bit of a limit in terms of whether you'd want to want to do a
lot of new development to them.
Hi all,
This all sounds very interesting!
Did I understand everything correctly?
I never tried rust, that could be an opportunity!
BR,
_
Thierry
In that case, a good first goal would be to determine what the features of mmj2 *are*. Specifically, what features are actually used by people? There are a lot of dead relics. The main ones that come to mind are:* unification (kind of a requirement for any proof assistant),
* filling in a step given all the type info (and also showing all matches in case some unification is possible),
* as well as the more recent "auto step" proof search, which applies any theorem matching some descent criterion (and not on a blacklist).Anything else? There are a bunch of options in the RunParms that do stuff but I don't think any of them are really important (the definition checker excepted but that's already on the todo list). There is some documentation as well but it's a mixture of old stuff and new stuff and not very well organized. This is probably something even the less technically minded could help with.
On Nov 21, 2020, at 10:15 PM, Mario Carneiro <di....@gmail.com> wrote:On Sat, Nov 21, 2020 at 8:42 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:Providing a Scheme-like interface is a reasonable approach. It’s easy to implement & provides a lot of flexibility. The big problem is that MANY people hate their syntax, e.g., “lots of irritating silly parentheses”. As you know, I think it’d be *much* better if it supported neoteric syntax (at least), so that you can use syntax like f(5) and {2 + 3}, as that eliminates the main complaint about Lisps while retaining all their benefits.I'm inclined not to spend much time on this complaint. Better to spend some time with it, get a sense for the way things are put together, and *then* propose improvements. Alternate syntax is not out of the question but it needs to fit within the other design constraints of the language. In particular, MM1 is in many ways an MVP for a metamath based proof assistant, enough to help me prove my big theorems and not much more. If this is to become some big flagship product then I don't mind investing more to make it convenient, but only after the more pressing problems are dealt with.
If you’re picky about types, you could even trivially implement a preprocessor to convert the Scheme-like language into Rust, and then compile it into the result. Then, once you’re happy with something, you could “freeze” into a faster Rust implementation.Indeed, I don't recommend going overboard with the metaprogramming because the result isn't especially maintainable without static types. Complicated tactics should be written as plugins, either in rust or dynamically linked from another language. The main strength of the language is for micro-tactics like when two branches of a proof are almost but not quite the same, and simple pattern matching tactics like norm_num.
Java has garbage collection & semantics that are very familiar to many (e.g., object orientation & references).Rust's approach to handling memory feels very similar to Java as an end user, but it's quite different under the hood (the latter is obvious if you hear the press, but the former might be more surprising). You almost never have to explicitly drop things, and when you do it's usually because you need to unlock a mutex or something like that that goes beyond regular memory management.
There are lots of verification-related technologies that don't have an LCF style approach; SAT and SMT solvers, model checkers, and even some proof languages like PVS and NuPRL come to mind. But I think MM1 is qualitatively different from these examples, in that MM1 is a tool for producing a proof at the end of the day, while the others are producing "correctness", with a yea/nay answer at the end and nothing more. If that's all you have, you really want to know that everything that goes into that yea/nay answer is trustworthy, and that's just what our verifiers are doing. But with a proof object, you can always just check it at your leisure.
...
In summary, I don't think it's important to have a kernel given how many backup plans we have, although any embedded verifier would be held to the usual standards of correctness, but it can be done if we care to pursue this.
There might need to be some work so that the data structures are easy-to-navigate & not fragile. I wonder if methods would be useful (e.g., what appear to be “values” are really computed). I would hope a REPL could query their state, and in some cases change them (though maybe only in specific ways).In Rust, there is some focus placed on privacy as an abstraction mechanism. You can have a struct with private fields, and provide public functions as accessors to the data. This is especially important for anything around the "kernel" like the Environment struct, since in a public API we probably want to make it hard to misuse. Right now I think almost nothing in mm0-rs is public, although a lot of things are pub(crate) (meaning accessible by other code in the project but not from other modules). Making something public is to some extent a stability promise; there are semver rules related to changing the layout of a struct to add public fields and so on so each of these things should be considered carefully once we have some user code that wants to interface with it.
Please, let me know what's the best environment to set up to contribute to the new tool:- VSCode + RUST seems to be the candidate, right? (if it were possible to have a portable environment it would be a plus)- at least Windows + Linux is a must, I guess
On Nov 21, 2020, at 6:22 PM, Mario Carneiro <di....@gmail.com> wrote:If there is enough interest from others that I'm not the only one on the project, I don't mind taking the lead here. If it incorporates common code from mm0-rs then that will be a good excuse for me to split it off to a new project (the MM0 monorepo is getting pretty hefty) and maybe also expose a library (depending on whether this new verifier is literally mm0-rs under some settings or a separate executable that just links against a library with common code from mm0-rs).
Since most of my experience in this area is coming from MM1 and the mm0-rs implementation, that would be my default answer to such questions, unless others object. You interact through vscode or another LSP-enabled editor, with a relatively small file (not set.mm) containing "code" in some TBD language that I will assume looks like MM1 :) . The server runs in the background and provides point info and diagnostics. By typing directives in a do block you can use it like a REPL. At the top of the file is likely "import "set.mm";" which says to preload set.mm and base the current development on it. (Perhaps it should instead be something like "altering "set.mm";" if the goal of the file is to construct an alteration to set.mm that may involve inserting theorems in places, renaming things and other such stuff.)
The user can add lines to adjust set.mm notation to their preference, and the language can come with some presets that can be included so that we can collect an approved set of alterations for set.mm.If you want to add a new theorem, you can declare one in the file, with a notation like MM1's but possibly with some modifications to support DV conditions that are not expressible in MM0 (for example if two set variables are not necessarily disjoint). You can write a literal expression if the proof is simple enough, or you can call a tactic, or you can pop open a (focus) block as in MM1 to enter tactic mode where you evolve a goal state through the use of imperative commands like applying theorems, switching between goals, calling automation and so on.At the end of the day, you get a file that represents an alteration to set.mm, or a new .mm file.
On Nov 22, 2020, at 8:58 AM, Thierry Arnoux <thierry...@gmx.net> wrote:Hi all,
This all sounds very interesting!
From the different posts, here is a possible breakdown I see:
On Nov 21, 2020, at 10:15 PM, Mario Carneiro <di....@gmail.com> wrote:On Sat, Nov 21, 2020 at 8:42 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:Providing a Scheme-like interface is a reasonable approach. It’s easy to implement & provides a lot of flexibility. The big problem is that MANY people hate their syntax, e.g., “lots of irritating silly parentheses”. As you know, I think it’d be *much* better if it supported neoteric syntax (at least), so that you can use syntax like f(5) and {2 + 3}, as that eliminates the main complaint about Lisps while retaining all their benefits.I'm inclined not to spend much time on this complaint. Better to spend some time with it, get a sense for the way things are put together, and *then* propose improvements. Alternate syntax is not out of the question but it needs to fit within the other design constraints of the language. In particular, MM1 is in many ways an MVP for a metamath based proof assistant, enough to help me prove my big theorems and not much more. If this is to become some big flagship product then I don't mind investing more to make it convenient, but only after the more pressing problems are dealt with.This is something I can easily do. I’ve implemented neoteric expressions in Scheme, Common Lisp, and Java. It turns out to be very short, *AND* they’re totally optional for use. That is, you can always say (foo bar bar) if you prefer it over foo(bar baz).
To be fair, some SMT solvers *do* have proof producing mechanisms (e.g., CVC4 and Z3). For comparisons, see: http://homepage.divms.uiowa.edu/~viswanathn/qual.pdf
Careful consideration is important, agreed. But I think we want to make sure that a lot of things are (eventually) accessible by a library call. If the library can be imported from (say) Python & JavaScript, and the library is eventually rich, then a whole lot of re-implementation does *not* need to happen.
I’m definitely interested. If there’s a way I can help, I’ll help. My math chops are nowhere near yours, but I can sling code.
Since most of my experience in this area is coming from MM1 and the mm0-rs implementation, that would be my default answer to such questions, unless others object. You interact through vscode or another LSP-enabled editor, with a relatively small file (not set.mm) containing "code" in some TBD language that I will assume looks like MM1 :) . The server runs in the background and provides point info and diagnostics. By typing directives in a do block you can use it like a REPL. At the top of the file is likely "import "set.mm";" which says to preload set.mm and base the current development on it. (Perhaps it should instead be something like "altering "set.mm";" if the goal of the file is to construct an alteration to set.mm that may involve inserting theorems in places, renaming things and other such stuff.)I think it should be like “import set.mm [[before|after] NAME]”, so you know what’s allowed & what is not.
The user can add lines to adjust set.mm notation to their preference, and the language can come with some presets that can be included so that we can collect an approved set of alterations for set.mm.If you want to add a new theorem, you can declare one in the file, with a notation like MM1's but possibly with some modifications to support DV conditions that are not expressible in MM0 (for example if two set variables are not necessarily disjoint). You can write a literal expression if the proof is simple enough, or you can call a tactic, or you can pop open a (focus) block as in MM1 to enter tactic mode where you evolve a goal state through the use of imperative commands like applying theorems, switching between goals, calling automation and so on.At the end of the day, you get a file that represents an alteration to set.mm, or a new .mm file.
This doesn’t seem very interactive. Can this be made fast enough to provide rapid feedback so someone can see what is (or is not) working? Is there a variant that would be easily interactive? Maybe we can cache results so that “if nothing has changed here’s the answer” to make this fast?
In principle I think that’s right, at least in the sense that there would be multiple crates, each one focused on different tasks & building up on others. There will probably be changes in the details as we flesh it out.I think that, for speed, there will probably need to be a separate crate for “bulk verification of a file’s contents”. This is a role performed by smm3. There are optimization tricks for a bulk verifier, and we verify whole files often enough that it makes sense to do that. Also, I think a PA may only accept grammatical databases, while the bulk verifier might be designed to handle non-grammatical ones too.
On Nov 22, 2020, at 5:35 PM, Mario Carneiro <di....@gmail.com> wrote:In MM1, I think it wouldn't be so great, because (1) it's way too easy to misspell (f g (a b) c) as (f g(a b) c), particularly when typing quickly;
and (2) it doesn't mesh well with the @ syntax for cutting down parens.
I call it scheme-like but it's sufficiently different that it is its own language with its own idioms, which is why I emphasize that you should try using it before proposing changes.
(Also, there is a precedence issue in (f ,g(a) b), does that mean (f (,g a) b) or (f ,(g a) b)?)
Of course we want to avoid reimplementation of core components as much as possible. My plan is to wait for the dependent program to start existing, and then use its requirements to help determine what needs to be public.
Your average set.mm modification, especially a maintenance change, may touch many theorems in many places. So I wouldn't want to require that they all fit in some contiguous block. Perhaps (before/after NAME) can be a freestanding command to change the context, or it can be a modifier on the theorem command to affect where an individual theorem goes.
...
It's quite interactive. The script is executed continuously every time you type a character in the editor, so you don't have to press a command or anything to make it go. Peano.mm1 is starting to have noticeable slowdown (maybe .7 seconds) but it's already 6500 lines and almost 2000 theorems, and you can always speed it up by moving a prefix of the file to another file. (I'm planning to support more checkpointing within a file so that it's fast even if you are editing in the middle, but currently it just reads and executes the whole file.) I think that's more than fast enough for the average metamath proof. Honestly it's an order of magnitude faster than mmj2.
Yes, that's the "CI verifier" that started this discussion. I find it easier for maintenance purposes to support all the modes in one tool, using subcommands in the command line like "mm0-rs server" and "mm0-rs compile foo.mm1", although you can compile out the tools separately if one of them requires more dependencies or has too much code in it.
Hi Mario,hereyou show peano.mm1 in VSCode and you write"The basic idea is that MM1 is a scripting language for assembling MM0 proofs and statements. It's untrusted, and functions as the IDE for MM0"Looking at one of your presentations I've seen you've also completely translated set.mm to mm0, isn't it?Would it be possible, for you, to video-record a session in which you proof a simple new theorem (starting from the mm0 translation of set.mm) ?
No audio is needed, and there's no need to make the video available on youtube to everybody. Just a short session to show us how it would be the workflow:load available axioms/definitions/terms/theorems > create new theorem> write/verify proof > save created proof (add to the pre-existing "stuff")
On November 27, 2020 12:14:09 AM EST, Mario Carneiro <di....@gmail.com> wrote:
step folding is also an option although I don't know how to make
>that not annoying.
If it can be done easily without JavaScript, you should do it that way instead. It's generally faster do to it that way, and it'd be nice to have some functionality work when client-side JavaScript is disabled. There are obviously diminishing returns where that doesn't make sense.
Basic text search is already built into browsers; I don't know if people need more than that for searching.
> Another thing that is somewhat important for MM0 is
>"expr-folding", where subexpressions that are used in many contiguous
>steps
>(like the proof context) are abbreviated. MM/MM0 like to work with such
>expressions as they can be unified in constant time, but the standard
>metamath proof display format makes this look very repetitive (and it
>is
>also expensive to print), suggesting that somehow the print isn't
>capturing
>"the essence of the proof" because it appears to be more repetitive
>than is.
A fair point. The metamath proof display has this problem also.
In some texts you would show at the beginning some definitions to make notation simpler, followed by the text that uses it. Perhaps you could automatically detect sequences of symbols of a certain length that get reused more than a certain number of times, give them special symbols, and put them at the top as shorthand definitions. E.g., $1, $2, and so on. Each list would be local to a particular theorem. They could even other shorthand definitions. I don't know if that would actually help, but I'm throwing it out there as an idea.
On Nov 27, 2020, at 1:26 PM, Mario Carneiro <di....@gmail.com> wrote:On Fri, Nov 27, 2020 at 1:17 AM David A. Wheeler <dwhe...@dwheeler.com> wrote:On November 27, 2020 12:14:09 AM EST, Mario Carneiro <di....@gmail.com> wrote:
step folding is also an option although I don't know how to make
>that not annoying.
If it can be done easily without JavaScript, you should do it that way instead. It's generally faster do to it that way, and it'd be nice to have some functionality work when client-side JavaScript is disabled. There are obviously diminishing returns where that doesn't make sense.I'm not fussed about the technology used to achieve it, but my point is that if you use step folding you will be clicking on unfold icons all day to get through a 200 step proof. MM0 has a heavy linear sequence due to its use of @ , so perhaps we can fold steps off that linear path; the parenthesis nesting is usually only 3 or 4 (and often lower) except in some highly automated proofs, while the actual step depth increases linearly with the proof size (so it could be 20 or 30 for an average proof).
Basic text search is already built into browsers; I don't know if people need more than that for searching.No? I use metamath's search function all the time when the web site can't help, and I guess URLs pretty often when metamath is not on hand. I'm talking about finding *theorems*, not steps. And anything with a fancy unification search isn't going to be usable with just browser search. Granted, the index page can probably be text-searched, but I doubt it will stay as one page forever; I think there are over 200 mmtheorems*.html pages.
My idea is that the user selects a target step and a "width" (a configurable constant, say 10), and then all subexpressions that are not "destructured" in the steps which are less than distance 10 from the chosen point along the graph are abbreviated. (In other words, this is what you would get if you wrote all those steps in mmj2 without the formulas and let it find them by unification.) If you consider all the steps, you probably won't get any abbreviations, but the more "local" you make it the more aggressively it will shrink terms. This will require the pretty printer to be in JS, though.
I've just put the finishing touches on the mm0-rs HTML generator, which makes pages such as https://digama0.github.io/mm0/peano/thms/addass.html .
I guess there's the concept of "definition" for those terms(?) : can it be rendered in a linked html page?
--
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/6a622530-e403-43d0-962d-8526bd54e1e8n%40googlegroups.com.
I'm a bit late to the discussion, but do I understand correctly that this new community verifier is supposed to be a spin-off to MM0/MM1 project? In particular, MM1 code base will be the starting point, proofs won't look like mmj2's proof sheets, and most of tactics/automation will be written in a custom language (as I understood, MM1 uses a scheme-like language)? Also as far as I understand this new verifier should be able to replace an ensemble of tools we use now for CI (or is this a separate project which will include support for ungrammatical databases?).
When I first read this thread, I imagined the project roughly as depicted on Thierry's diagram (a universal core library agnostic of grammar, tactic language etc + PA program using that lib to imitate mmj2 or imitate MM1 and so on), but on the second reading I got the impression that the underlying idea was to base it of MM1 from the beginning. I'm not sure if this is a source of confusion for others, but it is definitely for me, so it would be nice if the intended connection between MM0/MM1 and the new verifier could be clarified.
Yeah, I was somewhat involved in the research behind that paper. I think it's trying too hard to fit imperative style into a proofy language; it's difficult to be direct with that approach and there are certain kinds of constructions that are impossible with it (like getting the value you store in a pointer-keyed hash table back out later). You still need a good compiler to make the code efficient - this was a big problem in lean 3 and lean 4 is solving it at great development expense. Here I think we do better to just let the established programming languages do what they were designed to do.
Hi Stefan, David and all,
Eight months after this discussion was launched I have made what
I think is an important breakthrough: the "grammar" addition to
SMM3 / metamath-knife can now parse all statements of set.mm,
including the complex ones where look ahead is required, into
tree-like "formula" structures. Code is as always available on
my fork for those interested.
On my MacBookPro 2015, parsing the full database takes around 3s
on one single thread, and 1s when multi-threaded. This is roughly
the same cost as the "scopeck" step. Building the grammar for the
parsing, based on the syntactical axioms, only takes around 13ms.
I was surprised how easy it was to introduce multi-threading.
I believe this is the first step to make `metamath-knife` a
library for a new community proof assistant. I want to continue to
evolve the resulting "Formula" structure so that it supports basic
functionalities such as substitution and unification. However I
don't want to go too far beyond that, I think further
functionality shall be placed in the "application" part.
Stefan, David, I would like to soon move on pulling this code
into an official rust crate. You own the repositories for
`smetamath`, respectively `metamath-knife`.
How could we proceed?
Specifically:
PS. smetamath's TODO
lists both grammatical parser (the topic of this mail),
and also outline inference: I've also added outline
inference in the branch 'outline'.
--
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/76f1763b-c048-06ed-92fd-5e8ca45e30e6%40gmx.net.
Hi Mario,
Where did you get the grammar parsing algorithm from?
I had already touched the parsing mechanism in my
previous post. I have not followed any given architecture
but built my own. After the fact, I see that I originally built a
Moore machine, and then mixed it with a Mealy machine. The result
is a parser which does not need to do neither lookahead nor
backtracking, so it works in O(n). This is probably thanks to the
fact that
Here comes the longer explanation:
This works in two steps. First, I'm extracting the grammar
information in the form of a tree. That
tree represents the Moore Machine, where each node is a state of
the automaton, and transitions are made between node based on
input tokens. Once a terminal node is reached, a full construct
has been read and a 'reduce' step is made. Pictures below are
partial graphical representations of that tree / state machine. I
encourage you to follow the link above and browse that tree /
state machine!
The algorithm keeps two states:
For example, when parsing " A C_ B ", the parser would first
encounter the ` A ` token. This makes it shift that token and move
its pointer to node 115, which tells it 'reduce' a `cA` and push
it to its stack.
Next it restarts from the root node of the grammar tree. A class
has been parsed, so it would then move to node 56 and then 'shift'
the next token, ` C_ `. This leads to node 239. Then ` B ` is
parsed recursively. This works just as for the ` A ` token, and `
cB ` is also pushed on the stack, which now contains [ cA, cB ]. `
cB ` is a class, so the machine state pointer moves to node 240,
which tells to reduce a ` wss `. This consumes both ` cA ` and `
cB ` nodes which were on the stack, and replaces them with a
single ` wss[cA, cB] ` node. The stack only contains one formula
node, and all tokens of the expression have been shifted, so
parsing is over.
Actually parsing a statement is the easy part, and the complex part really lies in building the tree correctly. This is done in several passes. The first pass simply takes all syntax axioms, and adds them to the grammar tree. However, there are still several ambiguities to handle:
Below are parser commands I needed to add to set.mm, in order to
give hints to the parser about those ambiguities:
$( Warn the parser about which
particular formula prefixes are ambiguous $)
$( $j ambiguous_prefix ( A => ( ph ;
type_conversions;
ambiguous_prefix ( x e. A => ( ph ;
ambiguous_prefix { <. => { A ;
ambiguous_prefix { <. <. => { A ;
$)
It might have been possible to detect them automatically, but I
took the shortcut to specify them in set.mm. I'll kindly ask those
lines to be included in the official set.mm so that the parser
works!
BR,
_
Thierry
PS. This also means that I have introduced a generic mechanism to
parse $j statements - that shall also be part of the library.
On Aug 15, 2021, at 9:23 AM, Thierry Arnoux <thierry...@gmx.net> wrote:Hi Stefan, David and all,
Eight months after this discussion was launched I have made what I think is an important breakthrough: the "grammar" addition to SMM3 / metamath-knife can now parse all statements of set.mm, including the complex ones where look ahead is required, into tree-like "formula" structures. Code is as always available on my fork for those interested.
On my MacBookPro 2015, parsing the full database takes around 3s on one single thread, and 1s when multi-threaded. This is roughly the same cost as the "scopeck" step. Building the grammar for the parsing, based on the syntactical axioms, only takes around 13ms. I was surprised how easy it was to introduce multi-threading.
I believe this is the first step to make `metamath-knife` a library for a new community proof assistant. I want to continue to evolve the resulting "Formula" structure so that it supports basic functionalities such as substitution and unification. However I don't want to go too far beyond that, I think further functionality shall be placed in the "application" part.
Stefan, David, I would like to soon move on pulling this code into an official rust crate. You own the repositories for `smetamath`, respectively `metamath-knife`.
How could we proceed?Specifically:
- I believe the 'statement parsing' functionality shall be part of a basic Metamath library. Do we have an agreement here? This would mean I could go ahead an issue a PR :-)
- Which repository shall be used and evolve? Stefan's `smetamath`, or David's `metamath-knife` ?
- Since there was broad agreement to build a community project on Rust, could we move the repository into GitHub's Metamath organization? Norm, would you agree?
Below are parser commands I needed to add to set.mm, in order to give hints to the parser about those ambiguities:
$( Warn the parser about which particular formula prefixes are ambiguous $)
$( $j ambiguous_prefix ( A => ( ph ;
type_conversions;
ambiguous_prefix ( x e. A => ( ph ;
ambiguous_prefix { <. => { A ;
ambiguous_prefix { <. <. => { A ;
$)
It might have been possible to detect them automatically, but I took the shortcut to specify them in set.mm. I'll kindly ask those lines to be included in the official set.mm so that the parser works!
Hi Mario,
Indeed set.mm's grammar is unambiguous, and as you write, these
are not true ambiguities, but just prefixes which my initial naive
implementation did not parse correctly. The concept of
"garden-path" was new to me, but describes well this problem: do
you think I shall rename the keyword?
Unfortunately the way I wrote the parser, these are not detected
naturally when building the grammar, and I don't see how they
could. The first pass is simply adds all syntactic axioms to the
machine. Each different construct is added independently, they
don't interfere with each other. In the example of my last mail,
there are 3 different paths, " setvar e. setvar
", " ( wff /\ wff ) ", and
" ( setvar e. class |->
class ) ". Even if the last two share " ( "
as a common prefix, they differ afterwards because one is followed
by a setvar, while the other is followed by a class,
so the state machine goes to diverging states at that point.
I completely agree that it would have been better if the parser
could have figured them out purely based on the indication that
the grammar is KLR(5). The way I initially though about handling
that was to let the parser consider each possible combination of
production against each production, and see if there was a
conflict. However this would have been difficult to implement and
computationally very intensive. Giving those hints was the best
compromise I could find. I'd be happy if you or anyone else wants
to have a closer look at the algorithm and propose improvements!
In any case, I'll try to write down detailed explanations so that
it is not only in emails.
You have a valid point about the risk of breakage when a new syntax is introduced. But these prefix ambiguities (or "garden paths") arose in set.mm only with basic constructs like class builders and maps-to notations, which we don't introduce anymore, or extremely rarely: df-opab was introduced in 1994, df-oprab in 1995, and df-mpt in 2008, and never modified since. So the introduction of such garden paths is once-in-a-decade event :-)
The meaning of the parser command " ambiguous_prefix
X => Y " is "X shadows Y", i.e., one may initially
mistakenly read "X", although "Y" might also be valid for the same
prefix. "X" is always a prefix of a valid set.mm expression, like
" ( x e. A " is a prefix for a mapping-to expression " ( x e. A
|-> B ) ".
As for the syntax of the parser commands, they could also have
been put in quoted strings. The (MM) parser unquotes the string if
it finds quotes, and you can escape quotes, so that the unquoted (
is equivalent with the quoted '('. For a semicolon, you could
write ';', and '\'' for a single quote. The way you write them
also works.
BR,
_
Thierry
--
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/CAFXXJSsVMwevtMAR8i0OB3zbni%3D7g3xho3u17soXpBKYnUw6Rg%40mail.gmail.com.
Hi Mario,
Indeed set.mm's grammar is unambiguous, and as you write, these are not true ambiguities, but just prefixes which my initial naive implementation did not parse correctly. The concept of "garden-path" was new to me, but describes well this problem: do you think I shall rename the keyword?
Unfortunately the way I wrote the parser, these are not detected naturally when building the grammar, and I don't see how they could. The first pass is simply adds all syntactic axioms to the machine. Each different construct is added independently, they don't interfere with each other. In the example of my last mail, there are 3 different paths, " setvar e. setvar ", " ( wff /\ wff ) ", and " ( setvar e. class |-> class ) ". Even if the last two share " ( " as a common prefix, they differ afterwards because one is followed by a setvar, while the other is followed by a class, so the state machine goes to diverging states at that point.
I completely agree that it would have been better if the parser could have figured them out purely based on the indication that the grammar is KLR(5). The way I initially though about handling that was to let the parser consider each possible combination of production against each production, and see if there was a conflict. However this would have been difficult to implement and computationally very intensive. Giving those hints was the best compromise I could find. I'd be happy if you or anyone else wants to have a closer look at the algorithm and propose improvements! In any case, I'll try to write down detailed explanations so that it is not only in emails.
You have a valid point about the risk of breakage when a new syntax is introduced. But these prefix ambiguities (or "garden paths") arose in set.mm only with basic constructs like class builders and maps-to notations, which we don't introduce anymore, or extremely rarely: df-opab was introduced in 1994, df-oprab in 1995, and df-mpt in 2008, and never modified since. So the introduction of such garden paths is once-in-a-decade event :-)
The meaning of the parser command " ambiguous_prefix X => Y " is "X shadows Y", i.e., one may initially mistakenly read "X", although "Y" might also be valid for the same prefix. "X" is always a prefix of a valid set.mm expression, like " ( x e. A " is a prefix for a mapping-to expression " ( x e. A |-> B ) ".
As for the syntax of the parser commands, they could also have been put in quoted strings. The (MM) parser unquotes the string if it finds quotes, and you can escape quotes, so that the unquoted ( is equivalent with the quoted '('. For a semicolon, you could write ';', and '\'' for a single quote. The way you write them also works.
Many thanks for the description of the KLR parser! I'll take the time to read and understand it!
Concerning the parsing of $j comments, I've implemented it in two steps:
This way, any other part, or user of the library also has
access to all parser commands, pre-processed in a very minimal
way.
Concerning the parsing of $j comments, I've implemented it in two steps:
- a first step, which is completely agnostic of the usage, and for which I've followed the Metamath book, chapter 4.4.3 : Additional Information Comment ($j). This states:
Within an additional information comment is a sequence of one or more commands of the form command arg arg ... ; where each of the zero or more arg values can be either a quoted string or a keyword. Note that every command ends in an unquoted semicolon.
This step does not interpret the commands, but simply saves them as list of arguments in the database. At this step, I'm removing the quotes if there were any.
Hi Zheng Fan,
I'd be glad to help you use and understand that program. There were several new developments since that email, and my personal fork might not have been up-to-date, can you please try again with the code on David's branch?
https://github.com/david-a-wheeler/metamath-knife
I hope that project will soon be in a state where it can be moved
to the set.mm GitHub organization!
Also, could you please point me to the version of set.mm and the command line parameters you're using, so that I can try to reproduce the issue?
In order to avoid bothering this list with our possible back-and-forth trying to pinpoint the root cause of the issue, you could also open an issue in that GitHub repository, and we can keep our exchanges there.
A better description of the algorithm is due, I tried to
introduce it in one
of my posts here.
More generally, thank you very much for the attribution, but as
the thread title suggests, the idea is to build a community
verifier. I would not like to see this project as mine but rather
as the community's. This is really actually a community work
starting from Stefan O'Rear's foundaments, with major
contributions from Mario and David. In his original post, Mario
expressed his wish to avoid fragmentation in the community.
The plan is to start a new "community verifier" and build it with those tasks in mind. I think there has been too much fragmentation in verifier land; this makes it very hard for newcomers, especially those that are not especially computer literate such as traditional mathematicians.So the spirit would rather be that instead of building your own verifier/proof assistant, you're welcome to contribute to this community project :-) BR,
_
Thierry
--
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/88c026c9-f20a-4651-ac86-4d138662a8c4n%40googlegroups.com.
Hi all,
I'd like to log some modest progress on a Visual Studio Code assistant, which reuses a lot of Mario's work on MM0, and relies on metamath-knife.
I've put up a small screen recording here,
demonstrating basic hover and go-to-definition support:
BR,
_
Thierry
Hi Glauco,
In MMJ2, here are some methods for mmj.pa.ProofStepStmt:
public String getStepName();
public String[] getHypSteps();
public void setRef(Stmt ref);
public Stmt getRef();
public String getRefLabel();
public Formula getFormula();
public boolean isHypothesisStep();
public boolean isDerivationStep();
So:
Any documentation about MMJ2 should be here: https://github.com/digama0/mmj2/tree/master/doc
In metamath-vspa, I've been using similar names.
BR,
_
Thierry
--
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/7e84b4c0-e4f4-409b-b54d-4d51f4edaf74n%40googlegroups.com.
Hi all,
FYI, I've added a few screenshots to the README file of the metamath-vspa
project, including one with an example of unification at the
bottom of the page (still work in progress..)
So I'm still slowly getting there...
BR,
_
Thierry
- "StepName" would be the name of the step, "72" in your example,
- "HypSteps" would be the essential hypotheses, "71,70" in your example,
- "RefLabel" would be the label of the theorem applied, like "mpbid",
- and "formula" is the formula itself (not shown in your example)
Hi Glauco,
I think I found what you're looking for:
http://mmj2-doc.tirix.org/doc/ProofAssistantGUIDetailedInfo.html
As far as I'm concerned I only have a difference at the
level of the proof step, and then these components, so I did not
have to name that "prefix".
It could be useful to have such a definition of what a
"Metamath Proof File" is. My previous Eclipse plugin (which was
a shell around MMJ2) used the same format, metamath-knife
can output that format, and I'm starting to use the exact same
format in metamath-vspa.
Maybe we could simply write a ".MD" markdown file in
set.mm for filling that purpose?
--
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/4d2b9eb5-5fbb-4a6e-b69f-1045f6806de2n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4a64ad66-71b6-8087-23b9-4ee607d756de%40gmx.net.