I quickly double checked the behaviour, and the commands do run, but with the wrong result. You'll get back blank answers, or messages about variables not existing.
Long term, this should get fixed in Idris2, but for now I at least wanted the warning. Status bar warnings are a bit subtle, but having a pop up would get really annoying after the first time.
Addresses https://github.com/meraymond2/idris-vscode/issues/18.
I quickly double checked the behaviour, and the commands do run, but with the wrong result. You'll get back blank answers, or messages about variables not existing.
Long term, this should get fixed in Idris2, but for now I at least wanted the warning. Status bar warnings are a bit subtle, but having a pop up would get really annoying after the first time.