Dear all,
I am sending you this email since I believe that you are using Abella in your research from time-to-time. Kaustuv and I are involved with a grant writing project to build a European-wide community dedicated to building up a library of formal proofs that spans many different proof assistants (Coq, Isabelle, HOL, etc).
We're proposing to write Abella into this proposal. The central technology behind the storage of proofs and their checking will be based on Dedukti. If funding becomes available via this proposal, we're hoping to direct a PhD student to work on problems related to outputting Abella proofs as something Dedukti can check. There are many challenges to that project and we think it's quite interesting to consider.
We have been asked to document the size of the Abella community for this proposal. Compared to say Coq and Isabelle we are, of course, tiny. Still we would like to get an estimate of the number of occasional/serious users and the size of their Abella effort. For the latter, we plan to have a simple count of the following:
- number of .thm files written
- total lines of code (simply the lines in .thm files)
- number of objects (here, only the number of definitions and
theorems)
Can I ask those of you using Abella to estimate these values and send them to me.
I used the following script to compute a rough count of objects (simple counts of definitions and theorems), loc, and file count.
find . -name "*.thm" -print > files.txt
wc --lines files.txt
find . -name "*.thm" -exec grep "Theorem" '{}' \; > objects.txt
find . -name "*.thm" -exec grep "Define" '{}' \; >> objects.txt
wc --lines objects.txt
find . -name "*.thm" -exec wc --lines '{}' \; > loc.txt
I used some separate emacs command to add up all the loc in the loc.txt file into one final value.
I ran this script on three subdirectory on my disk and got the following statistics.
60 files 291 objects 8868 loc : Abella example subdirectory on GitHub
36 files 690 objects 4170 loc : Dale's private assortment of Abella files
396 files 4758 objects 60941 loc : supporting thm files for Dale's paper
==========================================================
492 files 5739 objects 73979 loc : total
Can you send me something similar. I only need the total. Don't worry about precision since we are only need a rough estimate. Also, don't worry too much about double counting (since any distributed counting like this will necessarily involve double counting).
Your response would be most useful if you can send it by Tuesday 21 January 2020. Thanks for your help. -Dale
PS: Feel free to forward this email to Abella users that might not be on this mailing list.