Test with Alectryon 1.4 and Coq 8.14.

[Zimmi48]

No description provided.

[Zimmi48]

This seems to work well. However, the update to Coq 8.14 creates new warnings that are reported in the Alectryon snippets (missing locality for Instance).

[Zimmi48]

This warning is already disabled in _CoqProject. Maybe we need a way to also report the warning disabling when calling SerAPI through Alectryon.

[cpitclaudel]

For warnings that can be unconditionally disabled, we could use Global Set Warnings "-…". in a core file. I'm don't think that SerAPI has a way to customize warnings from the command line otherwise, but maybe there's a [protocol command that we could use for that if the Set Warnings route is not desirable.

[Zimmi48]

Global Set Warnings is frowned upon because of the transitive reach (beyond project boundaries). That's why command line arguments are usually preferred for that kind of stuff. That being said, in this precise case, I can also fix the warning by adding #[ global ] annotations everywhere they are missing.

[cpitclaudel]

Makes sense, thanks!