Hey @Etienne LAFOND and @Karl Palmskog: do you want to set a time to talk about templates v2?
sure, I'm available (Paris time/CET):
I've been meaning to mention that I forked and changed the templates to be usable in gitlab: https://gitlab.com/ana-borges/templates
Were you thinking of making big changes for v2?
@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.
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.
In v2, we plan to reimplement the templates from scratch (and in particular to ditch mustache, cf. coq-community/templates#95).
The goal is to be more flexible to support the diversity of Coq projects that exist and their various requirements.
Cool! Here is a link to the issue I just opened: https://github.com/coq-community/templates/issues/113
@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.
Yes, I'm available on Thursday. At the moment, my only constraint is that I'd like to attend the Nix session at 10am.
OK, so we aim for 15:00 on Thursday then. I assume Théo will set up and let us know a Renater link.
Great! See you Thursday then
@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?
We won't be able to use a breakout room if we overlap with the core session schedule of the Hackathon.
So better to use a Rendez-vous link.
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
I'm also available right now if you wanna start.
I guess we only wait for Théo to give go-ahead then
Yes, let's start then: https://rendez-vous.renater.fr/templates-v2
This topic was moved here from #Coq Hackathon and Working Group, Winter 2022 > Coq-community templates v2 by Karl Palmskog.
OK, I will do a cleanup in the
v2 branch in the next hour, and put some notes from the meeting in the README
my suggestion for project name:
Monorepo configuration templates for Coq
Monorepo configuration tools for Coq
Or "Generic" instead of "Monorepo"?
hmm, in that case perhaps:
Repository configuration tools for Coq projects
"that support more use cases" :grinning:
@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:
you probably want to experiment with both
make-based and Dune compilation (Huffman supports both, while Stalmarck only supports Dune, and MathComp only supports
@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?
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
ah OK, I though maybe you had some academic requirements. We let Etienne decide then (e.g., put something in root or
anyway https://github.com/coq-community/templates/tree/v2 looks decent now, now we "just" have to actually do the project work...
maybe you had some academic requirements
If there are some, I am not aware about them and Etienne would have more info.
put something in root or docs directory
I think the idea was to keep that in a separate Overleaf project.
OK, Overleaf is fine by me
some ideas for milestones:
What do you call doc for Hydras & Co.? Not the PDF generation pipeline I hope.
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.
would be nice to also have some HTML welcome page,
index.html, but that might require a generator like pandoc
maybe pandoc has OCaml bindings?
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...
thanks, I'll add that to our list of resources
some resources pointed out by Emilio that are relevant for templates v2:
dune initcommand to generate boilerplate for OCaml projects: https://dune.readthedocs.io/en/stable/usage.html#initializing-components-1
Also https://esy.sh/ may have some templating support
@Karl Palmskog Could you explain what you had in mind in your diagram about the
name for Continuous Integration Configuration and Continuous Integration System?
@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:
TravisCI. Then in the other entity, you have configuration templates for each of these systems
so you could say it just expresses that you could have a bunch of files following the pattern:
Last updated: Jun 03 2023 at 18:01 UTC