May be some code could be written, as an alternative to /extract (it extracts some statements that are not needed and, in some cases, it does not extract some syntactic axioms that would be useful for proof assistants).
In the meanwhile, this regexp works well in VSCode, to remove all comments (replace it with an empty string) \$\((.|\n)+?\$\) Then this regexp ^$\n can be used to remove empty lines and get a "compact" theory. Glauco Il giorno venerdì 24 giugno 2022 alle 14:19:00 UTC+2 Glauco ha scritto: > 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/73f1a636-beaf-4f63-b972-8ec6f82d5495n%40googlegroups.com.
