Can't find interaction point 0

[JonathanLorimer]

Getting the error Can't find interaction point 0 when I run CornelisRefine

[JonathanLorimer]

Seems to be coming from here

[JonathanLorimer]

I think it might be an issue with concurrency, and when the interaction point gets inserted in to the interaction points map in BufferStuff:

data BufferStuff = BufferStuff
  { bs_agda_proc  :: Agda
  , bs_ips        :: Map InteractionId (InteractionPoint Identity)
  , bs_ip_exts    :: Map InteractionId Extmark
  , bs_goto_sites :: Map Extmark DefinitionSite
  , bs_goals      :: DisplayInfo
  , bs_info_win   :: InfoBuffer
  , bs_code_map   :: LineIntervals
  }
  deriving Generic

[JonathanLorimer]

It also may be that the interaction point state is getting clobbered somehow? If I do CornelisLoad and then CornelisRefine immediately before CornelisLoad has finished, refine seems to work (kind of like buffering a jump in a video game lol)

[carlinigraphy]

I am also seeing this issue.

Example:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc {! m + n !}

Positioning cursor in the hole, running CornelisRefine gives "Can't find interaction point 0". Though I do note running it 3-4 times will eventually succeed.

Seems to be consistent when I'm using any of

• CornelisRefine, or
• CornelisGive, or
• CornelisElaborate.