Closed nothingnesses closed 2 years ago
meraymond2
commented
3 years ago Thank you for the very detailed bug report :+1:
It looks like the idris2 process has either crashed, or not started correctly. I don't see anything wrong in your config though. I haven't been able to replicate this. I'm on an older version of vscodium, tomorrow I'll try with 1.54.3 — maybe something's changed.
When you start the extension are there any error popups? I'm assuming none of the other commands work either?
nothingnesses
commented
3 years ago When you start the extension are there any error popups?
I'm not sure what you mean by "start the extension". I thought that it's automatically started when the editor starts, as long as it's enabled, or have I maybe been missing a step to activate it? The only thing I did as far as setting up the extension was to install it and then change the settings to use it with Idris 2 as per the readme. In any case, no error popups appear when I start the editor, and I think the extension otherwise starts fine since the syntax highlights it provides for Idris source files seems to work.
I'm assuming none of the other commands work either?
Aside from idris.addClause, the only other commands I've tried are idris.generateDef and idris.caseSplit. Neither also worked and both produced similar errors as with idris.addClause. E.g., running idris.caseSplit, when the cursor is on the x in the following buffer contents:
foo : Bool -> Bool
foo x = ?foo_rhsresults in the following error in Log (Extension Host):
[2021-03-22 23:54:19.693] [exthost] [error] Error [ERR_STREAM_DESTROYED]: Cannot call write after a stream was destroyed
at doWrite (_stream_writable.js:431:19)
at writeOrBuffer (_stream_writable.js:419:5)
at Socket.Writable.write (_stream_writable.js:309:11)
at /home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/node_modules/idris-ide-client/build/client.js:71:24
at new Promise (<anonymous>)
at IdrisClient.makeReq (/home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/node_modules/idris-ide-client/build/client.js:69:16)
at IdrisClient.loadFile (/home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/node_modules/idris-ide-client/build/client.js:229:21)
at /home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/out/commands.js:279:36
at Generator.next (<anonymous>)
at /home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/out/commands.js:8:71
at new Promise (<anonymous>)
at __awaiter (/home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/out/commands.js:4:12)
at Object.exports.loadFile (/home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/out/commands.js:275:42)
at /home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/out/commands.js:55:25
at Generator.next (<anonymous>)
at fulfilled (/home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/out/commands.js:5:58)
at runMicrotasks (<anonymous>)
at processTicksAndRejections (internal/process/task_queues.js:94:5) idris.caseSplitShould I test the other commands as well?
Not sure if this is pertinent, but in my system (Bedrock Linux) I think the Code editor uses glibc whereas Idris 2 might be using musl (IIRC the Chez Scheme I bootstrapped it from was built with musl):
$ ldd `which scheme` | rg -F "libc."
libc.so => /lib/ld-musl-x86_64.so.1 (0x7f9ac415f000)
$ ldd /bedrock/strata/`brl which code-oss`/bin/electron9 | rg -F "libc." # The editor apparently uses electron v9.4.1 according to its "About" option.
libc.so.6 => /lib64/ld-linux-x86-64.so.2 (0x7f70b194c000)That said, Idris 2 seems to run fine in the editor's built-in terminal, so I'm not sure if that is the cause. Should I maybe try to rebuild the Idris 2 binary using glibc?
nothingnesses
commented
3 years ago I rebuilt Idris 2 from the current latest branch, using Chez Scheme built with glibc, and tried the idris.addClause command again (using the same buffer contents as in the original post). It still didn't work, but now the error in Log (Extension Host) is:
[2021-03-23 15:20:02.373] [exthost] [error] Error: Illegal value for `line`
at g._lineAt (/usr/lib/code-oss/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:82:1166)
at Object.lineAt (/usr/lib/code-oss/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:82:95)
at Object.exports.lineAfterDecl (/home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/out/editing.js:47:35)
at /home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/out/commands.js:67:40
at Generator.next (<anonymous>)
at fulfilled (/home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/out/commands.js:5:58)
at processTicksAndRejections (internal/process/task_queues.js:94:5) idris.addClauseNot sure if this is pertinent, but in my system (Bedrock Linux) I think the Code editor uses glibc whereas Idris 2 might be using musl (IIRC the Chez Scheme I bootstrapped it from was built with musl):
That's really interesting, and I have no idea why that would cause a problem but I can completely believe that it did. I'm curious, so I may try to reproduce that sometime.
Error: Illegal value for
line
I think this one is going to be a bit easier. My guess is that you're on the last line of the editor, and you don't have VSCodium set to insert a final new line on save ("files.insertFinalNewline": true). Can you confirm that?
The extension is trying to insert the new clause on a line that doesn't exist, and apparently it won't automatically extend the document. I've never run into this, because the extension saves before running commands, and mine is set to insert a final newline, so it's never tried to insert into a non-existent next line.
nothingnesses
commented
3 years ago Can you confirm that?
Yes, that was the case. I've since added that entry and added a new line to the buffer contents. After doing that, the commands I've tried have worked as expected. Thanks for help troubleshooting this!
Edit: I did another test. Apparently, the libc of the Chez Scheme that is used to build Idris 2 isn't important, only that the appropriate Chez Scheme exists, because apparently either version of Chez Scheme (musl or glibc) can run either version of Idris 2 (whether or not it was built with a Chez Scheme that uses the same libc), but the extension will only work when I am using Chez Scheme built with the same libc as the editor. So I guess if my Code uses musl, I have to be using Chez Scheme built with musl. But since my Code uses glibc, I need Chez Scheme built with glibc.
meraymond2
commented
3 years ago I've pushed a fix for the insert bug, and it's in the latest version that I just released.
but the extension will only work when I am using Chez Scheme built with the same libc as the editor.
Is your Idris2 binary dynamically linked?
nothingnesses
commented
3 years ago Thanks, the fix seems to work well.
Is your Idris2 binary dynamically linked?
I don't actually seem to have an Idris 2 binary, but a script instead:
$ ldd `which idris2`
ldd: /home/a/.idris2/bin/idris2: Not a valid dynamic program
$ cat `which idris2`
#!/bin/sh
case `uname -s` in
OpenBSD|FreeBSD|NetBSD)
DIR="`grealpath $0`"
;;
*)
DIR="`realpath $0`"
;;
esac
export LD_LIBRARY_PATH="`dirname "$DIR"`/"idris2_app":$LD_LIBRARY_PATH"
"`dirname "$DIR"`"/"idris2_app/idris2.so" "$@"
$ ldd `dirname $(which idris2)`/idris2_app/idris2.so
ldd: /home/a/.idris2/bin/idris2_app/idris2.so: Not a valid dynamic programIs your setup not like that?
meraymond2
commented
3 years ago No, I'm compiling it using Nix and I end up with a static binary.
System
(Click to expand)
``` $ uname -a Linux a 5.10.25_1 #1 SMP 1616262869 x86_64 GNU/Linux $ code-oss --version Warning: 'app' is not in the list of known options, but still passed to Electron/Chromium. 1.54.3 Unknown commit x64 $ code-oss --list-extensions --show-versions | rg idris Warning: 'app' is not in the list of known options, but still passed to Electron/Chromium. meraymond.idris-vscode@0.0.8 $ idris2 --version Idris 2, version 0.3.0 $ which idris2 /home/a/.idris2/bin/idris2 $ cat "/home/a/.config/Code - OSS/User/settings.json" | rg idris "idris.idrisPath": "/home/a/.idris2/bin/idris2", "idris.idris2Mode": true, ```Reproduction
(Click to expand)
* In a terminal, run: ```sh mkdir -p ~/tmp printf 'foo : Bool -> Bool' > ~/tmp/Main.idr code-oss ~/tmp/Main.idr ``` * In the editor, navigate cursor to `foo`. * Input `Ctrl-e`. * Input `>idris.addClause`.Expected behaviour
(Click to expand)
* Buffer now contains something similar to: ```idris foo : Bool -> Bool foo x = ?foo_rhs ``` * Log (Extension Host) has no errors related to this extension.Actual behaviour
(Click to expand)
* Buffer still only contains: ```idris foo : Bool -> Bool ``` * Log (Extension Host) contains: ``` [2021-03-21 20:54:03.174] [exthost] [error] Error [ERR_STREAM_DESTROYED]: Cannot call write after a stream was destroyed at doWrite (_stream_writable.js:431:19) at writeOrBuffer (_stream_writable.js:419:5) at Socket.Writable.write (_stream_writable.js:309:11) at /home/a/.vscode-oss/extensions/meraymond.idris-vscode-0.0.8/node_modules/idris-ide-client/build/client.js:71:24 at new Promise (Miscellaneous
(Click to expand)
* The `:ac` Idris 2 command seems to work fine: ``` $ idris2 --client ':ac 1 foo' ~/tmp/Main.idr foo x = ?foo_rhs ```