> I understand that the system has to be trained on a particular version of > set.mm. It seems to me that it would not be that difficult to create a > difference file that identified new theorems, and perhaps new definitions, > that could be fed into this tool. Then it could automatically work on current > versions of set.mm even though it had been trained on older versions.
Totally, I think ideally we let you specify a commit on set.mm or, if there is usage, bite the bullet and simply make the tool stateful and let you upload your own .mm files to work from. This would solve the "underlying kernel versioning" problem entirely. As far as training is concerned, it would be a bit more involved to adaptively train on diffs of set.mm but not completely out of reach. -stan On Thu, Jul 2, 2020 at 4:12 PM David A. Wheeler <[email protected]> wrote: > > This looks very cool, thanks for posting about it here! > > I understand that the system has to be trained on a particular version of > set.mm. It seems to me that it would not be that difficult to create a > difference file that identified new theorems, and perhaps new definitions, > that could be fed into this tool. Then it could automatically work on current > versions of set.mm even though it had been trained on older versions. > > Thoughts? > --- David A.Wheeler > > -- > 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/30A4B5BD-CE3E-45B6-A2B1-836F071A4EA4%40dwheeler.com. -- 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/CACZd_0wuRrRqZ_HLkPo-GsuRq5h_s2P%2BwxKONRnnFLzh3KfOSA%40mail.gmail.com.
