The Coq mailing list

[John Beattie <jkb AT jkbsc.co.uk>]

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)
> > > 
> > >