[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] MML duplications
Andrzej,
At least one functor registration had been already removed (I mean the
duplication of it).
Yes, the data were taken from MML 1011 (that one at
http://octopi.mizar.org/~mptp/mml/html/), some things maybe outdated.
it is very useful and very important utility.
this one is actually very simple, nothing remotely advanced like the
(type)generalization in MoMM; just string equality after normalization of
the formula
1. I would like it to be called after every revision (good chances that new
repetitions happen).
2. It would be useful tool for reviewers, or for the Athors if they would
rather avoid problems with reviews.
Could be it distributed with Mizar? How long it runs?
the posted data are a byproduct of a MaLARea uniquifier
(http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/MPTP2/MaLARea/script/uniquify.pl?view=markup)
run on all the MPTP top-level items, piped to a htmlizer
(http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/MPTP2/MaLARea/script/htmlize.pl?view=markup)
assuming that the formulas are normalized (like in MPTP) into a file of
lines like:
fof(name,formula).
the Perl code could be just:
perl -e '%h=(); while(<>) { m/^fof.([^,]*),(.*)/; if(exists $h{$2}) {print "$1,$h{$2}\n"} else { $h{$2}=$1}}'
This will take very short time on 100000 entries (about the number of
MML top-level items) - less than one second on my computer.
So the only task is the normalization, i.e. exporting formulas in absolute
notation. I do it for various reasons using XSLT, which is slow in
comparison with Pascal. For all the MML top-level items it would take
probably (tenths of) minutes (I do it for all of MML, not just top-level
items). But if you want it fast, simple, and not dependent on a XSLT
processor, have a Pascal program that prints instead of symbols like "K10"
their absolute name like k3_abcmiz_0 or ABCMIZ_0:func 3 (whatever). Just a
different printing function in "exporter" (if only top-level items are
needed). That should also take only seconds for all of MML.
Regards,
Josef
Josef Urban wrote:
Hi,
at http://octopi.mizar.org/~urban/dupl.html is a list of more than 1000 MML
duplications.
Josef