The Coq mailing list

[thomas lamiaux <thomas.lamiaux AT ens-paris-saclay.fr>]

Hi everyone,
Thanks for showing interest.

The goal of the project is among others to turn folklore into knowledge.
This includes promoting good practices and making non-expert users aware 
of common pitfalls.
For instance, as shown by the Coq survey, expert users tend to use very 
different
tools than beginners, usually for good reasons. With this project, we 
hope to reduce this gap.

Considering meta-programming, we are supposed to have a section 
dedicated to it: Ltac2, Mtac, MetaCoq, CoqElpi etc...
Once, we'll have good tutorials and how-to about meta-programming 
showcasing "all" that is possible,
there should already be much less attempts to write plugins in Ocaml for 
basic meta-programming that e.g. basic Ltac2 would cover.
That is already a lot to cover, but if there is a need from the community,
there could additionally be tutorial and how-to guides about 
meta-programming in Ocmal,
targeting more expert users and with a bunch of disclaimers towards 
beginners.

Once written, tutorials and how-to guides should be relatively stable as 
most features do not change on a day to day basis.
However, until then, tutorials and how-to guides takes a lot of time to 
write,
so we are necessarily dependent on contributions, and the project will 
progress along with them.

Best,
Thomas Lamiaux

On 22/07/2024 09:58, John Beattie wrote:
> Can I suggest a short page based on the below paragraph?  It is useful for a
> beginner to be pointed away from something dodgy, with clear reasons.
>
> Best regards,
> John
>
> On 2024-07-22 08:08 +0200, Pierre Roux wrote:
> > About plugins, we have to be very careful that we absolutely don't want
> > to invite users to write plugins if they don't need it. Most use cases
> > of plugins are nowadays covered by metalanguages such as Ltac2 or coq-elpi
> > that should offer a much better experience in terms of maintenance
> > (OCaml plugins depend on Coq API that is unstable and breaks at each new
> > version). So considering the limited use cases, maybe we just don't need
> > additional teaching material here.
> >
> > Le 2024-07-22 07:48, Iaroslav Baranov a écrit :
> > > Hi Thomas!
> > >
> > > Thank you very much for your effort to make coq more easy to learn! The
> > > tutorial on Search and its tricks / advanced features is especially
> > > useful
> > > for many coq users.
> > >
> > > Do you have plans on creating any similar tutorials on coq plugin
> > > writing
> > > in OCaml? I've recently decided to learn it, but found only 4
> > > non-interactive demo projects. Or maybe you can recommend some if they
> > > do
> > > exist somewhere
> > >
> > > Best regards
> > >
> > >
> > > On Thu, Jul 18, 2024, 4:47 PM thomas lamiaux <thomas.lamiaux AT inria.fr>
> > > wrote:
> > >
> > > > Dear Coq users and developers,
> > > >
> > > > We would like to shed some light on our new project "Coq Platform
> > > > Doc".
> > > > Our goal is to provide an online compilation of short, practical and
> > > > interactive
> > > > tutorials and how-to guides about Coq and the Coq Platform. We wish
> > > > this
> > > > content
> > > > to be part of the upcoming Rocq website. A detailed description of the
> > > > project can
> > > > be found in our Coq Enhancement Proposal (CEP) here:
> > > > https://github.com/coq/ceps/pull/91
> > > >
> > > > The first few tutorials are available as well as a (very preliminary)
> > > > online
> > > > interface here:
> > > > https://www.theozimmermann.net/platform-docs/
> > > > (note that this is a temporary URL that will cease to be available
> > > > once the tutorials are migrated to the official Coq organization)
> > > > At this moment, it contains:
> > > > - a Search tutorial
> > > > - a Basic library file and module management tutorial
> > > > - 3 tutorials about the Equation plugin
> > > > More will follow, especially with your help!
> > > >
> > > > There is a dedicated Zulip channel to discuss and participate:
> > > > https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs
> > > > The preliminary git repository is
> > > > https://github.com/Zimmi48/platform-docs
> > > >
> > > > Any contribution would be greatly appreciated and we welcome in
> > > > particular:
> > > > - help to improve or write tutorials or how-to guides
> > > > - comments or feedback on the project or existing tutorials or your
> > > > needs
> > > > - new tutorials about your favorite feature/plugin
> > > > - help to turn folklore or secret powers into common knowledge
> > > > - propositions to enhance interactive and non-interactive interfaces
> > > > - reviews of our CEP
> > > >
> > > > Do not hesitate to contact us, if you are interested in this project!
> > > >
> > > > Formally yours,
> > > > --
> > > > Thomas Lamiaux (@thomas-lamiaux),
> > > > Pierre Rousselin (@Villetaneuse),
> > > > Théo Zimmermann (@Zimmi48)