Stream: CUDW 2020

Topic: WG: coq-community template documentation


view this post on Zulip Assia Mahboubi (Nov 30 2020 at 09:45):

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

view this post on Zulip 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.

view this post on Zulip Assia Mahboubi (Nov 30 2020 at 09:46):

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

view this post on Zulip Karl Palmskog (Nov 30 2020 at 09:47):

essentially, templates are very much WIP

view this post on Zulip Assia Mahboubi (Nov 30 2020 at 09:47):

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

view this post on Zulip Christian Doczkal (Nov 30 2020 at 09:47):

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

view this post on Zulip Karl Palmskog (Nov 30 2020 at 09:47):

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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 09:48):

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

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (Nov 30 2020 at 09:49):

@Karl Palmskog Yes.

view this post on Zulip 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

view this post on Zulip Christian Doczkal (Nov 30 2020 at 09:49):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Assia Mahboubi (Nov 30 2020 at 09:52):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Christian Doczkal (Nov 30 2020 at 11:58):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 30 2020 at 13:40):

just pick 5 or ten different ones, for example:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Assia Mahboubi (Dec 03 2020 at 16:35):

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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Karl Palmskog (Dec 03 2020 at 16:58):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Christian Doczkal (Dec 03 2020 at 17:00):

@Assia Mahboubi thank you for your observations.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Assia Mahboubi (Dec 03 2020 at 17:07):

What is a "special requirement"?

view this post on Zulip Karl Palmskog (Dec 03 2020 at 17:12):

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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 03 2020 at 17:13):

generate.sh will not take care of things like this

view this post on Zulip Assia Mahboubi (Dec 04 2020 at 09:22):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 04 2020 at 11:09):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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 :)

view this post on Zulip 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?

view this post on Zulip Assia Mahboubi (Dec 04 2020 at 11:13):

Otherwise, it should be quite easy.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Dec 04 2020 at 11:14):

you can write

file.v : dep1
dep1 : dep2 dep3

it will close it transitively for you

view this post on Zulip Karl Palmskog (Dec 04 2020 at 11:14):

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

view this post on Zulip Karl Palmskog (Dec 04 2020 at 14:05):

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

view this post on Zulip Erik Martin-Dorel (Dec 04 2020 at 14:06):

yes! sorry for the delay :)


Last updated: Oct 16 2021 at 07:02 UTC