Null pointer exception raised when variable has not yet been declared

[agilot]

The following code snippet causes a NullPointerException.

object A extends lisa.Main{
  val f = x === x
  val x = variable
}
object C extends lisa.Main {
  A.x
}

This is due to the fact that x is declared after f. In more substantial pieces of code, this is not always obvious to spot, especially when objects start to be nested and variables imported from other files. In those cases, we may want to hint the user that the variable has not been declared yet.

[sankalpgambhir]

I'm not sure if there is a good solution to this. Initialization of objects is generally out of our hands.

We can (and did) use the compiler option to ensure good initialization orders, but it makes compilation much slower, and for larger proofs, fails and prints very very long warnings.

So a while ago, we disabled the option again (I forget what it's called) :/

If you know of a better solution, we can look at it.

Edit: the option is -Ysafe-init