Is it possible to automatically remove all comments from the extracted theory?
I need to build "small" theories for unit testing my code. I can, of course, pipeline the /extract step with a subsequent /removeComments step (if the "remove comment" feature is present in metamath.exe) Thanks in advance Glauco Il giorno sabato 5 settembre 2020 alle 05:04:01 UTC+2 Norman Megill ha scritto: > 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5a798fc3-9f95-4746-aaac-faab1f7b0cb9n%40googlegroups.com.
