On Sat, Nov 21, 2020 at 10:54 AM Glauco <[email protected]> wrote:
> 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 think you can see why I'm not really interested to build on the architecture of mmj2. Sure it has a lot of good features, but it is tied to way too many things about java and the editor interaction itself that make it difficult to address these structural problems through ongoing maintenance. (I say this as someone who tried to do just that for a few years.) I don't think the features of mmj2 are so special they can't be replicated elsewhere, but also I think there are some new avenues to explore, and I'm not sure I want to make an mmj2 clone in the first place. The "edit my code" interaction mode makes everything synchronous, which is not good (and also unlike every programming language IDE I've ever seen). 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. > 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. 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. On Sat, Nov 21, 2020 at 12:47 PM vvs <[email protected]> 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. On Sat, Nov 21, 2020 at 2:47 PM David A. Wheeler <[email protected]> wrote: > On Nov 20, 2020, at 3:02 PM, Mario Carneiro <[email protected]> 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. > I should amend "verifier" -> "verifier or proof assistant" in the last two sentences. Neither the verifiers nor the proof assistants are being developed. New verifiers occasionally come out, but there isn't a pressing need for them, it's mostly because it's an easy thing to do as a personal project. You can argue that verifiers don't need upkeep, although most of them could still be improved by implementing more of metamath's optional features, but I agree the main problem is that the *proof assistants* aren't being developed. > 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. > That all sounds doable, assuming we can get a handle on the web page generation task itself. 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. > FYI I defined the term "grammatical database" in my paper "Models for Metamath" and usually use it to refer to the combination of unambiguous grammar and context free productions for grammatical type codes (which is what you need to ensure that parsing works and has the intended meaning). > 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.) > 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. > I'm not really sure where this impression comes from. I don't think I know any system that doesn't have some way of constructing proofs in all directions. In MM1, proofs are provided as "refine scripts", which look basically like terms, where a theorem is the head of an application and the arguments are the subproofs. If you want to do a subproof, you can use the "have" tactic, where you say (have 'h $ type $ 'subproof) where $ type $ is the statement of the theorem and 'subproof is the proof. You can also use _ as the proof so that it becomes a new goal and you can prove it in your own time. 'h is the name of the newly proved step, which you can later refer to in the main part of the proof. This is somewhat different from mmj2 style, where every step is on equal footing; here most steps have no names, so step reuse is confined to just a few important statements. (However, note that internally all steps are deduplicated, so any step that is proved twice will result in only one step being produced.) > 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. That's worked quite well for lean, and MM1 uses many of the same techniques as I mentioned. There is of course also general purpose automation that can be implemented in the prover itself, but it's pretty hard to say anything about metamath databases in general. I have some abortive work on an FOL mode for MM1, where the tactic language itself gains some knowledge of the classical logical connectives so that you can use a lambda-calculus-like syntax to do proofs (this is bikesheddable though; lean uses tactics like "intro" and "cases" to do logical manipulations and that's an option too). 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. > I think this ties in to the earlier point about using it as a library. Interop is good. 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 (,). > One option would be to allow introducing new notations, for example "empty" for (/), that get baked out in the final proof. That can be part of a more comprehensive syntax mapping to something more flexible; it would be nice to get something a bit more like a regular programming language syntax. MM1 suggests a number of modifications in this direction but I'm not wedded to the particular design decisions there. We can even do like lean and go full unicode. 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? > 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. On Sat, Nov 21, 2020 at 3:34 PM [email protected] <[email protected]> wrote: > " 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. > 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. On Sat, Nov 21, 2020 at 6:01 PM David A. Wheeler <[email protected]> wrote: > 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. > This is definitely on my radar. I don't even think it would be that hard to do with mm0-rs, although one has to pick a web IDE and make that work which is a bit tricky. Another cool idea I'm playing with is explorable MM1 documents, where you can view more information on proofs by clicking on them, kind of like the metamath web pages but more interactive and generated on the fly. I think all the technical factors to make this happen, even to generate everything from CI, are in place; there are just a lot of open design questions. Mario -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsvHaG1KtnCsmUtLctjDKw60pU99aGeMFSheOF0kB94kQ%40mail.gmail.com.
