I've got it working, thanks :-) >
This is cool! (I've never even tried it myself, to clone the repository in a new folder) Unfortunately, I still feel I'm a newbie about the npm / package.json / tsconfig.json / launch.json architecture, so your support is really welcome. Please, let me know if / how I could rewrite the installation instructions so that a TS developer would be able to "compile" the "project" :-) > The biggest obstacle to me following David's video in yamma is that the > LOC_AFTER feature of a .mmp file doesn't seem to be working yet. So it > keeps trying to unify and prove reccot from reccot, which is cute and > amusing but not very practical. I assume you would have fixed this by now > if it was easy > I've never been able to make LOC_AFTER to work in mmj2 (but for years I've been using a "custom" version, that Mel wrote / maintained for a limited period of time; does LOC_AFTER work in your mmj2 installation?). I've simplified (I believe) the header structure of .mmp files: Yamma expects a $theorem <label> as a first statement (in the next few days, I plan to feat code to add this line automatically when a ctrl+u is performed; it needs to match the .mmp file name, otherwise a diagnostic / quickFix is displayed) Now, it is used to check that your theorem is consistent with the database version (if you are refactoring an already existing theorem). And it will be used to check that the eHyps labels are coherent (<label>.xxx format), otherwise a warning / quickFix is risen (the quickFix can be to either change the label or to add a statement $allowanyhyplabel , that suppresses this kind of warning, for this .mmp file) Since there's interest, I will add a new statement $locateafter <label> (it shouldn't be hard to implement; but it has to be handled both in StepDerivation, in Search statements, and in StepSuggestions) If you've not tried a Search yet, you can simply invoke it with ctrl + h (same as in mmj2); yamma will analyze the statement under the cursor and populate the search with the most "relevant" symbols (the 3 least frequent ones, if I remember correctly). The "Search Comment:" part is not implemented, yet. And a semantic tokenization for the keywords, is deserved... (near to the top of my current TODO list) > Generating a .mmp file from a .mm file is another possible task for me > once I am properly armed with a parser. > Absolutely (the same as ctrl+g in mmj2). Thierry already had this feature with its rust language server, metamath-vspa https://github.com/tirix/metamath-vspa (Thierry has written a number of impressive theorems and tools!) This feature is really important, I use it a lot with mmj2, both to refactor proofs for existing theorems, and to write proofs for new, but "similar", theorems. But I was planning to leave this feature for the second release of yamma (I'm still working on the first one...) The other "popular" feature that I was planning to leave for the second release, is "renumbering" ( alt + u + r in mmj2) I understand one expects these features to be there, but I cannot keep adding stuff, otherwise I will never be able to publish something for metamathicians to play with (and give some feedback) > Finally, one smaller matter, I notice your unifier puts long terms on a > single line (unlike mmj2) > If I'm not mistaken, mmj2 has two/three modes 1. all statements in single line 2. all statements in multiple lines (with standard formatting) 3. "some" statements in multiple lines (with standard formatting) You can toggle between 1. and 2. using ctrl + o I'm always in mode 1. (single line) and then, selectively, reformat the single statement I'm focusing on (with right click > "Reformat Step: Swap Alt" ; sometimes, you have to do it twice, to actually work) Of course, the plan is to port these 3 modes to yamma, too (only mode 1. is available, now) But now I see what you mean: if you break a statement on multiple lines "by hand", mmj2 keeps your formatting, after a unification. In mmj2 I'm constantly typing ctrl + r to get the "standard" formatting, thus my custom formatting would not survive for long :-) (as a side note, yamma ctrl+u triggers the "DocumentFormatting" language server protocol standard request, I guess that in my mind it's always been derive/unify/reformat) Thanks again for having found the time to play with yamma, your feedback is really precious! Glauco -- 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/70437437-193e-43ab-b576-9ea758811267n%40googlegroups.com.
