Add hover/go-to-def/refs for options

[digama0]

Now, clicking on foo in set_option foo true takes you to the register_option declaration for foo, if one exists; hover shows the docstring for the declaration, or the option's description; and find references on the declaration takes you to uses of the set_option.

[digama0]

Unfortunately this is another of those tests that can't be written: This test jumps into the location of the lean 4 sources, which is different for the different CI runners and also for me locally. The goTo.lean tests fix this by only doing intra-file jumps, but options must be declared in a separate file so we have the usual issue about tests being single-file only.

[gebner]

Can we just replace the lean4 source directory by the empty string like we do for the tests?

[Kha]

I don't know if this is desirable. We try to avoid source location references into src/ from tests since they are far from stable. It's really annoying when supposedly unrelated tests suddenly fail.

[digama0]

I don't know what is being asked of me here. I think the test scripts need to be rewritten in some way?

[gebner]

I would have liked to have the test included. To be clear my suggestion was to add a sed "s/$LEAN_DIR/\$LEAN_DIR/g" to tests/common.sh. It's indeed annoying if a test fails because of an added line in unrelated code, but it's even more annoying if LSP features regress without anybody noticing.

But I don't want to block the PR on that.

@Kha do you have any issues with this PR?