Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix empty snapshot list server errors #1259

Merged
merged 2 commits into from Jun 28, 2022

Conversation

Kha
Copy link
Member

@Kha Kha commented Jun 28, 2022

It looks like I didn't properly review the updateFinishedPrefix uses

Comment on lines +290 to +291
-- Ignore exceptions, we are only interested in the successful snapshots
let (cmdSnaps, _) ← oldDoc.cmdSnaps.updateFinishedPrefix
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A coincidental simplification, but it seems reasonable to ignore errors from the old document. This subsumes the "Internal server error" from above.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we still have the check for aborted here? It's basically just an assertion to make sure we don't violate assumptions internally.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know, does the assertion have any bearing on the surrounding code? As the comment says, all we're here for is recycling snapshots before the old document gets dumped.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, it is a "non-local" check which verifies that a totally different part of the code behaves correctly. Maybe this isn't great practice so makes sense to leave out.

@leodemoura
Copy link
Member

@Kha I am merging this PR as-is. My system became unusable today because of the panic error messages. It was happening every time I opened Emacs and then src/Lean/Elab/Command.lean. This PR seems to fix the problem after update-stage0.

@leodemoura leodemoura merged commit 80217cf into leanprover:master Jun 28, 2022
@Kha Kha deleted the async-head-wait branch June 29, 2022 15:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants