Théo Zimmermann (Oct 25 2022 at 10:41): 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?
Enrico Tassi (Oct 25 2022 at 11:46):I think I sent the credentials on coq-team
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
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
Théo Zimmermann (Oct 25 2022 at 12:00):For the benefit of others, this is what I have:
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.
Théo Zimmermann (Oct 26 2022 at 08:05):Not hearing feedback is usually a good sign. It means that it works.
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.
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
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.
Michael Soegtrop (Oct 26 2022 at 08:09):Well I hope dune solves this and make will be forgotten mid of next year.
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)
Karl Palmskog (Oct 26 2022 at 08:12):also, IDE support...
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.
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.
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.
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
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.
Paolo Giarrusso (Oct 26 2022 at 20:43):Proof General does _not_ rely on make...
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)
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
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: Jun 03 2023 at 03:01 UTC