Hosting project templates in coq-community?

[ejgallego]

Hi folks,

this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also coq-community/templates#95 ) , in particular as to setup full projects such as the plugin template.

Moreover, we have the current alternative Coq project templates in the wild:

• https://github.com/ejgallego/coq-plugin-template
• https://github.com/palmskog/coq-program-verification-template

How should we organize things? Should we move all the templates to coq-template-foo and have this repository just be an index to all the existing templates, as suggested in the thread?

[Zimmi48]

IMHO you are comparing two very different things. On the one hand, this repository should be considered as a tool to generate and maintain some standard files (e.g. CI) for both new and preexisting projects. On the other hand, the repositories you point to are example projects that demonstrate how to do certain things and can be used as a template to create a new project. (BTW, given that GitHub supports marking a repository as a "template", maybe this should be done for these two repos.) If we wanted, the latter could even include a meta.yml file and include some files that would be auto-generated with the templates here.

[palmskog]

I fully agree with the analysis of Théo, and I even have a local meta.yml for my program verification template repo (which I didn't want to distract people with).

But more generally, how do you feel about hosting template repos like Emilio's and mine in coq-community @Zimmi48? Maybe the proper place for this discussion is in the manifesto repo?

[Zimmi48]

But more generally, how do you feel about hosting template repos like Emilio's and mine in coq-community @Zimmi48? Maybe the proper place for this discussion is in the manifesto repo?

It would totally make sense to host these repos in coq-community indeed! And sure, that would probably deserve a discussion in the manifesto repo. Should we just transfer the current issue over there (since GitHub supports that)? Or is it worth keeping as a separate issue?

[palmskog]

I think we can actually turn the template repos (meant to be forked/copied by devs) into good displays of using our meta.yml format and possibly even use that to drive new functionality. We also get dedicated case studies instead of referring to only "live" projects in the README. In particular, Dune config generation support is not great at all currently.

[palmskog]

@ejgallego so how do you feel about transferring your repo? In my view, the two of us should either both transfer, or none of us transfer. As per above, I think it's a good idea and fits with the idea of coq-community doing collaborative documentation.

We can work on improving the meta.yml handling for Dune in the template repos after the transfers.

[ejgallego]

I am OK transferring if you folks think that's the best choice.

[ejgallego]

Actually something I still didn't figure out, is how to best manage all the different kind of templates that users need; actually they may need more different "variants" than the ones I originally thought of, so I dunno if one repos for template is feasible.

[Zimmi48]

There are two main categories IMHO: configurable templates (that's what we have in the coq-community/templates repository with the objective of covering a large set of use cases) and demonstration templates (this is what your project and Karl's are, and it makes sense that they are quite specialized and do not cover all use cases, people can learn from them and adapt them to their needs).

[palmskog]

I completely agree with Théo here. The main "demonstration template" repo besides mine and Emilio's that we should arguably try to add is a project that extracts verified Coq code to OCaml in a nice way using Dune to build some CLI program, and includes things like testing on the OCaml side. But most other typical use cases can be adapted from scratch using coq-community/templates or the existing demonstration template repos.

[jjhugues]

I can propose a demonstration template for a project that extracts verified Coq code to OCaml using Dune. Mine uses Coq.IO instead of an OCaml stub for parsing CLI arguments though. I would assume you would prefer a demo with OCaml, is that correct?

[palmskog]

@ejgallego please feel free to transfer your Coq plugin template repo to the coq-community organization: https://github.com/ejgallego/coq-plugin-template

After the transfer, I believe we can market this repo better to plugin developers and other interested Coq users. And we can also use it to continually determine best practices in the Dune+OCaml+Coq development workflow.

[ejgallego]

Yes, finally time to transfer it and complete the documentation.

Should I just go ahead and do the transfer?

[palmskog]

Should I just go ahead and do the transfer?

Yes please. After the transfer, I will set up some basic repository metadata (and even a basic meta.yml) if you don't mind.

[ejgallego]

I get an error "You don’t have the permission to create public repositories on coq-community"

There are several ways to solve this, I tried to transfer it to you @palmskog which should solve the issue as you should be able to tranfer it to coq-community, however you already have a fork so I couldn't complete the transfer.

[palmskog]

@ejgallego I invited you to become a member of the organization. If you accept the invitation (check GitHub notifications) you should be able to do the transfer directly to coq-community.

[ejgallego]

Thanks @palmskog , transfer completed.

For the "baseline" 8.17.1 + Dune 3.8.2 we can have a project that:

• composes with multiple packages, installed or in workspace
• produces and consumes packages that are both-way compatible with coq-makefile
• supports findlib-based Coq plugin development, including plugins with complex deps that must be loaded at runtime
• detects native automatically
• the usual Dune stuff (coqdoc, dune coq top, extraction, etc...)

What is NOT working:

• Composing with Coq itself is broken, the fix is not hard but we need some cycles
• if your project depends on stuff on user-contrib and that changes (for example opam update) Dune should rebuild your project, however the test case in Dune repos was looking weird
• Some minor features may be needed to support some projects (elpi, load, etc...)

[palmskog]

I transferred my program verification template repo as well: https://github.com/coq-community/coq-program-verification-template

I think this concludes this issue. People are still welcome to propose new template repos in new manifesto issues.