The amount of material in set.mm has grown quite large and may be overwhelming for someone who just wants to see what is needed to prove a particular theorem of interest.
Organizing set.mm with section headings and splitting it into modules help but only partially address the problem. "show trace_back" does show only the earlier theorems that are needed, but it isn't user friendly in the sense that it can be easily browsed, and it doesn't aggregate the traces of multiple statements. In metamath version 0.192 ( http://us2.metamath.org/index.html#mmprog ), "write source" has a new qualifier, "/extract <label-list>", which will create a self-contained database containing exactly and only the axioms and theorems needed to prove <label-list>, as well as the section headings relevant to them. For example, after "read set.mm", MM> write source xyz.mm /extract exmid,canth will extract everything needed to prove exmid and canth, and nothing more. (See "help search" for the format of <label-list>. For example, "/extract ax-mp~stoic4b" will extract all of propositional calculus.) A possible use for this is to create a miniature local website for the extracted xyz.mm, which can be used as a self study guide, for example. To do this, download metamathsite.zip from the Metamath Home Page, unzip it, create the subdirectory mpeuni, and copy the content of the mpegif subdirectory as well as xyz.mm to it. Assuming the metamath program is in your path, run from inside the mpeuni directory metamath "read xyz.mm" \ "write theorem_list /alt_html /show_lemmas" \ "show statement */alt_html" \ "exit" Some notes: 1. A "~ <label>" in a comment may sometimes refer to a theorem that no longer exists in the extracted database. When this happens, it is converted to a link to the corresponding page on us.metamath.org. 2. If you do "write source xyz.mm /extract *" i.e. extract everything, it doesn't reproduce set.mm exactly although it's functionally equivalent. This is because it extracts the statements individually then uses them to reconstruct the output file, discarding unrelated content. (There are some interesting differences such as orphan $c's, redundant $d's, and headers deleted because there are no statements between them and the next same- or higher-level header.) However, "verify proof *" and "verify markup */f" will pass, and the output of "write theorem_list /a/s" will be identical. 3. File inclusion markup ("$( Begin $[...") and $j comments are currently not included. If people need these, I could try to put them in, but it would take some work to figure out which ones are relevant to the extracted statements. However, the output .mm is primarily intended for read-only display purposes rather than development. 4. If you are puzzled about why an apparently unrelated earlier theorem is included, use the "/to" option of "show trace_back". -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b4ddf2bb-0a74-4942-bbb6-1d5d9c4fad23n%40googlegroups.com.
