persistent information left by a linter

Stream: lean4

[Damiano Testa]

This is in some sense a follow up of this thread.

I tried using a linter to "plant" some information on parsing a command that could be retrieved by the same parser while parsing a following command. However, no matter what I try (updating the option of the linter, tracing a message, reading past errors,...) seems doomed to fail.

Is this something that linters are forbidden from doing? E.g. suppose that I wanted a linter that simply counted the number of commands on which it ran in the current file. Is that possible? How?

[Eric Wieser]

You could write to an IO.Ref I think

[Eric Wieser]

(but that's probably a bad idea for other reasons)

[Damiano Testa]

I will experiment with that, although I'm not sure that I understand exactly how IO.Ref works.

[Damiano Testa]

Why would it be a bad idea?