Stream: Coq Platform devs & users

Topic: Installation metrics


view this post on Zulip 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?

view this post on Zulip Tim Carstens (Dec 15 2021 at 19:36):

I’m curious how people get Coq by the numbers

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Dec 15 2021 at 19:38):

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

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Dec 15 2021 at 20:16):

I do have access to stats

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Dec 15 2021 at 21:14):

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

view this post on Zulip 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:

view this post on Zulip 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"

view this post on Zulip Enrico Tassi (Dec 16 2021 at 11:43):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Dec 16 2021 at 13:24):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 05 2022 at 17:53):

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

view this post on Zulip 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”)

view this post on Zulip Karl Palmskog (Jan 05 2022 at 18:02):

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

view this post on Zulip Karl Palmskog (Jan 05 2022 at 18:03):

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

view this post on Zulip Tim Carstens (Jan 05 2022 at 18:11):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Li-yao (Jan 05 2022 at 18:23):

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

view this post on Zulip 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;

view this post on Zulip Karl Palmskog (Jan 05 2022 at 18:29):

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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 07:01 UTC