[Bug] [Lean] [Spike] Verified file up to line is inconsistent

[pimotte]

What happened?

When opening files from this repo (solutions secret for students)
the progress bar is quite inconsistent. It will either say "up to line 1", "up to line x", where x is the line before #doc or not be present, even when goals after line 1/x are already shown.

How can we reproduce this issue?

Example:

1. Open any worksheet from the linked repo
2. Observe the inconsistent behaviour

What was supposed to happen?

The progress bar should reflect the checking progress. Same for the progress marker.

Additional Information

The reason I've marked this as a spike is because I'm not sure it has a reasonable resolution: It could very well be that the LSP indeed only communicates this information with the given granularity.

When investigating this, pay attention to the proof bars as well.

Outcomes of this spike are answers to the following

• Is the problem indeed the LSP information not being granular enough, or is there another bug?
  (#verso > Fine grained file progress suggests that the information should be available somewhere)
• If yes, Could we get more finegrained progress from the LSP?
  • If yes, describe the technical steps needed to improve this
  • If no, describe the best mitigation possible to retain this information
• Design proposal or prototype for the progress reporting behaviour.

Also possibly related to impermeable/waterproof-editor#77

[pimotte]

Hypothesis: From the Lean extension we get the information both that the #doc is elaborated, but also where we are in proofs. We currently just look at the first one. We might want to do something along the lines of "look at bottom

@GitLuckier I've taken the liberty of assigning this to you, since it seems a good follow-up issue to what you have been doing so far.