On Sat, Feb 22, 2020 at 12:47 PM Olivier Binda <[email protected]> wrote:
> Apparently, it is quite easy to write plugins for intellij idea. > > I just tried and one day later, I had written lexers and primary parsers > for the mm0 and mmu files, with JFlex and GrammarKit (and thanks to mario's > answers and the experience gained by writting home made parsers for > mm0/mmu), > > A few minutes ago, I just pushed accidently my prototype plugin to > https://github.com/Lakedaemon/mm0-kotlin-tooling > I did not push the plugin to the market place yet though (because it > misses lots of functionnalities, I'll do that later when it is ready) > > So, I'll probably be able to develop and distribute a fully feature plugin > adding mm0 and mmu support to intellij idea (which has a free community > version), with the usual intellisense goodness added to it. > This should be a nice alternative to vs-code. > > There is an issue that must be addressed though : > > Intellij idea refuses to open set.mm.mmu outside of raw mode (no syntax > highlighting/advanced features) because it is much too big (at 450MB). > Which is quite understandable. But that means that people will have to > break mmu (and mm0) files into smaller parts to be able > to work with them confortably. > 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. 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. 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, and I've never even used it.) > There is an "import file.mm0;" statement at the top of > https://github.com/digama0/mm0/blob/master/examples/string.mm0 > that could mitigate the issue, by allowing to split files in smaller parts > and to reassemble them when veryfing. > BUT the fact that these statements aren't in the mm0 grammar should render > vscode and intellij idea unable to work with these files (because parsing > these files that hold an invalid statement will fail). > > So,it would be nice to have a solution that allows : > > - reusing mm0/mmu files (like modules) > - limit their length/split them > - agregate them > > Yep, in my mind this is already a solved problem. 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. 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. These issues all come up when working on set.mm as well. 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), 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 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. (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.) 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/CAFXXJSt4n41LZ8dqU5FdB-9wm2%2Buwq%2Bq-1Lyc%2BZso8OpZrNd%3Dw%40mail.gmail.com.
