Stream: Coq Platform devs & users

Topic: Installation metrics

Tim Carstens (Dec 15 2021 at 19:35):

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?

Tim Carstens (Dec 15 2021 at 19:36):

I’m curious how people get Coq by the numbers

Karl Palmskog (Dec 15 2021 at 19:36):

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

Karl Palmskog (Dec 15 2021 at 19:37):

we can see how often people fetch the Docker images quite easily also (but they currently don't contain the whole platform)

Karl Palmskog (Dec 15 2021 at 19:38):

probably there is some dashboard on the snap store, maybe Enrico (Tassi) has access

Tim Carstens (Dec 15 2021 at 19:39):

https://snapcraft.io/coq-prover

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)

Enrico Tassi (Dec 15 2021 at 20:16):

I do have access to stats

Enrico Tassi (Dec 15 2021 at 20:17):

but I'm away from my pc, so I can't really see them.
I will post them tomorrow.

Tim Carstens (Dec 15 2021 at 20:20):

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

Enrico Tassi (Dec 15 2021 at 21:14):

Screenshot-from-2021-12-15-22-13-52.png

Théo Zimmermann (Dec 16 2021 at 09:48):

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:

Karl Palmskog (Dec 16 2021 at 09:50):

from what I remember, a Snap periodically checks for updates, and I guess they log this and record it as "active device"

Enrico Tassi (Dec 16 2021 at 11:43):

indeed, it does not mean they use it, but rather that their pc is on.

Théo Zimmermann (Dec 16 2021 at 13:15):

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...

Karl Palmskog (Dec 16 2021 at 13:16):

I wonder if this is not more due to snap install coq putting you on "latest" than any conscious choice

Enrico Tassi (Dec 16 2021 at 13:24):

It is the "default" way of using snaps. Tracks are for "devs", random users (e.g. students trying Coq) should pick latest, IMO.

Enrico Tassi (Dec 16 2021 at 13:24):

Some notable packages don't even use tracks, I get my vscode updated even too often ;-)

Tim Carstens (Jan 05 2022 at 17:44):

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

https://twitter.com/intoverflow/status/1478503717162741763

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)

https://growth.applied.fm

Karl Palmskog (Jan 05 2022 at 17:47):

one idea is to track the GitHub number of entries for the topic coq: https://github.com/topics/coq

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

Karl Palmskog (Jan 05 2022 at 17:53):

don't forget to add Standard ML as a language for comparison (it also hosts HOL4)

Tim Carstens (Jan 05 2022 at 18:01):

Good idea

(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”)

Karl Palmskog (Jan 05 2022 at 18:02):

SML is roughly equivalent to Coq on GitHub per the latest RedMonk report

Karl Palmskog (Jan 05 2022 at 18:03):

and it still has a few high-impact projects, like: https://github.com/cakeML/cakeml

Tim Carstens (Jan 05 2022 at 18:11):

Looks like github’s language model tracks SML ✅ this will be an easy addition, thanks!

Karl Palmskog (Jan 05 2022 at 18:18):

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)

Tim Carstens (Jan 05 2022 at 18:20):

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

Tim Carstens (Jan 05 2022 at 18:21):

(I’m testing a diff that adds Standard ML; it should be pushed to prod before tonight’s pipeline run)

Karl Palmskog (Jan 05 2022 at 18:22):

for HOL4, there is one possible heuristic: a file with HOL4 code has to follow the pattern <name>Script.sml (or <name>Script.ml I guess, since SML doesn't even mandate a file extension, to my knowledge)

Li-yao (Jan 05 2022 at 18:23):

Would a HOL formalization of Java be called JavaScript.sml?

Karl Palmskog (Jan 05 2022 at 18:24):

yeah, that's one possible name, and you would get an SML module called JavaTheory so you can do:

open JavaTheory;

Karl Palmskog (Jan 05 2022 at 18:29):

so JavaScript.sml is only JavaScript in theory, in practice it's a Java theory

Karl Palmskog (Jan 05 2022 at 18:31):

but jokes aside, the HOL family already has Jinja: https://www.isa-afp.org/entries/Jinja.html

Karl Palmskog (Jan 07 2022 at 15:08):

very nice that SML showed up now, it looks comparable to Coq and Ada in the charts I looked at

Last updated: Oct 13 2024 at 01:02 UTC