Support compute normal form in Agda 2.6

[banacorn]

The protocol has changed in Agda-2.6 https://github.com/banacorn/agda-mode/wiki/Conversations-between-Agda-&-agda-mode

[ruhatch]

So for normalisation outside a goal we now have

  | Cmd_compute_toplevel B.ComputeMode
                     String

And inside the goal we have

  | Cmd_compute         B.ComputeMode
                    InteractionId range String

Where ComputeMode is defined as

data ComputeMode = DefaultCompute | IgnoreAbstract | UseShowInstance

deriving (Read, Eq)

[banacorn]

Thanks for pointing the problem out. I have tested sending this to Agda and it works in the version 2.6

IOTCM "/some/path/to/file.agda" None Indirect (Cmd_compute_toplevel DefaultCompute "some expression")

[banacorn]

I think these are the commands that correspond to ComputeMode. They are:

• C-c C-n: Compute normal form DefaultCompute
• C-u C-c C-n: Compute normal form, ignoring abstract IgnoreAbstract
• C-u C-u C-c C-n: Compute and print normal form of show UseShowInstance

Prior to 2.6 there were only DefaultCompute and IgnoreAbstract so it was represented with a Bool.

@markokoleznik you may want to look at this, they are messing with the protocol again 😂.

[ruhatch]

Thanks for fixing that up! Do you have an ETA for when this might hit stable release? Just wondering whether to install the dev version.

[banacorn]

I haven't had the chance to do much testing (it's still mostly manual 😭), but I think it's good to go. What could possibly go wrong?? 😬 *microwaving popcorn*