Using `IO.Ref`

Stream: lean4

[Damiano Testa]

I would like to confirm that I am not doing anything wrong when working with IO.Ref: my understanding is very superficial!

To show my issue, there is the need for two files: one defining (initializing) the IO.Ref and one reading it.
File1:

import Lean.Elab.Command

initialize myRef : IO.Ref Bool ← IO.mkRef true

/-- checks whether the counter is `true` and, if so, then sets it to `false`.
It also prints a summary of what it is doing. -/
elab "to_false" : command => do
  if ← myRef.get then
    Lean.logInfo "Counter was `true`, setting it to `false`"
    myRef.set false

File2:

import File1

to_false -- Counter was `true`, setting it to `false`

If you have this setup, in File2 you will see the message that the command emits.

However, with essentialy whatever you type (adding a line-break, a new command, a space, virtually anything), the message disappears and will not be back until you reload the file.

[Damiano Testa]

I can guess that, once the Ref is set to false, it does not get "reset" with modifications of the file. Is there a way around this, ensuring that the message on the first to_false stays there if I modify the file?

[Sebastian Ullrich]

That is the purpose of environment extensions

[Damiano Testa]

So you are saying that I should be using an environment extension instead?

[Damiano Testa]

(I have never worked with them, so I really do not know what they are or how they work.)

[Damiano Testa]

Actually, the reason I was playing with this is for use in a linter: would an environment extension be something that a linter can modify?

[Damiano Testa]

Updated example:
File1:

import Lean.Elab.Command

open Lean

structure counter where
  f : Bool
  deriving Inhabited

initialize myCounter : Lean.EnvExtension counter ← Lean.registerEnvExtension (pure ⟨true⟩)

/-- checks whether the `EnvExtension` is `true` and, if so, then sets it to `false`.
It also prints a summary of what it is doing. -/
elab "EnvExt_false" : command => do
  if (myCounter.getState (← getEnv)).f then
    Lean.logInfo "EnvExt was `true`, setting it to `false`"
    setEnv <| myCounter.setState (← getEnv) ⟨false⟩

File2

import File1

EnvExt_false -- EnvExt was `true`, setting it to `false`

and EnvExt_false does not stop printing its message when I edit the file!

[Damiano Testa]

The next step is to check whether this will work with a linter.

[Damiano Testa]

Unfortunately, I do not seem to be able to modify the EnvExtension from within a linter.

[Matthew Ballard]

I think you need to write to the environment during the build of the oleans. The most common way this is done is via attribute tagging. I am not sure how useful it is to your use case but it gives examples of use.

[Damiano Testa]

Can you give me an example of something that does that?

[Matthew Ballard]

I’m away from my computer but rg 'addEntry' Mathlib/Tactic should provide many

[Damiano Testa]

Ok, thanks! This is probably enough: I just wanted to find an entry-point!

[Matthew Ballard]

You probably want a PersistentEnvExtension also

[Damiano Testa]

I am probably making things too complicated: all that I want is to pass the knowledge to the linter of whether it has already processed a command in a file or not.

[Damiano Testa]

(Note that import statements are not "seen" by the linter, so "the first command" really means "the first non-import command", but that is by default and also what I want!)

[Matthew Ballard]

Processed in a separate file?

[Damiano Testa]

I am trying to check whether each linted file starts with a doc-module string and report it if it does not.

[Damiano Testa]

So, every file that imports the linter will be processed.

[Damiano Testa]

If I understood your question correctly, then yes: the linter is in one file and every downstream file from there is where I want the check to happen.

[Damiano Testa]

Reading the docs, I think that PersistentEnvExtensions may not be what I want: if I understand correctly, the Persistent part is that it passes on information to the downstream modules. While I do not really care about that information, I just want to perform a check on each module separately.

[Matthew Ballard]

Sorry, I’m not exactly sure what is wanted. It seemed from your example that you wanted to persist some state from one file to the next.

[Damiano Testa]

Ah no, I wanted the state of each file to change upon reaching some command. The example above worked as intended for the actual command EnvExt_false, but linters do not seem to be able to globally modify environment extensions.

[Damiano Testa]

So, it appears that within the linter, when it is processing a command, I can modify the envExtension, but as soon as the linter releases the current command, the environment switches back to what it was before the linter modified it.

[Damiano Testa]

I suspect that linters run in a withoutModifyingEnv wrapper, so I am really not sure what to do.

[Damiano Testa]

Their modifications of IO.Refs do work, but the IO.Refs are flimsy and need to reload the file to be reliably used.

[Sebastian Ullrich]

I think what you actually want is for a linter to be able to access any syntax tree/snapshot up to the current command, which is a request that has come up before

[Sebastian Ullrich]

Then you don't need to carry any state yourself, which is good because we want linters to run in parallel to elaboration

[Damiano Testa]

That would certainly be enough! I think that for this specific case, a much smaller amount of information would be already sufficient!

[Damiano Testa]

While we are here, would it be possible to have an option to make the linters run before the corresponding the command that they are linting?

[Sebastian Ullrich]

This is a bit of speculation at this point but if we give linters access to the snapshot of the command, we could have them decide for themselves if they want to wait for the snapshot after elaboration or not

[Damiano Testa]

Ok, I have wanted the option of choosing to run a linter before its command very often.

[Damiano Testa]

The typical case is that you modify the command, say by replacing a proof by sorry and you want to see if it still compiles, up to the sorry message.

[Damiano Testa]

Currently, you have to find a way to make the name not clash with the one of the current declaration.

[Damiano Testa]

If you could run the linter before the command, you could simply make it not modify the environment and be done!

[Sebastian Ullrich]

I'm not sure I see how that wouldn't utterly tank performance unless you're extremely careful about what commands you want to modify and test

[Damiano Testa]

These are more "diagnostic" linters: I do not intend to run them everywhere, but either every once in a while, or just on some files.

[Damiano Testa]

E.g., imagine that at some point you want to see which lemmas could be proved by by simp. You run your linter once a week and tally the results.

[Damiano Testa]

Another situation that I have encountered is when you want to know if using a terminal refine is quicker than an exact: you run the linter and wait for the results!

[Damiano Testa]

Can I just get confirmation that linters cannot modify EnvExtensions, whether they are persistent or not? I have been failing to do it, but I do not know if it is just that I am misunderstanding how to do that! :smile:

[Mario Carneiro]

they cannot do it, because EnvExtensions store data in the Environment, and linters are run inside a withoutModifyingEnv block

[Mario Carneiro]

actually I take it back, looking at the code it seems like there is nothing stopping them from modifying the environment

[Damiano Testa]

Mario, if you could show me some code where a linter leaves a trace of it linting something, I'd be very grateful!

[Damiano Testa]

All I really would like is just to know if a linter already linted something in a file or not, but anything would be welcome!

[Damiano Testa]

Also, where do you see what the linters do? I have been able to figure something out by seeing the "in action", but I have not found the code that is used to run them.

[Mario Carneiro]

search for runLinters in core

[Damiano Testa]

Oh, in Lean.Elab.Command?

[Damiano Testa]

If I am reading this correctly, it saves the state before running each linter and then sets it back but returns the messages!

[Damiano Testa]

So, I could embed persistent information in the messages!

[Mario Carneiro]

none of that seems to be rolling back the environment though, AFAIK

[Damiano Testa]

Doesn't the State contain the Environment? That seems to be saved and returned by the linters.

[Mario Carneiro]

oh, yes it's the let savedState ← get ... modify fun s => { savedState with messages := s.messages } part

[Damiano Testa]

Right, the only thing that seems to filter through are the messages.

[Mario Carneiro]

I don't think you get access to those messages later though, they are collected in the server

[Damiano Testa]

I guess that you are right: you can detect them outside of the linter, but not pass them on "silently" to the linting of the next command.

[Damiano Testa]

Maybe linters can store some information in the infotrees? Anyway, time for bed here!

Thanks a lot, though! This has been very fruitful!

[Damiano Testa]

In case anyone here is interested, I was able to get an IO.Ref to work for a new linter: #15794.

[Sebastian Ullrich]

Just to mention one more caveat without looking too far into your code: did you consider the thread safety of such a linter? The language server is an asynchronous program.

[Damiano Testa]

I would be happy to consider thread safety, but I do not know what it is... :upside_down:

[Damiano Testa]

Is it a valid/useful data point that the linter successfully identified all of mathlib?

[Henrik Böving]

Damiano Testa said:

I would be happy to consider thread safety, but I do not know what it is... :upside_down:

Thread safety is relevant once your function is not the only thing that may access some piece of data (in this case your IO.Ref) at any given time. This can happen when someone is using your linter while editing code with the language server. The fun thing about thread safety is that violations of it do not necessarily have to show up for everyone always when using the feature. Due to the way that concurrency etc. works it can be a sporadic, hard to observe but confusing phenomenon.

[Damiano Testa]

Oh, I see! Thanks for the explanation!

[Damiano Testa]

I have certainly observed thread unsafety when I was using IO.Refs, although I have not played enough with this linter to know if this one is or not thread safe. I did not observe "funny behaviour", but also did not use it extensively.

[Damiano Testa]

Just to be clear: in the aseptic setting of CI running lake build, thread safety is completely irrelevant, right?

[Henrik Böving]

At the moment yes, lake runs one process per file and that process is currently still single threaded (though that is partially going to change when we have in file parallelism of course)

[Damiano Testa]

In the case of an IO.Ref, if a thread starts "in the middle", what value does it use?

[Henrik Böving]

Oh the interesting question is what happens when two threads write to it at the same time

[Henrik Böving]

And the answer is, who knows!

[Damiano Testa]

So, is an IO.Ref ever "safe"?

[Henrik Böving]

If you can guarantee it is not accessed by multiple threads sure.

[Damiano Testa]

And how can you guarantee that?

[Damiano Testa]

(In my case, there is a linter that modifies the IO.Ref as its last step.)

[Damiano Testa]

(And the linter is the only process that knows about the IO.Ref.)

[Kim Morrison]

I fear the answer here is: "by not using IO.ref from a linter".

[Damiano Testa]

Yes, I tried a few possibilities and they only worked "statically": most edits to the file would make the linter unpredictable.