Closed suzumiyasmith closed 1 year ago
Hi, thank you for making an issue, and apologies for taking so long to answer.
I'm not able to reproduce this, do you have an example file you could share where this happens?
I'm getting this problem as well.
Here's a minimal example:
module Main
main : IO ()
main = putStrLn 1
And here's a screenshot of what I see:
Hey, thanks for providing that. I've tried on mine with that file and I'm not getting the same result.
Can you tell me a bit more about your system? OS, Idris version, VS version, etc. The extension converts from the Idris process line numbers, which are 1-indexed, to the 0-indexed VS line numbers, and I wonder if one of them has changed.
OS:
Edition Windows 10 Pro
Version 21H2
Installed on 10/1/2021
OS build 19044.1706
Experience Windows Feature Experience Pack 120.2212.4170.0
Idris:
Idris 2, version 0.5.1-a1e762a27
VS Code:
Version: 1.67.1 (user setup)
Commit: da15b6fd3ef856477bf6f4fb29ba1b7af717770d
Date: 2022-05-06T12:37:03.389Z
Electron: 17.4.1
Chromium: 98.0.4758.141
Node.js: 16.13.0
V8: 9.8.177.13-electron.0
OS: Windows_NT x64 10.0.19044
Running in wsl2 (ubuntu 22.04) with Extension is enabled on 'WSL: Ubuntu-22.04'
Linux DESKTOP-CB1QCD2 5.10.102.1-microsoft-standard-WSL2 #1 SMP Wed Mar 2 00:30:59 UTC 2022 x86_64 x86_64 x86_64 GNU/Linux
Hey,
so that issue sounds quite like this issue https://github.com/idris-lang/Idris2/issues/2226 but I believe that should have been fixed in the version you're running.
I don't have easy access to a Windows machine to test on, but I have put together a minimal test repo that should help clarify the problem. I want to confirm whether the message coming from the Idris process is correct or not.
If you could run it and post the outcome, that would be very helpful.
git clone -b error-msg-lines --single-branch https://github.com/meraymond2/idris-ide-test.git
cd idris-ide-test
npm install
npm test
Here is the output:
tom@DESKTOP-CB1QCD2:~/work$ git clone -b error-msg-lines --single-branch https://github.com/meraymond2/idris-ide-test.git
Cloning into 'idris-ide-test'...
remote: Enumerating objects: 17, done.
remote: Counting objects: 100% (17/17), done.
remote: Compressing objects: 100% (13/13), done.
remote: Total 17 (delta 4), reused 14 (delta 1), pack-reused 0
Receiving objects: 100% (17/17), 25.43 KiB | 685.00 KiB/s, done.
Resolving deltas: 100% (4/4), done.
tom@DESKTOP-CB1QCD2:~/work$ cd idris-ide-test/
tom@DESKTOP-CB1QCD2:~/work/idris-ide-test$ npm install
added 111 packages, and audited 112 packages in 2s
19 packages are looking for funding
run `npm fund` for details
2 moderate severity vulnerabilities
To address all issues, run:
npm audit fix --force
Run `npm audit` for details.
npm notice
npm notice New minor version of npm available! 8.11.0 -> 8.19.2
npm notice Changelog: https://github.com/npm/cli/releases/tag/v8.19.2
npm notice Run npm install -g npm@8.19.2 to update!
npm notice
tom@DESKTOP-CB1QCD2:~/work/idris-ide-test$ npm test
> idris-ide-test@0.0.0 test
> npx mocha --recursive --require ts-node/register --extensions ts 'test.ts'
Running idris-ide-client
1) shows the expected warning for the expected line
0 passing (315ms)
1 failing
1) Running idris-ide-client
shows the expected warning for the expected line:
AssertionError: expected { Object (err, id, ...) } to deeply equal { Object (id, type, ...) }
+ expected - actual
{
"err": {
"end": {
- "column": 17
- "line": 3
+ "column": 18
+ "line": 4
}
"filename": "test.idr"
- "metadata": [
- {
- "length": 4
- "metadata": {
- "decor": ":bound"
- }
- "start": 36
- }
- {
- "length": 3
- "metadata": {
- "decor": ":type"
- }
- "start": 75
- }
- {
- "length": 6
- "metadata": {
- "decor": ":type"
- }
- "start": 79
- }
- {
- "length": 10
- "metadata": {
- "decor": ":bound"
- }
- "start": 75
- }
- {
- "length": 15
- "metadata": {
- "decor": ":type"
- }
- "start": 88
- }
- {
- "length": 3
- "metadata": {
- "decor": ":type"
- }
- "start": 105
- }
- {
- "length": 3
- "metadata": {
- "decor": ":type"
- }
- "start": 122
- }
- {
- "length": 3
- "metadata": {
- "decor": ":type"
- }
- "start": 128
- }
- {
- "length": 3
- "metadata": {
- "decor": ":type"
- }
- "start": 146
- }
- {
- "length": 1
- "metadata": {
- "decor": ":postulate"
- "textFormatting": ":bold"
- }
- "start": 189
- }
- ]
+ "metadata": []
"start": {
- "column": 16
- "line": 3
+ "column": 17
+ "line": 4
}
"warning": "While processing right hand side of main. Can't find an implementation for Num String.\n\ntest:4:17--4:18\n 1 | module Main\n 2 | \n 3 | main : IO ()\n 4 | main = putStrLn 1\n ^\n"
}
"id": 1
at /home/tom/work/idris-ide-test/test.ts:39:12
at Generator.next (<anonymous>)
at fulfilled (test.ts:5:58)
at processTicksAndRejections (node:internal/process/task_queues:96:5)
/home/tom/work/idris-ide-test/node_modules/mocha/lib/runner.js:964
throw err;
^
Unhandled character: h at 0 in he file is
(Use `node --trace-uncaught ...` to show where the exception was thrown)
Hi, thank you for putting that together, that's very helpful :+1:.
There was a commit made between 0.5.1 and 0.6.0 that changed the way it reports errors. I think you might have run into it sooner if you were on a more up to date version of Idris 2.
I'll work on a fix, and let you know when there's a new version up.
This should be fixed in the latest version.
Using idris2-git in aur Idris 2, version 0.5.1-50c5be30d
Idris Language v0.0.12