Théo Zimmermann (Feb 15 2022 at 15:55): 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?
Karl Palmskog (Feb 15 2022 at 15:58):sure, I'm available (Paris time/CET):
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
Ana de Almeida Borges (Feb 15 2022 at 16:00):Were you thinking of making big changes for v2?
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.
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.
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).
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.
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
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.
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.
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.
Etienne LAFOND (Feb 15 2022 at 17:28):Great! See you Thursday then
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?
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.
Théo Zimmermann (Feb 17 2022 at 13:12):So better to use a Rendez-vous link.
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
Etienne LAFOND (Feb 17 2022 at 13:35):I'm also available right now if you wanna start.
Karl Palmskog (Feb 17 2022 at 13:35):I guess we only wait for Théo to give go-ahead then
Théo Zimmermann (Feb 17 2022 at 13:38):Yes, let's start then: https://rendez-vous.renater.fr/templates-v2
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.
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
Karl Palmskog (Feb 17 2022 at 14:45):my suggestion for project name:
Monorepo configuration templates for Coq
Karl Palmskog (Feb 17 2022 at 14:46):or maybe
Monorepo configuration tools for Coq
Théo Zimmermann (Feb 17 2022 at 14:46):Or "Generic" instead of "Monorepo"?
Karl Palmskog (Feb 17 2022 at 14:47):hmm, in that case perhaps:
Repository configuration tools for Coq projects
Théo Zimmermann (Feb 17 2022 at 14:49):"that support more use cases" :grinning:
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:
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)
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?
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).
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)
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...
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.
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.
Karl Palmskog (Feb 17 2022 at 15:28):OK, Overleaf is fine by me
Karl Palmskog (Feb 18 2022 at 09:09):some ideas for milestones:
Théo Zimmermann (Feb 18 2022 at 10:19):What do you call doc for Hydras & Co.? Not the PDF generation pipeline I hope.
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.
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
Karl Palmskog (Feb 18 2022 at 10:29):maybe pandoc has OCaml bindings?
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...
Karl Palmskog (Feb 18 2022 at 12:05):thanks, I'll add that to our list of resources
Karl Palmskog (Mar 03 2022 at 15:12):some resources pointed out by Emilio that are relevant for templates v2:
dune init command to generate boilerplate for OCaml projects: https://dune.readthedocs.io/en/stable/usage.html#initializing-components-1 Emilio Jesús Gallego Arias (Mar 03 2022 at 15:15):Also https://esy.sh/ may have some templating support
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?
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
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: Jun 03 2023 at 18:01 UTC