Stream: Coq Platform devs & users

Topic: Number of Snap installations


view this post on Zulip Théo Zimmermann (Oct 25 2022 at 10:41):

@Michael Soegtrop @Enrico Tassi I would like to know the number of Snap users (since Snapcraft tracks this). But I don't have access to these stats AFAIK. Could you please share them or grant me access?

view this post on Zulip Enrico Tassi (Oct 25 2022 at 11:46):

I think I sent the credentials on coq-team

view this post on Zulip Enrico Tassi (Oct 25 2022 at 11:46):

To clarify, there is a coq-term account, and other accounts which can be linked to the same snap

view this post on Zulip Enrico Tassi (Oct 25 2022 at 11:46):

you should have the key to "the master one" in the coq-team mailing list, otherwise just make an account on snapcraft and I'll link it to coq-prover

view this post on Zulip Théo Zimmermann (Oct 25 2022 at 12:00):

For the benefit of others, this is what I have:

view this post on Zulip Michael Soegtrop (Oct 26 2022 at 07:55):

One thing that would interest me is approximately how many students are attending Coq courses each semester and how common technical issues for attendees are - say what fraction of students needs 1:1 tutor assistance to solve technical issues around Coq.

I hear relatively little about this from Coq Platform and I am not sure if this is a good sign or a bad sign. E.g. I would expect that there are requests to include SF in Coq Platform or to include make on Windows. The lack of such requests worries me a bit.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 08:05):

Not hearing feedback is usually a good sign. It means that it works.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 08:05):

FTR I was in contact with someone teaching with Coq to first-year student this year and who said that the installation went smoothly.

view this post on Zulip Karl Palmskog (Oct 26 2022 at 08:07):

maybe relevant: I try to collect links to Coq course material in the Awesome Coq list: https://github.com/coq-community/awesome-coq#course-material

view this post on Zulip Michael Soegtrop (Oct 26 2022 at 08:08):

I just wonder what people do on Windows without make. Originally I had make included, but it used CMD as shell, which needs some minor adjustments to makefiles (rm vs. del e.g.). And people complained that this make did hide some other bash based make people had installed by other means, so I removed it. But for students having to install make and bash doesn't seem feasible.

view this post on Zulip Michael Soegtrop (Oct 26 2022 at 08:09):

Well I hope dune solves this and make will be forgotten mid of next year.

view this post on Zulip Karl Palmskog (Oct 26 2022 at 08:11):

I don't see Dune being a replacement until the problem with checking "partially installed" projects is solved (one wants to allow a project to both be in user-contrib or in the scope of Dune)

view this post on Zulip Karl Palmskog (Oct 26 2022 at 08:12):

also, IDE support...

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 09:58):

IDE support is mainly in the ball of IDE maintainers and contributors now that dune coq top is a thing IIUC.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 09:59):

As for what people do without make, the answer is probably single-file exercise sheets and projects.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 10:00):

If teachers actually need make, then they can recommend using the Platform scripts or WSL. And they usually know about this beforehand.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 10:00):

FTR the stats on universities teaching Coq come from https://github.com/coq/coq/wiki/Universities-teaching-Coq

view this post on Zulip Michael Soegtrop (Oct 26 2022 at 10:02):

As for what people do without make, the answer is probably single-file exercise sheets and projects.

Possibly. But I assume that some lectures are based on SF and I don't see how SF would work like this. Maybe people distribute precompiled VOs for a specific Windows version. I guess I should ask Benjamin.

If teachers actually need make, then they can recommend using the Platform scripts or WSL. And they usually know about this beforehand.

Yes, this might be.

view this post on Zulip Paolo Giarrusso (Oct 26 2022 at 20:43):

Proof General does _not_ rely on make...

view this post on Zulip Paolo Giarrusso (Oct 26 2022 at 20:48):

I haven't tried on Windows, but I think PG's "Compile before Require" worked well enough for quite a while (it's been long)

view this post on Zulip Paolo Giarrusso (Oct 26 2022 at 20:49):

when I was still a bit of a beginner a beginner, Proof General worked well enough that I had no idea about coq_makefile or _CoqProject — the first time I tried browsing 2 files with CoqIDE (to help a colleague, so in 2016 at the latest), I completely failed

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 07:00):

@Paolo Giarrusso : thanks, interesting! I agree that for students it would likely be best if all IDEs would support a similar, preferably technically compatible feature.
CoqIDE has a compile to VO function which does work, but no auto dependency feature. I am not sure about VSCoq.


Last updated: Jan 30 2023 at 10:03 UTC