Stream: coq-community devs & users

Topic: Coq-community templates v2


view this post on Zulip Théo Zimmermann (Feb 15 2022 at 15:55):

Hey @Etienne LAFOND and @Karl Palmskog: do you want to set a time to talk about templates v2?

view this post on Zulip Karl Palmskog (Feb 15 2022 at 15:58):

sure, I'm available (Paris time/CET):

view this post on Zulip Ana de Almeida Borges (Feb 15 2022 at 16:00):

I've been meaning to mention that I forked and changed the templates to be usable in gitlab: https://gitlab.com/ana-borges/templates

view this post on Zulip Ana de Almeida Borges (Feb 15 2022 at 16:00):

Were you thinking of making big changes for v2?

view this post on Zulip Karl Palmskog (Feb 15 2022 at 16:01):

@Ana de Almeida Borges please open an issue in the regular GitHub template repo with that link, something like "GitLab support". We can make this part of the new template requirements.

view this post on Zulip Karl Palmskog (Feb 15 2022 at 16:01):

Ana de Almeida Borges said:

Were you thinking of making big changes for v2?

yes, it's a clean-slate redesign, but we will try to keep the good ideas and CI support, etc.

view this post on Zulip Théo Zimmermann (Feb 15 2022 at 16:02):

In v2, we plan to reimplement the templates from scratch (and in particular to ditch mustache, cf. coq-community/templates#95).

view this post on Zulip Théo Zimmermann (Feb 15 2022 at 16:02):

The goal is to be more flexible to support the diversity of Coq projects that exist and their various requirements.

view this post on Zulip Ana de Almeida Borges (Feb 15 2022 at 16:12):

Cool! Here is a link to the issue I just opened: https://github.com/coq-community/templates/issues/113

view this post on Zulip Etienne LAFOND (Feb 15 2022 at 17:23):

@Karl Palmskog @Théo Zimmermann I'm not available today nor tomorrow so it would be great to meet up thursday.
I'm free all day long so I let you choose the time which is the most convenient if Mr Zimmermann agree with the date.

view this post on Zulip Théo Zimmermann (Feb 15 2022 at 17:24):

Yes, I'm available on Thursday. At the moment, my only constraint is that I'd like to attend the Nix session at 10am.

view this post on Zulip Karl Palmskog (Feb 15 2022 at 17:25):

OK, so we aim for 15:00 on Thursday then. I assume Théo will set up and let us know a Renater link.

view this post on Zulip Etienne LAFOND (Feb 15 2022 at 17:28):

Great! See you Thursday then

view this post on Zulip Karl Palmskog (Feb 17 2022 at 13:11):

@Théo Zimmermann @Etienne LAFOND I'm available from now if you want to start early, otherwise we go for 15:00 as planned.

Do we use a breakout room of the hackathon BBB? Or a renater link?

view this post on Zulip Théo Zimmermann (Feb 17 2022 at 13:12):

We won't be able to use a breakout room if we overlap with the core session schedule of the Hackathon.

view this post on Zulip Théo Zimmermann (Feb 17 2022 at 13:12):

So better to use a Rendez-vous link.

view this post on Zulip Karl Palmskog (Feb 17 2022 at 13:16):

For reference, here is the graphical rendition of my current entity-relationship model of next templates: https://raw.githubusercontent.com/coq-community/templates/v2/Coqtemplate.svg

I use an open source program called DrawIO to construct it, the source lives here: https://github.com/coq-community/templates/blob/v2/Coqtemplate.drawio

view this post on Zulip Etienne LAFOND (Feb 17 2022 at 13:35):

I'm also available right now if you wanna start.

view this post on Zulip Karl Palmskog (Feb 17 2022 at 13:35):

I guess we only wait for Théo to give go-ahead then

view this post on Zulip Théo Zimmermann (Feb 17 2022 at 13:38):

Yes, let's start then: https://rendez-vous.renater.fr/templates-v2

view this post on Zulip Notification Bot (Feb 17 2022 at 14:31):

This topic was moved here from #Coq Hackathon and Working Group, Winter 2022 > Coq-community templates v2 by Karl Palmskog.

view this post on Zulip Karl Palmskog (Feb 17 2022 at 14:33):

OK, I will do a cleanup in the v2 branch in the next hour, and put some notes from the meeting in the README

view this post on Zulip Karl Palmskog (Feb 17 2022 at 14:45):

my suggestion for project name:

Monorepo configuration templates for Coq

view this post on Zulip Karl Palmskog (Feb 17 2022 at 14:46):

or maybe

Monorepo configuration tools for Coq

view this post on Zulip Théo Zimmermann (Feb 17 2022 at 14:46):

Or "Generic" instead of "Monorepo"?

view this post on Zulip Karl Palmskog (Feb 17 2022 at 14:47):

hmm, in that case perhaps:

Repository configuration tools for Coq projects

view this post on Zulip Théo Zimmermann (Feb 17 2022 at 14:49):

"that support more use cases" :grinning:

view this post on Zulip Karl Palmskog (Feb 17 2022 at 15:01):

@Etienne LAFOND if you feel like getting started already this week with something practical, I recommend setting up an opam-based environment with Coq 8.14.1 and Dune and getting the following projects to compile:

view this post on Zulip Karl Palmskog (Feb 17 2022 at 15:03):

you probably want to experiment with both make-based and Dune compilation (Huffman supports both, while Stalmarck only supports Dune, and MathComp only supports make)

view this post on Zulip Karl Palmskog (Feb 17 2022 at 15:07):

@Théo Zimmermann I pushed the "cleaned out" v2 branch now. Maybe you can help with some appropriate LaTeX template/boilerplate for the project description?

view this post on Zulip Théo Zimmermann (Feb 17 2022 at 15:09):

LaTeX template? Only Étienne's report will be written in LaTeX, right? Then this should be kept on the side and he can decide whatever he wants to use (e.g., basic article class).

view this post on Zulip Karl Palmskog (Feb 17 2022 at 15:10):

ah OK, I though maybe you had some academic requirements. We let Etienne decide then (e.g., put something in root or docs directory)

view this post on Zulip Karl Palmskog (Feb 17 2022 at 15:13):

anyway https://github.com/coq-community/templates/tree/v2 looks decent now, now we "just" have to actually do the project work...

view this post on Zulip Théo Zimmermann (Feb 17 2022 at 15:23):

maybe you had some academic requirements

If there are some, I am not aware about them and Etienne would have more info.

view this post on Zulip Théo Zimmermann (Feb 17 2022 at 15:23):

put something in root or docs directory

I think the idea was to keep that in a separate Overleaf project.

view this post on Zulip Karl Palmskog (Feb 17 2022 at 15:28):

OK, Overleaf is fine by me

view this post on Zulip Karl Palmskog (Feb 18 2022 at 09:09):

some ideas for milestones:

view this post on Zulip Théo Zimmermann (Feb 18 2022 at 10:19):

What do you call doc for Hydras & Co.? Not the PDF generation pipeline I hope.

view this post on Zulip Karl Palmskog (Feb 18 2022 at 10:27):

no, I just meant the README.md file as a start, which is currently being pseudo-automatically generated, and we should be able to generate fully automatically.

view this post on Zulip Karl Palmskog (Feb 18 2022 at 10:28):

would be nice to also have some HTML welcome page, index.html, but that might require a generator like pandoc

view this post on Zulip Karl Palmskog (Feb 18 2022 at 10:29):

maybe pandoc has OCaml bindings?

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 12:01):

To my surprise, https://github.com/smimram/ocaml-pandoc exists (no experience): apparently pandoc filters are separate binaries that filter JSON. That avoids Haskell<->OCaml FFI fun...

view this post on Zulip Karl Palmskog (Feb 18 2022 at 12:05):

thanks, I'll add that to our list of resources

view this post on Zulip Karl Palmskog (Mar 03 2022 at 15:12):

some resources pointed out by Emilio that are relevant for templates v2:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 03 2022 at 15:15):

Also https://esy.sh/ may have some templating support

view this post on Zulip Théo Zimmermann (Jun 17 2022 at 12:56):

@Karl Palmskog Could you explain what you had in mind in your diagram about the configuration and name for Continuous Integration Configuration and Continuous Integration System?

view this post on Zulip Karl Palmskog (Jun 17 2022 at 13:04):

@Théo Zimmermann this is the least fleshed out part of the diagram. In databases, you may want to scope configuration data based on the system you are configuring. So for example, name could be table/set with rows/tuples: GitHub Actions, CircleCI, TravisCI. Then in the other entity, you have configuration templates for each of these systems

view this post on Zulip Karl Palmskog (Jun 17 2022 at 13:05):

so you could say it just expresses that you could have a bunch of files following the pattern: ci-name.conf.mustache


Last updated: Feb 04 2023 at 02:03 UTC