Hi Mario Many thanks for the answer > > You probably know this already, but I've been focusing my user interface > stuff on the .mm1 file format. The mmu file format currently doesn't even > have a syntax highlighter, although it could without too much trouble (it's > just an s-expression). But don't make users write mmu files, that's not > nice. That's like asking people to write metamath proofs (the contents of > $p $= proof... $.) by hand. > > Yes. I'll remove the part about editing/looking at mmu files and concentrate on mm0 (I experimented first on mmu because the grammar is easier)
Before I remove it, could you please have a look at the mmu lexer rules <https://github.com/Lakedaemon/mm0-kotlin-tooling/blob/master/intellijIdeaPlugin/src/main/kotlin/org/lakedaemon/mm0/plugin/mmuLexer.flex> and the mmu primary parser bnf <https://github.com/Lakedaemon/mm0-kotlin-tooling/blob/master/intellijIdeaPlugin/src/main/kotlin/org/lakedaemon/mm0/plugin/MMU.bnf> And use those to update the specs of mmu in the official mm0 repository, please. That way, it'll be easier for other developers to adopt mm0 and build their own tools > Writing an .mm1 IDE is not a trivial matter, not least because users want > many things from an IDE, but now there are two, and they both conform to > the LSP specification explicitly so that you can plug them into alternative > editors. So if you like IntelliJ idea, see if you can write a plugin that > communicates to mm0-rs via the json protocol. > I'll look into that > That's what it was designed for. (If you check the marketplace / plugin > database, I will bet you can already find a LSP client implementation for > intelliJ, > Good, it'll make things easier. I am just concerned about one bit : the plugin will probably have to ship native binaries (for multiple platforms). So, it'll be at best more cumbersome that a java/kotlin/groovy/scala solution that runs on the jvm already shipped with intellij idea. But if it is doable, I'll do it. > > Yep, in my mind this is already a solved problem. > I knew it. :) You are a bit like Fermat ("I have just solved a very important problem for mankind") except - he wrote short esoteric blog posts in the margin of his proofs while you write short proofs in your esoteric blog posts - that we can wring answers out of you and implement those solutions in a matter of days instead of centuries, which is definately nice. ;) Imports aren't in the mm0 grammar because raw mm0 should not get that > large. The set.mm translation is supposed to be passed an -f argument to > specify what theorem or theorems in set.mm you care about, and those go > into the mm0 file. > Mmmh. This is nice > Even for very advanced theorems the resulting mm0 files are only a few > hundred KB. The mmb file is much larger, but it is not meant to be edited > by a text editor anyway. The mmu file is even larger because it is a > textual version of the mmb file, but it is also not meant to be edited by a > text editor, and it's rather overwhelming for non-toy problems. > yes. The only people who will want to have a look at mmu/mmb files are probably software developers that want to implement mm0 backed features. The rest of humanity don't need to look inside that. It just needs to work (as excpected). > These issues all come up when working on set.mm as well. > Yes Imports can be used to lop off the "introduction" section of a development > and put it in a different file. As of recently, you can now directly import > a .mmu file into an mm1 file (mmb import support is coming), > ok. I'm not sure I'll ever want to go in the mm1 direction mostly because no one likes to read piles of s-expressions and selection doesn't seem to look favorably on Lisp-backed languages (which might just be a corollary of the first quote) I try to be open minded but I think It'll take a lot of convinving to get me to even open a mm1 file. meaning that you could have a small mm1 file that imports set.mm.mmb and > then adds a few hundred theorems of your own on top. The imported file will > not be rechecked on every keypress, so you get fast response times, and you > can write your local development that way. > > >> Mario recently published a tool that can agregate files with "import at >> their top". >> But that doesn't fix the issue for intellij idea >> >> Maybee, a solution would be to stip the mm0 files from the import >> statement and have a third filetype (.mmerge) >> that holds a structured document telling how to build big mm0/mmu files >> from smaller parts >> > > It sounds like you are proposing > Actually, I'm not proposing. I mostly want to talk about the issue to know what should be best done about it, so that we can reap benefits in the future (and not shed tears later) - You have pondered a long long time and you did a marvelous job at designing mm0, but most of the explanations are still in your mind. I need to know the reasoning behind things before I implement stuff, to do a good job (and also, because I'm curious and not a robot). - it gives people (including me) the opportunity to speak their minds, suggest ideas, give advice and maybe find an even better solution what the .mm0 files in the examples folder already are, which is to say, > mm0 files which are non-conforming because of the addition of import > statements, which can be assembled into conforming mm0 files by the > aggregation utility. > > It is critical that import statements remain a "non-conforming extension" > to the mm0 file format, rather than actually part of the spec, because it > is extremely difficult to formalize file includes in a reasonable manner, > and they aren't needed for scalability at the low level. > Yes. I completely agree now on that (but I had to think about it/try to put myself in your shoes to reach that conclusion). > (The aggregator is careful to preserve things like formatting when > building the mm0 files, so that the output is still readable, yet self > contained, because it is the source of truth for the target axiomatization.) > mm0/mmu/mmb files excell at what they where designed for. Imo, aggregating is an external concern and shouldn't touch mm0/mmu/mmb files and it would be nice to allow everyone (including non mm1 believers) to do the aggregation themselves. So, it would be nice to design a very simple and open solution that would elegantly handle the issue. Also, there is the issue of proof authoring (which is a fundamental part of getting mm0 to succeed). I'm not saying that you should solve proof authoring too. But again it would be nice if everything was in place so that other people could have the basic core features to be able to write authoring tools on top of mm0/mmb. This is quite a lengthy subjects so I'll just throw subjects around in later posts but we already spoke of : 1) spliting mm0 files in short parts (looks like you are ok with that) 2) having custom mm0 files with selected theorems (looks like you already did it) 3) aggregating mm0 files together (already brushed) somehow this reminds me of libraries and software development and screams package managers. :) 4) having a standard file format to allow spec/proof conversion between theorem provers (You already did that) Yet, you say A production quality verifier should probably use a binary file format, but the information contained in the file should be about the same which somewhat implies that you don't intend mmb to become an interchange format, as it would be best for the binary formats to get the best of the platform/endianness it is target at for performances reasons, I guess So, do you intend .mmu files are what will be used to exchange proofs between people, worldwide ? Say, you exchange .mm0 files (in a contest) and the someone A writes proofA on his linux pc, with mephistolus he sends the exported .mmu proof to someoneB on his windows/amiga/weird endianness box to read the proof and import it in hol (or whatever) ? We need a proof exchange format, a format that everyone can target to get inter-compatibility. (and that we can locally convert into a binary format for performance purposes then) Also, I reread your marvelous (but stil esoteric) paper and I now, I can see how awesome the mmb format is (no memory allocations, structures usable in place, wow) and I really, really really want to implement that. So, I'll be pestering you further to get the necessary details so that I can implement a mmb proof checker too. Best regards, Olivier > > 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/24c6ffa2-50aa-484e-b124-413c82d19942%40googlegroups.com.
