Weird, I never had a problem with LOC_AFTER in mmj2. A quick workaround in another prover is, if you're trying to prove something, don't reuse its proof in the database - instead stop reading at that point. After all, if you're trying to prove "foo", then reusing "foo" seems counterproductive :-).
--- David A. Wheeler > On Dec 23, 2022, at 6:55 PM, Glauco <[email protected]> wrote: > > > > 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. -- 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/12E5C5B0-91BE-45AA-B7A6-62571DF85CC3%40dwheeler.com.
