CI to test polyrith locally

Stream: mathlib4

[Miguel Marco]

PR #20334 (reviews welcome) includes the possibility of using a local installation of Sage/Singular/Macaulay2 as a backend for polyrith (and keep the online service as a fallback).

Besides the obvious advantage of giving the option of not relying on an external service, it could allow to run tests for polyrith in the CI works, in a reproducible way. But in order to do so, the CI work should run in a container that has one of those CAS systems installed (I would say Singular is probably the natural choice).

How should that be done? Who makes the decission about the CI works?

[Kim Morrison]

Yes, I think it is definitely out of scope for Mathlib CI to be running external CAS, and further I don't think we want scripts/tactics that we can't test.

This should be an external package downstream of Mathlib, that takes responsibility for its own testing.

[Kim Morrison]

If anyone is interested in pushing CAS integration further, I think the obvious first step is to take the current scripts that talk to the Sage server, and refactoring them so that are generic for an arbitrary query to Sage, rather than polyrith specific.

[Kim Morrison]

With that done, it becomes reasonable to add further tactics that rely on function calls to Sage.

[Kim Morrison]

Once those exist, it starts to make sense to think about integration with local CAS -- and the infrastructure investment, presumably in a project initially parallel to Mathlib and maybe eventually upstream, in building tool to deal with interacting with local user setups.