Stream: Coq users

Topic: coqpl dev session


view this post on Zulip Gaëtan Gilbert (Jan 20 2024 at 11:24):

the code for notation toggle supports local and export localities (load_function = noop)

view this post on Zulip Gaëtan Gilbert (Jan 20 2024 at 11:47):

does asking on zulip not work to get help with notations instead of private emails?

view this post on Zulip Karl Palmskog (Jan 20 2024 at 11:54):

for the record, questions about using/defining notations are best asked in the stream #Coq users, while questions on enhancements of the notation feature can go in #Coq devs & plugin devs. If in doubt, ask in the Zulip stream that seems to fit best and we (I) will move it to the right stream

view this post on Zulip Karl Palmskog (Jan 20 2024 at 11:56):

hopefully CoqPL organizers can indeed recommend the Zulip as the recommended first stop for any Coq-related questions/concerns

view this post on Zulip Gaëtan Gilbert (Jan 20 2024 at 11:57):

maybe this thread should be moved to the users stream

view this post on Zulip Notification Bot (Jan 20 2024 at 11:58):

This topic was moved here from #Coq devs & plugin devs > coqpl dev session by Karl Palmskog.

view this post on Zulip Gaëtan Gilbert (Jan 20 2024 at 12:00):

I like make
also I found its doc to be pretty good https://www.gnu.org/software/make/manual/make.html

view this post on Zulip Karl Palmskog (Jan 20 2024 at 12:03):

again for the record, it works fine (and is actually a good idea) to have both Dune and make/coq_makefile builds in the same project, here is an example: https://github.com/coq-community/coq-program-verification-template#file-and-directory-structure

view this post on Zulip Karl Palmskog (Jan 20 2024 at 12:05):

for people not at POPL (like me), here is the CoqPL stream: https://www.youtube.com/watch?v=YlVqyxU8lkg

view this post on Zulip Gaëtan Gilbert (Jan 20 2024 at 12:12):

Discussions of ltac1 vs ltac2 sometimes feel like bash vs python discussions to me.
I mean the sort of discussion where people say "if you have a shell script more than 50 LOC rewrite it in a real language like python"
yet AFAIK most people still use some posix+ shell for regular interaction (calling ls etc) not python
so I wonder if that part of the analogy will also apply to ltac1/ltac2 such that people will keep using ltac1 for interactive proofs for a long time but use ltac2 to construct the tactics

view this post on Zulip Karl Palmskog (Jan 20 2024 at 12:16):

I think the refman already gives advice to this effect, i.e., it recommends using Ltac2 for writing tactics, but maybe this mode of use (keep Ltac1 for proof scripts but always use Ltac2 for standalone tactics) should be highlighted/demonstrated more in other resources as well, e.g., Software Foundations and in Coq-community projects

view this post on Zulip Gabriel Scherer (Jan 20 2024 at 12:30):

I posted my notes and the Q/A session on Discuss: https://coq.discourse.group/t/notes-from-the-coqpl-2024-q-a-session/2183


Last updated: Jun 13 2024 at 21:01 UTC