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

Add option to disable super-slow "Proof View Diff" #321

Merged
merged 3 commits into from
Dec 14, 2022

Conversation

Blaisorblade
Copy link
Contributor

  • Some initial testing confirms @4ever2's diagnosis in Issues with speed/output of goal display (1s in CoqIDE, 3min in VSCoq) #317 (comment).
  • Apologies if this is unfinished; this was a quick prototype, but it's already robust enough that one can enable and disable the option and see the effect immediately. And I know I don't really know TypeScript well.
  • If I actually knew TypeScript, I'd maybe try using SettingsState.proofViewDiff? instead of adding a new boolean.

Initial testcase

Adapted from #317 (comment) with size 500 (I didn't want to wait for 3 minutes).

Require Import ZArith.
Open Scope Z.

Goal forall x, x>=500.
intros x.
Time cbv.

Motivation: this option can be very slow, according to
coq#317 (comment).

TODO: should probably be `coq.proofViewDiff`, but `coq.proofViewDiff.XYZ`
options exist and I'll test for interference later.
server/src/stm/STM.ts Outdated Show resolved Hide resolved
@Blaisorblade Blaisorblade marked this pull request as ready for review December 13, 2022 01:41
@TheoWinterhalter
Copy link

I have a silly question: with your patch, can you still get proof diff but from Coq (which is faster if I understood correctly) or will this require yet another patch?

@thery thery added this to the 0.3.7 milestone Dec 13, 2022
@Blaisorblade
Copy link
Contributor Author

@TheoWinterhalter it would need another patch, but I feel "VsCoq stops hanging for minutes" is still valuable, and a low-hanging fruit. The existing diffs still work AFAICT, and you can even tweak the setting without reloading the file.

@thery
Copy link
Contributor

thery commented Dec 14, 2022

Can we merge?

@Blaisorblade Blaisorblade changed the title (Prototype) Add option to disable super-slow "Proof View Diff" Add option to disable super-slow "Proof View Diff" Dec 14, 2022
@Blaisorblade
Copy link
Contributor Author

Assuming the bump hasn't changed things, this should be pretty safe and keep the old behavior by default. (Maybe we should change the default).

@thery thery merged commit 24a0c9b into coq:master Dec 14, 2022
@Blaisorblade Blaisorblade deleted the disable-proof-diff branch December 15, 2022 20:00
@Blaisorblade
Copy link
Contributor Author

Thanks for merging!

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.

4 participants