Dear all, We have extended Proof General interface with a new functionality that allows one to statistically analyse various patterns arising in Coq/SSReflect proofs. Finding common patterns in proofs may be used as a guidance in big proof developments across different users, as well as for educational/training purposes. We have successfully tested it on several examples and libraries, and are now looking for more users!
The tool will not alter your normal ProofGeneral routines -- but you will notice ProofGeneral will feature an extra option for Proof Statistics. More information can be found here: http://www.computing.dundee.ac.uk/staff/katya/ML4PG/ We will be happy to hear your feedback. Best, Jónathan Heras and Katya Komendantskaya The University of Dundee is a Scottish Registered Charity, No. SC015096.
_______________________________________________ ProofGeneral mailing list ProofGeneral@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral
