Split off reals into package coq-fourcolor-reals that is a dependency of coq-fourcolor

[palmskog]

As discussed on Zulip. This is a draft until CI details are figured out.

[palmskog]

@proux01 I just copied over Makefile boilerplate from Analysis, does it look reasonable to you?

[palmskog]

@ybertot any chance for a review here? This follows closely the boilerplate currently used in MathComp-Analysis.

[ybertot]

I am essentially happy with the way the implementation is written. I think it would be good to add some documentation of real package in the README.md file.

[ybertot]

I tried to understand where to change the text in the meta.yml file, but I was not able to locate the sources for the building and installing instructions.

[palmskog]

I tried to understand where to change the text in the meta.yml file, but I was not able to locate the sources for the building and installing instructions.

Nothing has changed in meta.yml or the README how the project is built. The "default" make action still builds the whole project, and opam install coq-fourcolor installs all files. The way this PR is structured, the only differences are in how opam packages are structured.

How do you propose we should document coq-fourcolor-reals (beyond the description already in the .opam file)? It may be just confusing to people interested in only the Four Color Theorem to mention this package.

[proux01]

Can we keep a meta.yml? My understanding was that this only supports single packages (hence the fact we don't use it in mathcomp).

[ybertot]

I just wanted to add a sentence of the form : "If you are only interested in the formalization of real numbers, here is the opam directive to install it : " and "if you want to compile from the source here is the make command to apply".

[palmskog]

Can we keep a meta.yml? My understanding was that this only supports single packages (hence the fact we don't use it in mathcomp).

meta.yml is used for much more than just packages. Indeed we can't currently define/generate packaging boilerplate for monorepo projects with multiple packages, but this doesn't prevent using it for README.md and so on.

[palmskog]

@ybertot see a201fda - does this fit what you had in mind?

[ybertot]

@palmskog and @proux01, thank you for your time.

[palmskog]

@ybertot to help out Frédéric Blanqui, there still needs to be a release and corresponding opam packages. I can help out if you want (e.g., I can add packages based on a tag).