Hi Antony, feel free to open issues in the repo, I'll be glad to learn from your experience, and give further support to try the extension (see below)
Yes, I would like to see your extension running. That would be cool all by > itself, but also I find it helps me understand code better sometimes if I > can see it running. I'm afraid I'm not familiar with mmj2. Now according > to your instructions: > > - Run `npm install` in this folder. This installs all necessary npm > modules in both the client and server folder > - Open an .mmp file (this triggers the extension) > >> >> - the final goal is to publish it as an extension, in the VSCode marketplace (then it will work by simply installing it) - but for the time being, you should launch it "as a developer" ( F5 / "launch client" is enough, to see it work) - it should open a new VSCode instance, named "Extension Host" (and move your "focus" to the new window); this new VSCode instance has yamma installed as an extension - there you should open an .mmp file (below further details); be sure to have a set.mm file in the same folder (it is used, by default, as the main theory) - this will activate the extension - the extension has several configuration parameters: the most important is a path to a .mm file; by default, it looks for set.mm in the same folder of the .mmp file you've opened - yamma parses set.mm (in the bottom left corner displays the progress notifications: on my low resources Linux VMs, takes about 10 seconds; it also creates a number of statistics that are going to be used by the extension, later on) - a notification is shown when the theory has been parsed - then you will see diagnostics in your .mmp file (for instance, if you are using labels that don't exist, if there are hard or soft dv constraints violated / missing, if there are wff syntax errors and where, and so on) - you will get "on hover" information and semantic tokenization (these are language server protocol "notions") - you should be able to use "step suggestions" (but to get "smart-ish" suggestions, you need a "model": a .mms file that takes about an hour to be updated; there's a script to build it; maybe I will create a repository for it); this feature is the main reason why I wanted to write yamma - you will see syntax suggestions while you write the wff(s) and diagnostics appear as soon as you write a character that "invalidates" the wff - you will get unification and "step derivation" as in mmj2 - you will have some "quick fix" (for instance, to add missing dv constraints) - you will be able to search the theory About .mmp file: this is the format used by mmj2 (I use a slight variation for "meta" instructions, but the proof steps format is identical) If you are interested, I suggest to look at David's amazing video tutorials, on YouTube Here's an example of a .mmp file * A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) h50::mp2.1 |- ph h51::mp2.2 |- ps h52::mp2.3 |- ( ph -> ( ps -> ch ) ) 53:50,52:ax-mp |- ( ps -> ch ) qed:51,53:ax-mp |- ch You can create a .mmp file for any theorem in your .mm file: - launch mmj2 - ctrl + g - it asks for a label - insert the name of the theorem > enter - done As a final note, it's clearly not yet ready for prime time, I'm only writing these pseudo-instructions for you, Antony, because you're familiar with Typescript / npm (much more than I am). If/when it will be published as an extension, everybody will be able to use, by simply installing the extension from the marketplace. As I wrote above, feel free to open issues on the repo, I'll be more than happy (with your help) to write detailed instructions, at least to build / launch it "as a developer". Thanks 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/ce06bfb4-cf5d-408a-be5e-8ec55734c5e8n%40googlegroups.com.
