While my style is not the same as everyone's, it is rare that I go into set.mm in a text editor without knowing more or less what I plan to do (add a new theorem to prove, edit a comment, etc.). I use the web pages to study proofs when I know the label but rarely search with e.g. google. I use occasionally use grep on set.mm although sometimes it can be annoying because of all the graphics characters that need to be escaped.
For browsing, searching, getting information about usage, dependencies, etc. I spend much of my time in metamath.exe. The main commands for that purpose are 'search', 'show usage', 'show trace_back', 'show statement', 'show proof'. See 'help search', 'help show usage', etc. and study the help pages. Most of them have qualifiers to help specify the output you want to see. Here are some things I use frequently: While not as rich as general regexes, labels can have wildcards * (match zero or more) and ? (match one), and multiple wildcard expressions can be separated by commas (no spaces) such as 'search *abc*,*def* ...'. Math expressions in 'search' can have wildcards $* and $? (which can be abbreviated $ and ?, provided ? is not used in a math token). The $? wildcard is peculiar; it means match one character in a token, not match one token; so "( ?? -> ?? )" will match "( ph -> ph )" but "( ? -> ? )" won't match anything. Label ranges can be specified with <label>~<label>. The '/comment' qualifier for 'search' means search comments. '/join' means also search the $e hypotheses of a $p statement, joining them into a long string of tokens before the search: "search * 'A = B $ |- $ C_'/join" will match sseq1i, sseq2i, sseq1d, etc. 'show usage' has a '/recursive' qualifier to show all direct and indirect uses of a statement. 'show trace_back ... /axioms /match ax-*' shows the axioms a proof depends on. 'show trace_back ... /to ...' will show just the path back to a specific statement, useful for e.g. debugging the unwanted usage of a certain axiom. 'show statement ... /comment' includes the comment above the statement. Command keywords can be abbreviated e.g. 'sh tr' for 'show trace_back' as long as they are unambiguous. This can save a lot of typing. Single or double quotes are needed around multiple tokens, but if a quote ends the line you can omit the trailing quote character to save typing: "search * '|- ph" will implicitly mean ""search * '|- ph'" If you are using gcc to compile metamath, it's almost essential to call it via rlwrap so that you have command line editing, up-arrow command line history etc. The pre-compiled metamath.exe for Windows has Windows-style command-line history built in. I hope this helps a little. Norm On Monday, March 2, 2020 at 4:50:41 AM UTC-5, Jon P wrote: > > Glad to find something helpful :) > > Re searching maybe an example would be helpful. So I was looking through > the web page and scrolled up to ghomid > <http://us.metamath.org/mpeuni/ghomid.html> and I wanted to find if the > same concept is proven elsewhere. I guess I'd appreciate a tutorial for how > others would go about that. > > The sort of things I do: > > Open set.mm in a text editor and ctrl+f for specific phrases, like group > homomorphism and then check the results. > Try to open what might be relevant pages on the website and scroll through > them and read to see if there are any there, this can be time consuming. > Search google in the hopes it will find the right page on the website. > > Things maybe I should try more of if they are better: > > Using the MMJ2 search function. > Using metamath.exe search function. > > I think the right partner for it is ghmid > <http://us.metamath.org/mpegif/ghmid.html> which I found by writing a > python script which goes through set.mm and finds all theorems which > contain "group", "homomorphism" and "identity" in their description. > > I wrote a script which can compare the descriptions of two statements for > general similarity however as you can see they are sufficiently differently > worded to mean that technique didn't work so well. > > In general any tips on searching would be really appreciated, thanks :) > -- 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/bbbba8bf-c368-4601-b7f3-ab14324f8a87%40googlegroups.com.
