Re-implement PixMap writer in Elpi

[MSoegtropIMC]

This PR re-implements the pixmap writer in Elpi, which has the advantage that no plugin needs to be maintained. It is also a bit more comfortable than the original plugin:

• it allows to give a file name for the .ppm file
• it does the required vm_compute, so that this need not (but can) be done upfront
• the resulting file is a PPM rather than a PGM file, which has only half the size (no spaces between numbers).

The conversion from a sparse raster to a 2D list of bools is done as Coq program. Tests showed that the complete conversion in one step is more efficient than e.g. a line by line conversion. Elpi is only used to write the PPM file and to define a top level vernacular command.

A conversion of the sparse raster as an Elpi program is also possible but likely not more efficient. If the vm_compute for doing the plot is done in a separate step, the conversion to a full raster and output as file takes only a few 10 ms for a 200x200 grid.

This also fixes some requires in examples/bigD.v

[SkySkimmer]

Don't forget to open a PR fixing the deps in Coq CI before this gets merged

[spitters]

LGTM! Sorry, I was too quick merging.
Please address the @SkySkimmer 's suggestion above.

[MSoegtropIMC]

Yes, I already did the change in a branch - I just had an odd problem with my commit email I need to clarify.

[MSoegtropIMC]

@SkySkimmer : I didn't do this in a longer while. I guess I need not create an overlay and just add the additional dependency in the yaml file. As far as I understand overlays are for the reverse situation where a change in Coq breaks packages in CI.

[SkySkimmer]

yes

[SkySkimmer]

also need to update Makefile.ci

[spitters]

also need to update Makefile.ci

@SkySkimmer I guess we are still waiting for this.
After that what's the best way to merge this PR? I don't immediately see a button for it on github.
(Also, feel free to just do it, if you know what to do...)

[MSoegtropIMC]

@spitters : as I wrote in the "Undo PR" this is solved in Coq CI. The Coq PR is coq/coq#19830 (merged).

[MSoegtropIMC]

To re-merge this, you need to undo the PR which reverted this PR. That is you need to revert #210. You should have a button for this at the bottom of the PR if you are admin.

[spitters]

I've reverted the revert. What should I do next? Or can you restart the PR?

[MSoegtropIMC]

@spitters : to me it looks fine as is - nothing else to be done.

You have the "write_image" folder in root and example/Circle.v has commands like

Elpi WritePPM "Circle.ppm" ( Circle_bigD ).

[SkySkimmer]

Can you also update https://github.com/coq/opam/blob/master/extra-dev/packages/coq-corn/coq-corn.dev/opam ?

[MSoegtropIMC]

@SkySkimmer : sure, will do right away,

[MSoegtropIMC]

See coq/opam#3247