search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167 stars 38 forks source link

Case split does not reload #165

Closed ncfavier closed 8 months ago

ncfavier commented 12 months ago 
open import Data.Bool
foo : Bool → Bool
foo b = {! b  !}

Running C-c C-c in that hole results in

open import Data.Bool
foo : Bool → Bool
foo false = ?
foo true = ?

I have to load again for the new holes to appear.

This is on Agda 2.6.3, agda-mode 0.4.0 (was also the case on 0.3.12).

banacorn commented 8 months ago

Closing this because I cannot reproduce this with agda-mode 0.4.4 and Agda 2.6.3.

ncfavier commented 8 months ago

It's still happening on 0.4.4 and Agda 2.6.4.1, in large files, not reliably or reproducibly. There is definitely some sort of race condition going on.