tirix / metamath-vspa Goto Github PK

1. Followed install instructions for Metamath LSP server https://github.com/tirix/metamath-vspa#installation.
2. Installed Metamath VS code extension.
3. Server Error when trying to open eengtrkg.mmp to test the functionality of the extension.

note: run with RUST_BACKTRACE=1 environment variable to display a backtrace [Info - 9:07:02 AM] Connection to server got closed. Server will restart. thread 'main' panicked at 'Bad file path: Os { code: 2, kind: NotFound, message: "No such file or directory" }', src/util.rs:105:33

Don't think I am doing anything wrong as I am following the instructions so this issue is being opened to help figure out my issue but also, in the event that it is something trivial, to add the fix to the install instructions in case others may hit the same thing.

Hi @tirix ,

to see if Diagnostics was implemented, I've changed the line

reelprrecn $p |- RR e. { RR , CC } $=

to

reelprrecn $p |- RR e. { RR , CCD } $=

and I get the error below:

thread 'main' panicked at 'called Option::unwrap() on a None value', /mydir/.cargo/git/checkouts/metamath-knife-c0afdf58ccf11b37/0dbd297/src/grammar.rs:1295:59
note: run with RUST_BACKTRACE=1 environment variable to display a backtrace
thread 'main' panicked at 'called Result::unwrap() on an Err value: Any { .. }', /mydir/.cargo/git/checkouts/metamath-knife-c0afdf58ccf11b37/0dbd297/src/database.rs:300:31
[Info - 5:14:40 PM] Connection to server got closed. Server will restart.

If I edit an .mmp file, I get this error

[Error - 5:08:09 PM] Request textDocument/completion failed.
Message: Not implemented
Code: -32601

I'm pretty sure it is because the server adverts that feature, but it's actually not implemented.

Just to let you know

Hi @tirix ,

in these days, every now and then I've tried to test your project. A few notes you could consider, when you'll update the Readme file:

• a little typo in the Readme intall > install

I've tried to install it on a clean Ubuntu VM:

• at some point (I don't remember if I was installing Rust, or I was compiling with Cargo) an error came up (googling for the error message, it was an easy fix, I was missing a C Compiler)

• please, consider adding a note about updating node.js (I had to do it, because my npm version was pretty old, not sure if VSCode comes with an old version of node); on Linux I always use nvm to manage node versions

• to silence warnings, I had to launch a 'npm install'

Now F5 runs, but it does nothing (I would expect the "Extension Development Host" to open). Should I look for the launch.json file?
I'll look further into it.

Thanks for the great job
Glauco

In general, the correct description is provided when hovering over constants:

However, in some cases, there is a shift between the correct description and the description shown:

Here, the correct description for /\ would be: Wedge (read: 'and')
But the description shown is: Vee (read: 'or')

VSCode opens a new empty tab "Untitled-n" and the cursor blinks at the beginning of the new tab

@glacode mentioned in issue #2 :

I'm getting an error when I hover on a constant; and the LSP server crashes/restarts:

thread 'main' panicked at 'called Option::unwrap() on a None value', //.cargo/git/checkouts/metamath-knife-c0afdf58ccf11b37/7954d40/src/grammar.rs:462:80
stack backtrace:
0: rust_begin_unwind
at /rustc/9d1b2106e23b1abd32fce1f17267604a5102f57a/library/std/src/panicking.rs:498:5
1: core::panicking::panic_fmt
at /rustc/9d1b2106e23b1abd32fce1f17267604a5102f57a/library/core/src/panicking.rs:116:14
2: core::panicking::panic
at /rustc/9d1b2106e23b1abd32fce1f17267604a5102f57a/library/core/src/panicking.rs:48:5
3: metamath_knife::grammar::Grammar::too_short
4: metamath_knife::grammar::Grammar::parse_formula
5: mm_lsp_server::definition::find_statement
6: mm_lsp_server::hover::hover
7: mm_lsp_server::server::Server::run
8: mm_lsp_server::main
note: Some details are omitted, run with RUST_BACKTRACE=full for a verbose backtrace.
[Info - 12:30:40 AM] Connection to server got closed. Server will restart.
[Error - 12:30:40 AM] Request textDocument/hover failed.