detect if we are running in CI

Stream: mathlib4

[Scott Morrison]

How can I have a tactic detect if we are running in CI?

The says combinator proposed in #5980 has a set_option says.verify true mode that tries to regenerate the right-hand-side. I think it makes sense to run this in CI.

However I can't just set -Dsays.verify=true, because this is not a built-in option, and so not available until the build actually reaches that file.

Is there some way to detect that we are in CI? I think all we need is some already-defined global option that we can stuff a flag into, but that is not already in use.

[Scott Morrison]

Would it make sense simply to add a CI option to Lean core?

[Gabriel Ebner]

Alternatively you could also check an environment variable.

[Scott Morrison]

This works great! I'm just looking for the CI environment variable, as github sets this automatically. I've written some tests that verify it is working as expected locally.