On Sun, Jul 21, 2019 at 6:37 AM Thierry Arnoux <[email protected]> wrote:
> I've been enjoying a lot developing proofs in MM using MMJ2. What would be > the future of that? > mmj2 isn't going anywhere, you can still use it as always, and I plan to continue maintenance on the project (well my maintenance record hasn't been that great... I promise I will release a new version soon). But I have sensed some structural issues with continuing to improve mmj2, and it's quite slow, and being its own editor was a bad idea. So I probably won't be doing much more than bugfixes on mmj2; I'm looking for a more radical improvement that can't be done in the current codebase and that means a new project. > Do you expect that the tools in MM1 will be so advanced that people will > prefer using MM1 instead of MM, or do you expect developments on set.mm > (and iset.mm) to continue in the MM format? > That's the million dollar question isn't it. Assuming this all becomes wildly successful, there are three ways I could see metamath development moving to MM1: 1. MM1 gets a command saying "import the MM database up to theorem X", and then you write some MM1 theorems, and there is a compilation export format for MM. That means that you write the proofs in MM1 but the result is an MM snippet that you can put into set.mm. 2. The MM->MM0 conversion becomes pretty and lossless enough that we use it to do a wholesale conversion of set.mm to MM0, and development continues on set.mm0, and MM0 becomes the new lingua franca. 3. Similarly, MM->MM1 becomes good enough that we convert set.mm to MM1. I think option 2 is very unlikely to happen unless MM0 becomes much more popular than MM, but could be a reasonable long term strategy. MM0 is well specified and has the same focus on multiple verifiers, so I would call it a moral successor to MM. Option 3 has some serious drawbacks wrt compilation speed and the metamath philosophy. I've always said that metamath compiles fast because it stores proofs not proof scripts, but that's exactly what an MM1 file is. There is no built in limit on the complexity of tactics used in an MM1 file, but these can slow down the overall compilation significantly until we look like the lean and isabelle libraries where it takes half an hour to build the library. My advisor has suggested that caching should be used to improve this, but this is a new paradigm. I guess we have some experience with caching in the source tree (the discouraged file), but it could also be used in lieu of those big ASCII blobs in metamath files. > Will it be possible to have developments made in MM1 flow back into set.mm > ? > This would be option 1, which I think is the most likely short term strategy. It allows individual authors to "go MM1" without a groundshift in the community. I may need to have some kind of "metamath compatibility mode" to support this since the logic differs in a few ways and notations would have to be rendered differently, but I think it is doable. > In short, what would be the different development pipelines? > > - [MMJ2] MM -> MM0 -> publication in HOL/lean? > > That's an interesting idea. So far while you can run this pipeline you won't be "giving back" to the HOL community this way - you aren't using any existing HOL theorems but rather producing your own from scratch. Currently this requires a lot of "external" work to get the result into the right form on the target, but I think you could write a new theorem and then get it on the HOL side right away given the continuous nature of the pipeline. I would still call this a work in progress though - I'm not even sure if these other target systems are even interested in this kind of translation, how we can work this into their proofs and so on. > > - [mm0-hs] MM1 -> MM0 -> MM? > > This is more explicitly supported, so I expect it to be fairly good quality as a translation. The formalization project I am working on is simply MM1 -> MM0 with no further translation to MM, although it should not be hard to support a general MM0 -> MM conversion that just drops some of the guarantees on bound variables and definitions. It probably won't look that great though without a lot of work, which is essential for "blending in" if you want to actually do your work in a separate system and translate all the results. On Sun, Jul 21, 2019 at 2:00 PM vvs <[email protected]> wrote: > I've tried it and it seems promising indeed. > > But the whole interface isn't looking very interactive right now. The only > feedback that I can get is editor's pop-up while hovering mouse over a > problematic token. > Suggestions are welcome. So far the only thing I have implemented is diagnostics (the squiggles). Hovers (show me the statement of the theorem) and go-to-definition should be next. By the way, F8 (go to next error) will show you errors inline rather than futzing with hovers, which is good when the error printout is substantial. > And autocomplete isn't very helpful either yet. > I think a context unaware autocomplete should not be so hard, and we will have to see about the speed of the context aware autocomplete. > Of course, the project is in a very early stage and so this is expected. > Are you planning an improved interface for the future and what are > limitations of VSCode extension? > I can in principle do anything listed here: https://code.visualstudio.com/api/language-extensions/programmatic-language-features Let me know if you see anything that would fit well with the proof authoring experience. One bummer is that vscode doesn't support semantic syntax highlighting ( https://github.com/Microsoft/vscode/issues/585), which would have been a great option for improving the syntax highlighting on math blocks and lisp blocks. Another option which Lean uses but doesn't fall under any standard vscode feature is to have a "goal view" which pops up on the right side of the screen and basically shows you the result of (stat) continuously. To do this I would have to extend the vscode extension, which I am loath to do because it decreases the portability of the extension. Currently all the work is being done from mm0-hs as a backend server and communication goes via the language server protocol, which means that it should be easy to set up a similarly featureful editor mode for any other LSP supporting editor, such as emacs. > Also Plan9 interface comes to mind where any text is in fact a widget. > Could you elaborate on this? I haven't used Plan9, what's the interaction story there? 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/CAFXXJSvce8HUFRSYeVX1r_-52WM1tD%2B24ZN0_vPJX5K4UX3abg%40mail.gmail.com.
