Stream: Coq users

Topic: A "teaching" zulip stream?


view this post on Zulip Pierre Rousselin (Sep 06 2023 at 17:19):

I was wondering if a "teaching" stream about teaching Coq or teaching with Coq would be a good idea.
Would it be interesting to some people?

view this post on Zulip Théo Zimmermann (Sep 06 2023 at 17:22):

This does sound like a good idea as this may encourage people to share stuff that they wouldn't have talked about otherwise.

view this post on Zulip Théo Zimmermann (Sep 06 2023 at 17:22):

Furthermore, there was a recent workshop on teaching (with) proof assistants, so this shows a general interest for this topic.

view this post on Zulip Pierre Rousselin (Sep 07 2023 at 14:06):

If there is sufficient interest, "teaching [with] Coq" should be a good name, thank you @Théo Zimmermann for the suggestion.

view this post on Zulip Pierre Rousselin (Sep 12 2023 at 14:21):

At the moment it does not seem to attract many people, but I created the stream anyway, in the hope that there will be more users after. Since we are going to have the best discussions ever it is bound to happen.
It is called "Teaching [with] Coq".

view this post on Zulip Karl Palmskog (Sep 13 2023 at 11:01):

#Teaching [with] Coq

view this post on Zulip Cyril Cohen (Sep 13 2023 at 12:14):

I arrive after the fact but I would have strongly preferred that the name starts with the string "Coq"

view this post on Zulip Pierre Rousselin (Sep 13 2023 at 12:22):

Cyril Cohen said:

I arrive after the fact but I would have strongly preferred that the name starts with the string "Coq"

Why?

view this post on Zulip Kazuhiko Sakaguchi (Sep 13 2023 at 12:28):

Because the streams are sorted in alphabetical order?

view this post on Zulip Théo Winterhalter (Sep 13 2023 at 12:29):

Then you can "pin stream to top".

view this post on Zulip Cyril Cohen (Sep 13 2023 at 13:59):

Kazuhiko Sakaguchi said:

Because the streams are sorted in alphabetical order?

Yes, and thus "Coq teaching" would appear next to "Coq users" (and other "Coq ..." streams).

Théo Winterhalter said:

Then you can "pin stream to top".

Pinned streams are also sorted alphabetically among themselves :grinning: and it does not solve the problem of visibility of the stream for new users browsing the list.

view this post on Zulip Pierre Castéran (Sep 13 2023 at 14:14):

It may be useful to advertise this stream here (and other places too).

view this post on Zulip Théo Zimmermann (Sep 13 2023 at 15:29):

PRs welcome :smile:

view this post on Zulip Pierre Castéran (Sep 13 2023 at 16:55):

There is already a nice page about teaching Coq, accessible from the Learning about Coq box in Coq home page.
It may be nice to create a box Learning [with] Coq with a small text (like the draft below) and a pointer to CoqInTheClassroomfor more details ?

The teaching [with] Coq Zulip stream is a forum dedicated to various aspects of teaching Coq and use Coq as a tool for teaching various domains which would benefit from the possibility of building formal proofs (such as, but not limited to mathematics or formal methods in computer science).

This is a place where subscribers will share information about course outlines, libraries of examples and exercises, how to make these libraries available to the students, etc.

view this post on Zulip Théo Zimmermann (Sep 13 2023 at 17:45):

The wiki page is directly editable, feel free to add the link and your description there if that's what you had in mind.

view this post on Zulip Pierre Rousselin (Sep 13 2023 at 18:13):

And then maybe the page itself could be linked from coq.inria.fr/documentation.


Last updated: Jun 23 2024 at 04:03 UTC