WG: coq-community template documentation · CUDW 2020

Stream: CUDW 2020

Topic: WG: coq-community template documentation

Assia Mahboubi (Nov 30 2020 at 09:45):

I am interested in understanding better/improving the doc of templates.

Karl Palmskog (Nov 30 2020 at 09:46):

@Assia Mahboubi did you have a specific project you were trying to apply templates on? I could take a look if it's idiomatic.

Assia Mahboubi (Nov 30 2020 at 09:46):

The issue mentioned by @Yves Bertot about libraries is much more complicated I guess...

Karl Palmskog (Nov 30 2020 at 09:47):

essentially, templates are very much WIP

Assia Mahboubi (Nov 30 2020 at 09:47):

@Karl Palmskog Yes, it is https://github.com/math-comp/apery

Christian Doczkal (Nov 30 2020 at 09:47):

WIP yes, but at the same time widely used, no?

Karl Palmskog (Nov 30 2020 at 09:47):

in coq-community, yes, but mostly by the same people who develop them

Assia Mahboubi (Nov 30 2020 at 09:48):

Configuration is not finished because last time I worked on it I consumed all the time I could allocate to this.

Karl Palmskog (Nov 30 2020 at 09:48):

@Assia Mahboubi OK, so your goal would be to generate README, opam, and CI?

Assia Mahboubi (Nov 30 2020 at 09:48):

But the issue is mostly about setting up CI for projects depending on (a large chunk of) MathComp

Assia Mahboubi (Nov 30 2020 at 09:49):

@Karl Palmskog Yes.

Cyril Cohen (Nov 30 2020 at 09:49):

I am interested in this too, let only because whetever I do will have to be integrated with this anyway

Christian Doczkal (Nov 30 2020 at 09:49):

@Assia Mahboubi , what does your project depend on, other than coq-mathcomp-*?

Yves Bertot (Nov 30 2020 at 09:50):

An answer to previous remark by @assia concerning the "complicated question about libraries". I think this is not a documentation problem, so out of topic for this working group.

Assia Mahboubi (Nov 30 2020 at 09:50):

Also, I guess I would like to improve the documentation so that we know exactly what the CI is doing wrt dependencies.

Cyril Cohen (Nov 30 2020 at 09:50):

However, this looks like a topic that is a bit separate from the general documentation WG, should this be a sub-topic?

Cyril Cohen (Nov 30 2020 at 09:51):

I suggest to rename the topic of this discussion to WG: coq-community template documentation shall I?

Assia Mahboubi (Nov 30 2020 at 09:51):

@Christian Doczkal it is depending on CoqEAL, real-closed and bigenough (see https://github.com/math-comp/apery/blob/master/meta.yml)

Karl Palmskog (Nov 30 2020 at 09:51):

you can take a subset of the comments and rename and keep the general WG topic for documentation?

Assia Mahboubi (Nov 30 2020 at 09:52):

And by transitivity on other libraries of course (like paramcoq)

Karl Palmskog (Nov 30 2020 at 09:53):

OK, how about the following. I can set up apery for idiomatic template usage and make a pull request, and we can try to figure what the hard parts were and document them

Christian Doczkal (Nov 30 2020 at 09:54):

The first thing that comes to my mind is using mathcomp images as I do for instance in graph-theory: https://github.com/coq-community/graph-theory/blob/master/meta.yml#L57-L65

Karl Palmskog (Nov 30 2020 at 11:22):

here is my PR with the usual Actions CI: https://github.com/math-comp/apery/pull/1

Christian Doczkal (Nov 30 2020 at 11:38):

Coming back to the actual topic of this WG: there seems to be no documentation for the templates other than the pretty terse README.md and ref.yml, which is also not exactly newcomer friendly. Should we enable the wiki on this project to document the templates, or where should documentation go?

Karl Palmskog (Nov 30 2020 at 11:48):

I'm somewhat averse to wikis. I would aim for adding more to README.md as a first step

Christian Doczkal (Nov 30 2020 at 11:57):

I was just thinking that it may be a good idea to have a human-readable documentation of things like tested_opam_versions and other options, and that, if done properly, this could become too much or too verbose for the README.md

Christian Doczkal (Nov 30 2020 at 11:58):

Also, everyone can edit the wiki without having to go through PRs.

Théo Zimmermann (Nov 30 2020 at 12:31):

Feel free to extend the README and when it becomes too long, we can split it into multiple files.

Théo Zimmermann (Nov 30 2020 at 12:32):

We also have the manifesto's wiki that could provide a general introduction to the templates.

Théo Zimmermann (Nov 30 2020 at 12:32):

But if we want precise documentation, it's indeed best to keep it close to the code, i.e. in the templates' repo.

Karl Palmskog (Nov 30 2020 at 13:14):

I think a lot of complexity with using the templates is specifying all the requirements of the Coq project. Apery has 5+ dependencies, follows a certain naming schema for opam, etc.

Christian Doczkal (Nov 30 2020 at 13:26):

Yes, some help in writing the meta.yml might be nice. It looks like there isn't any skeleton meta.yml in the repository.

Christian Doczkal (Nov 30 2020 at 13:35):

To enable generating files using one such mustache tool, you should thus write a meta.yml file containing the required values.

I think we should, at the very least, curate one or two meta.yml files from projects inside coq-community and direct people to use those as a examples or starting points. The current wording leaves this best-practice implicit.

Karl Palmskog (Nov 30 2020 at 13:36):

we did have some examples originally. However, it's a huge chore to keep them up to date. I think we should simply provide a bunch of links to different projects' meta.yml files.

Christian Doczkal (Nov 30 2020 at 13:38):

Yes, the question is to which. Do we have simpler mathcomp based project than reglang? (that now also uses the repo key for custom images.

Karl Palmskog (Nov 30 2020 at 13:40):

just pick 5 or ten different ones, for example:

https://github.com/coq-community/huffman/blob/master/meta.yml (no deps, simple)
https://github.com/coq-community/gaia/blob/master/meta.yml (multiple deps)
https://github.com/coq-community/stalmarck/blob/master/meta.yml (plugin)

Christian Doczkal (Nov 30 2020 at 13:42):

I would advocate for as few as possible, covering (and mentioning) the features used in the respective projects: custom docker images, deps, single-branch, one branch per coq-version, etc.

Christian Doczkal (Nov 30 2020 at 14:02):

I created an issue for this: https://github.com/coq-community/templates/issues/78
Please feel free to suggest other projects/use-cases. I will make a PR once the list has been agreed upon.

Christian Doczkal (Dec 02 2020 at 14:01):

Karl Palmskog said:

here is my PR with the usual Actions CI: https://github.com/math-comp/apery/pull/1

@Assia Mahboubi After looking at the PR from @Karl Palmskog, could you have a look at the README.md of coq-community/templates and maybe give us some hints as to what is unclear (for someone less familiar with OPAM and CI).

Assia Mahboubi (Dec 03 2020 at 16:35):

Thanks a lot for all your comments. This is really helpful.

Karl Palmskog (Dec 03 2020 at 16:44):

I will do a comment pass as well, but I think we can merge the PR and summarize as an issue in the template repo

Assia Mahboubi (Dec 03 2020 at 16:57):

I had a look (again) at the README file of community/templates, and here are the remarks I can make:

This doc does not list exactly the configuration files/boilerplate that are handled by this template. The example of ACC is very useful but the reader does not know whether it is exhaustive or not.
It would also be useful to recall the purpose of each of the files that can be generated, even if some names seem self-explanatory.
For instance it was not clear to me at the beginning what was the relation between the generated opam config file and the config file I should use to submit a coq opam package.
The sentence "Keeping generated files under version control is not ideal, but README.md has to exist, and generally this is a common practice when using build systems such as Autotools." is only half informative (I am not very familiar with Autotools for instance). I would suggest to rephrase it so as to express which generated files have to be kept under version control.
The previous item is actually also related to the (missing) pointers to the documentation about configuring CI. There is indeed a link to the wiki, but it points to this home page. And it seems to me that the only vaguely related link in the menu on the right is "Continuous integration with nix". This is not very helpful if only because templates's readme sorts CI mechanisms according to travis vs actions vs CircleCI. Also, in the example of your pull request, you generated a coq-ci.yml file, when the wiki page mentions a travis.yml page.
I could not find another place which would document how to choose between the various options of CI.
After some time and questions on zulip I became aware of the coq-docker wiki pages. But it is not easy to find and the relation with templates is not crystal clear (to me at least).

Karl Palmskog (Dec 03 2020 at 16:58):

for the record, ref.yml lists all the affected files

Assia Mahboubi (Dec 03 2020 at 16:59):

@Karl Palmskog sure, I will merge the PR right away. Which content do you have in mind for the issue in the template repo?

Karl Palmskog (Dec 03 2020 at 17:00):

@Assia Mahboubi I will call it something like "Improving template documentation", and I will copy some of what you just wrote and complement with my own observations

Christian Doczkal (Dec 03 2020 at 17:00):

@Assia Mahboubi thank you for your observations.

Assia Mahboubi (Dec 03 2020 at 17:02):

My pleasure! I am also volunteering for small edits in the README of templates (once I understand things better).

Christian Doczkal (Dec 03 2020 at 17:04):

As mentioned above, the first thing I would like to do is to provide some more example meta.yml files for different setups. And indeed, we should probably say that, unless they have a reason to do otherwise, users should choose GitHub actions for CI.

Assia Mahboubi (Dec 03 2020 at 17:04):

But my feeling is that some improvements are also needed in the doc of CI setup for coq projects. A lot of material is already present but not yet as easy to find as one could hope for.

Assia Mahboubi (Dec 03 2020 at 17:05):

(I have to go offline for today, but will have a bit of time to allocate to this tomorrow if relevant).

Christian Doczkal (Dec 03 2020 at 17:06):

With the right meta.yml, CI setup is just a call to generate.sh. At least for projects that don't have special requirements.

Assia Mahboubi (Dec 03 2020 at 17:07):

What is a "special requirement"?

Karl Palmskog (Dec 03 2020 at 17:12):

for example, some projects have multiple opam files that depend on each other

Karl Palmskog (Dec 03 2020 at 17:13):

and we don't support adding system packages (outside opam) to CI as of yet, it has to be done manually in the CI configuration

Karl Palmskog (Dec 03 2020 at 17:13):

generate.sh will not take care of things like this

Assia Mahboubi (Dec 04 2020 at 09:22):

Is this made explicit somewhere in the doc? I could not find it.

Karl Palmskog (Dec 04 2020 at 09:25):

@Assia Mahboubi indeed we lack documentation of limitations, but right now there are many of those, so we probably start by being more thorough about what we can actually do

Karl Palmskog (Dec 04 2020 at 09:29):

@Assia Mahboubi by the way, I noticed that Apery has a "flaky build", i.e., it sometimes fails randomly when doing parallel proving (e.g., make -j8). This is due to coqdep not picking up file dependencies injected by Load commands. Specifically, some of the files under include have Require sentences for other files in the project.

Karl Palmskog (Dec 04 2020 at 09:31):

the topological sort of .v files done by coqdep wil miss some dependencies, and thus it sometimes happen that a file is not compiled by make when it is loaded

Karl Palmskog (Dec 04 2020 at 09:34):

one way this could be fixed manually is to make sure that there are no files under include that Require a file inside the project, i.e., they should at most Require external files.

Karl Palmskog (Dec 04 2020 at 09:35):

however, Dune 1.0 will support running coqdep on files that are only used by Load, i.e., files that may not compile by themselves but are used by other files - I discussed this case with Emilio

Karl Palmskog (Dec 04 2020 at 10:02):

@Erik Martin-Dorel do you maybe have a few minutes sometime today to synchronize on "the state of Coq CI" (and templates) in a BBB breakout room? Sometimes it can be a bit more effective than chat here.

Assia Mahboubi (Dec 04 2020 at 11:03):

Karl Palmskog said:

Assia Mahboubi by the way, I noticed that Apery has a "flaky build", i.e., it sometimes fails randomly when doing parallel proving (e.g., make -j8). This is due to coqdep not picking up file dependencies injected by Load commands. Specifically, some of the files under include have Require sentences for other files in the project.

I know this this unusual and may seem bad practice. But this development is of a bit special nature.

Assia Mahboubi (Dec 04 2020 at 11:06):

Part of certain files have been generated by translating the output of Maple sessions. These files are stored under include. These files need to Require some files of the project, the ones that contain the Coq (counterpart) definitions of some sequences used in the Maple sessions. The Require commands have actually been generated as well.

Karl Palmskog (Dec 04 2020 at 11:08):

yes, it's perfectly fine to organize a project this way, but it's not fully supported by coq_makefile unless you omit all Require for local files in the includedirectory

Karl Palmskog (Dec 04 2020 at 11:09):

basically, project compilation will fail nondeterministically if you try with more parallel jobs than, say, 3

Assia Mahboubi (Dec 04 2020 at 11:10):

I would rather not edit these files manually, because one of the points of this project was to show that it was possible to make the two systems cooperate. So fixing the issue would require editing the script which generates the Coq files from the output of Maple scripts. And that's not something I can do instantaneously.

Karl Palmskog (Dec 04 2020 at 11:11):

I understand, but just be aware of this issue and when Dune with 1.0 support for Coq comes out, Dune can compile the project properly regardless of number of parallel jobs

Enrico Tassi (Dec 04 2020 at 11:12):

In makefile.coq.local one can add lines like

foo.v: extra.bla

to add an extra dependency

Assia Mahboubi (Dec 04 2020 at 11:12):

Thanks for raising the issue indeed. So may be should I (at least temporarily) warn users about this limitation in the README?

Enrico Tassi (Dec 04 2020 at 11:12):

See for example: https://github.com/LPCIC/coq-elpi/blob/a03579e8f3c1d3dfcfe08c3c81a1795b45ede513/Makefile.coq.local#L10
(assuming I got the issue)

Karl Palmskog (Dec 04 2020 at 11:13):

Enrico's solution could work, but will require careful analysis of what is in each include file

Assia Mahboubi (Dec 04 2020 at 11:13):

Ah I was about to raise this question indeed: can I indicate dependencies explicitly to help coqdep?

Erik Martin-Dorel (Dec 04 2020 at 11:13):

Karl Palmskog said:

Erik Martin-Dorel do you maybe have a few minutes sometime today to synchronize on "the state of Coq CI" (and templates) in a BBB breakout room? Sometimes it can be a bit more effective than chat here.

Sure, I think I'll be available at 15:00 UTC+1 to discuss this (and also recap the latest changes I've done with @Théo Zimmermann this morning about docker-keeper, and the changes to come for docker-coq images on next week :)

Assia Mahboubi (Dec 04 2020 at 11:13):

Karl Palmskog said:

Enrico's solution could work, but will require careful analysis of what is in each include file

Do you mean that I should put the transitive closure of dependencies?

Assia Mahboubi (Dec 04 2020 at 11:13):

Otherwise, it should be quite easy.

Guillaume Melquiond (Dec 04 2020 at 11:13):

I would have done it the same way as Enrico, that is, dumping a bunch of dependencies into Makefile.

Enrico Tassi (Dec 04 2020 at 11:14):

you can write

file.v : dep1
dep1 : dep2 dep3

it will close it transitively for you

Karl Palmskog (Dec 04 2020 at 11:14):

@Erik Martin-Dorel OK, let's meet at 15:00 then

Karl Palmskog (Dec 04 2020 at 14:05):

@Erik Martin-Dorel so did you have time to chat a bit in BBB? Room 3?

Erik Martin-Dorel (Dec 04 2020 at 14:06):

yes! sorry for the delay :)

Last updated: Apr 20 2024 at 10:02 UTC