Minor breaking changes in IDE Mode

[meraymond2]

This issue to detail the current state, as of version 0.2.1, of minor inconsistencies in IDE Mode responses between Idris 1 and 2.

These aren't necessarily bugs, but it would be nice to maintain backwards compatibility where the differences are unintentional, minor and easy to fix, until breaking protocol improvements are made.

I'm skipping commands that are explicitly not yet implemented, or are mostly implemented (i.e. just missing metadata).

:add-missing
I know this is still unimplemented, but I wanted to mention that it's impossible to use, because currently missing cases will cause a file to fail to load.

:browse-namespace
Also still technically unimplemented, but the empty placeholder value is (:ok "" ()), and it should be (:ok () ())

:case-split
This will no longer work if the right side is not a hole. This might be an improvement, because it makes less sense to case-split after implementing it.

Case splitting on a Nat will return 0 rather than Z. I don't think this matters anymore, though in an earlier version of Idris 2, it was considered an error.

:interpret
This no longer includes the type in the response. Interpreting 2 * 2 would return 4 : Integer but now returns just 4.

:load-file
Any errors in files will cause the file not to load, which means you can't run commands on it. See :add-missing.

:warning messages now sometimes have relative file paths, before they were (to the best of my knowledge) always absolute.

:make-case
Used to end with a \n.

:make-lemma
The reply is less structured than before. Given

g : (n: Nat) -> (b: Bool) -> String
g n b = ?g_rhs

it used to return (:return (:ok (:metavariable-lemma (:replace-metavariable "g_rhs n b") (:definition-type "g_rhs : (n : Nat) -> (b : Bool) -> String"))) 2) but now it's "g_rhs : Bool -> Nat -> String\ng_rhs b n".

The declaration is slightly different, it doesn't have parameters names. In this example, the order has changed, but I haven't checked if that's consistent or random.

:make-with
Like :make-case, it used to end with a \n.

:metavariables
Premise names have 3 empty spaces in front of them. For the function above, the relevant part of the response is (:return (:ok (...("Main.g_rhs" ((" b" "Bool" ()) (" n" "Nat" ()))...)) 9)

:type-of
The response now includes the module name before the variable.

:version
This command isn't even officially unimplemented, it's entirely unrecognised by the IDE process. <- this is wrong
The format of the request has changed. Previously all commands were always wrapped in s-expression lists. In Idris 2, commands that don’t take arguments are just symbols, not lists. So 00000f((:version) 1) must be changed to 00000d(:version 1).

[meraymond2]

There's a PR open for :make-lemma #570

[ohad]

:interpret ":cd <dir>" now takes a string (with quotes).