a survey of Abella users

[Dale Miller]

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.

[Yuting Wang]

Dear Dale,

The following is my statistics:

64  files   760  objects  9824  loc    : Abella repository
55  files   2541 objects  30795 loc  : The compiler project of my thesis
73  files   724  objects  6585  loc    : My personal repository of abella examples
===================================================================================
192 files   4025 objects  47204 loc   : total

Best,

Yuting

--
You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/abella-theorem-prover/CAGbLtfjhaNUNn%3D5xYufruFaYfuiQkzY3AETvdLLb9bmJQ4H7ag%40mail.gmail.com.