This actually brings up something I’ve been curious about. What metrics does the community use to track the popularity of things like the Snap installer?
I’m curious how people get Coq by the numbers
we have discussed metrics before, but we don't do much currently. We can see how often the tarball on GitHub is downloaded, for example
we can see how often people fetch the Docker images quite easily also (but they currently don't contain the whole platform)
probably there is some dashboard on the snap store, maybe Enrico (Tassi) has access
I wonder if we could talk snapcraft into publishing some numbers :thinking: it looks like they do some amount of data gathering (see the log charts they have for OS breakdown)
I do have access to stats
but I'm away from my pc, so I can't really see them.
I will post them tomorrow.
It would be neat to track month-over-month. There’s a few other platform/growth related metrics I’ve been thinking about too. So many projects 😅 automation would be a boon
What does "weekly active devices" mean? Does this represent people actively using the Snap-installed Coq every week!? :thinking:
So much for not adding trackers inside Coq if the Snap installer is that intrusive :sweat_smile:
from what I remember, a Snap periodically checks for updates, and I guess they log this and record it as "active device"
indeed, it does not mean they use it, but rather that their pc is on.
The fact that almost all users switched almost instantly from 2021.02 to 2021.09 also seems to indicate that most are on the latest track instead of being on a version-specific track...
I wonder if this is not more due to
snap install coq putting you on "latest" than any conscious choice
It is the "default" way of using snaps. Tracks are for "devs", random users (e.g. students trying Coq) should pick latest, IMO.
Some notable packages don't even use tracks, I get my vscode updated even too often ;-)
Partly inspired by this discussion, over the holiday I started building a metrics tracker for Coq and other ecosystems
Right now it only studies GitHub, but I intend to add more data sources to it
Please let me know if there’s anything you’d like to see added, I can see what I can do
Have you ever wondered: :raising_hand: How big is the formal methods open source community? :raising_hand:♀️ How active is it? :raising_hand:♂️ How mature are its projects? Well, let’s find out! Today I’m excited to share FM Growth, a project that tracks stats about FM in open source :tada: https://growth.applied.fm- Tim Carstens (@intoverflow)
one idea is to track the GitHub number of entries for the topic
This represents conscious advertising that a project is using Coq (as opposed to just making a project that has Coq code). Lean has a curated topic too: https://github.com/topics/lean
don't forget to add Standard ML as a language for comparison (it also hosts HOL4)
(I’ve actually got data on a few other languages not shown here (OCaml, Haskell, rust, a half dozen others) but it’s voluminous enough that I only track “repos updated in the last 7 days”)
SML is roughly equivalent to Coq on GitHub per the latest RedMonk report
and it still has a few high-impact projects, like: https://github.com/cakeML/cakeml
Looks like github’s language model tracks SML ✅ this will be an easy addition, thanks!
the blessing and curse of the LCF classic approach: there is no simple way to distinguish source code in the embedded language and the host language (see: OCaml and HOL Light, HOL4 and SML)
Yeah, this deserves a slightly better methodology - one which I believe is possible, but it will require some iteration to get there. But it’s a high priority: this problem impacts other tech areas like SMT and model checking, which both deserve to be tracked as well
(I’m testing a diff that adds Standard ML; it should be pushed to prod before tonight’s pipeline run)
for HOL4, there is one possible heuristic: a file with HOL4 code has to follow the pattern
<name>Script.ml I guess, since SML doesn't even mandate a file extension, to my knowledge)
Would a HOL formalization of Java be called
yeah, that's one possible name, and you would get an SML module called
JavaTheory so you can do:
but jokes aside, the HOL family already has Jinja: https://www.isa-afp.org/entries/Jinja.html
very nice that SML showed up now, it looks comparable to Coq and Ada in the charts I looked at
Last updated: Jan 30 2023 at 11:03 UTC