trying to test it #2

glacode · 2022-02-25T22:00:05Z

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

tirix · 2022-02-26T02:57:43Z

Hi Glauco,

Thanks for the feedback!
I've updated the Readme file according to your remarks.

There might be another way to install it:

run npm run compile from the metamath-vscode directory,
copy or symlink the metamath-vscode directory to ~/.vscode/extensions/metamath-vscode/:
ln -sf <PATH TO YOUR GIT CLONE>/metamath-vspa/metamath-vscode ~/.vscode/extensions

Could you try that out?

I'll also try to publish the extension as-is, this is ultimately how it shall be used.
_
Thierry

tirix · 2022-02-27T08:58:22Z

@glauco The extension is now up in the Visual Studio marketplace!

glacode · 2022-02-27T17:31:53Z

Hi @tirix ,

I've installed it from the market place.

If I open a .mmp file, right-click a label, I see "Show Proof", thus I guess the extension is working.

But when I select "Show Proof" it does nothing.

I've added the .metamath.json file to point to a set.mm file in the folder (with a bunch of mmp files)

I've run
cargo install --path metamath-vspa/metamath-lsp
(after some permission issues, it went through clean)

Is there a way for me to check if the set.mm parsing was done?

Any hint?

Thanks in advance
Glauco

tirix · 2022-02-27T18:36:56Z

Hi Glauco,

If you saw the "Show Proof" option in the context menu it already means that the extension is correctly installed and activated - that's a first step!

Here are different things you could try:

Do the other features work? (hover, go to definition, diagnostics) There could be different issues depending on whether they work or not.
You could try to run the server in standalone from a command prompt to check that it is on your default path, just launch mm-lsp-server --help and check if it works. If not, you might have to add its full path in the Metamath extension configuration.
The server creates a file named lsp.log in the workspace directory: do you see it? There might be some information there.
There are also sever logs in the "Output" view, when you select "Metamath Server" in the drop-down menu.
Finally, in commit b4dc441 I fixed the detection of labels in proofs (especially for the case of labels in proof files), you could try a git pull, but that version is already two weeks old.

This tool is still in development, but your feedback will definitely help improving it!
BR,
_
Thierry

glacode · 2022-02-28T20:17:10Z

Hi @tirix ,

my answers below:

Do the other features work? (hover, go to definition, diagnostics) There could be different issues depending on whether they work or not.

I only see the "Show Proof", I don't get the other options/features.

And I don't get syntax highlighting

You could try to run the server in standalone from a command prompt to check that it is on your default path, just launch mm-lsp-server --help and check if it works. If not, you might have to add its full path in the Metamath extension configuration.

Yes, it works (I can launch it from any folder)

Looking at the help output, I've then tried
mm-lsp-server set.mm
and it ends with this console message

Content-Length: 95

{"jsonrpc":"2.0","method":"window/logMessage","params":{"message":"Database loaded.","type":4}}

But it still doesn't work.

The server creates a file named lsp.log in the workspace directory: do you see it? There might be some information there.

It didn't appear (on another VM).
But now there it is: I'm note sure if it was created by the
mm-lsp-server set.mm
command.

Here's the content:
20:00:56 [INFO] Parsing database set.mm
20:01:04 [INFO] Starting server
20:02:00 [ERROR] Error when starting server: ServerError(ProtocolError("expected initialize request, got Err(RecvError)"))

There are also sever logs in the "Output" view, when you select "Metamath Server" in the drop-down menu.

I don't have "Metamath Server", but I have many others, among which "Log (Extension Host)"

Here an interesting part of the log:

[2022-02-28 20:59:03.655] [exthost] [error] Activating extension tirix.metamath failed due to an error:
[2022-02-28 20:59:03.655] [exthost] [error] Error: Cannot find module 'vscode-languageclient'
Require stack:
- /home/mionome/.vscode/extensions/tirix.metamath-0.0.1/out/extension.js
- /usr/share/code/resources/app/out/vs/loader.js
- /usr/share/code/resources/app/out/bootstrap-amd.js
- /usr/share/code/resources/app/out/bootstrap-fork.js
	at Function.Module._resolveFilename (internal/modules/cjs/loader.js:934:15)
	at Module._load (internal/modules/cjs/loader.js:779:27)
	at Function.f._load (electron/js2c/asar_bundle.js:5:12913)
	at Function.i._load (/usr/share/code/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:112:32271)
	at Function.p._load (/usr/share/code/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:112:28855)
	at Function.v._load (/usr/share/code/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:107:60382)
	at Module.require (internal/modules/cjs/loader.js:1006:19)
	at h (/usr/share/code/resources/app/out/vs/loader.js:4:699)
	at Object.<anonymous> (/home/mionome/.vscode/extensions/tirix.metamath-0.0.1/out/extension.js:15:33)
	at Module.u._compile (/usr/share/code/resources/app/out/vs/loader.js:4:1313)
	at Object.Module._extensions..js (internal/modules/cjs/loader.js:1155:10)
	at Module.load (internal/modules/cjs/loader.js:982:32)
	at Module._load (internal/modules/cjs/loader.js:823:14)
	at Function.f._load (electron/js2c/asar_bundle.js:5:12913)
	at Function.i._load (/usr/share/code/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:112:32271)
	at Function.p._load (/usr/share/code/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:112:28855)
	at Function.v._load (/usr/share/code/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:107:60382)
	at Module.require (internal/modules/cjs/loader.js:1006:19)
	at require (internal/modules/cjs/helpers.js:88:18)
	at Function.r [as __$__nodeRequire] (/usr/share/code/resources/app/out/vs/loader.js:5:101)
	at w._loadCommonJSModule (/usr/share/code/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:112:30425)
	at w._doActivateExtension (/usr/share/code/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:98:13341)
	at w._activateExtension (/usr/share/code/resources/app/out/vs/workbench/services/extensions/node/extensionHostProcess.js:98:12293)
	at processTicksAndRejections (internal/process/task_queues.js:93:5)
	at async Promise.all (index 0)

I also have a "Log (Window)" option. Here's an interesting part of that log

[2022-02-28 20:59:03.447] [renderer1] [error] Unable to load and parse grammar for scope source.metamath-proof from file:///<omitfullpath>/.vscode/extensions/tirix.metamath-0.0.1/syntaxes/metamath-proof.tmLanguage.json {"fileOperationResult":1,"options":{"preferUnbuffered":true}}
[2022-02-28 20:59:03.448] [renderer1] [error] No grammar provided for <source.metamath-proof>: Error: No grammar provided for <source.metamath-proof>
    at d (vscode-file://vscode-app/usr/share/code/resources/app/node_modules.asar/vscode-textmate/release/main.js:1:3170)
    at e.processQueue (vscode-file://vscode-app/usr/share/code/resources/app/node_modules.asar/vscode-textmate/release/main.js:1:2533)
    at e.<anonymous> (vscode-file://vscode-app/usr/share/code/resources/app/node_modules.asar/vscode-textmate/release/main.js:1:30633)
    at vscode-file://vscode-app/usr/share/code/resources/app/node_modules.asar/vscode-textmate/release/main.js:1:28677
    at Object.next (vscode-file://vscode-app/usr/share/code/resources/app/node_modules.asar/vscode-textmate/release/main.js:1:28782)
    at s (vscode-file://vscode-app/usr/share/code/resources/app/node_modules.asar/vscode-textmate/release/main.js:1:27496)

BR
Glauco

glacode · 2022-02-28T20:30:30Z

For the message

.vscode/extensions/tirix.metamath-0.0.1/syntaxes/metamath-proof.tmLanguage.json

I've now checked and I actually have

.vscode/extensions/tirix.metamath-0.0.1/syntaxes/metamath.tmLanguage.json

so I hope this shoud be an easy fix :-)

tirix · 2022-03-01T03:19:19Z

Hi Glauco!

Ok, so this is going into several different directions:

The "Log (Extension Host)" relates to extension development, but the error it mentions ("Cannot find module 'vscode-languageclient'") prompted me to check the dependencies, and I think I might have found and fixed an error there.
Concerning your last message about the tmLanguage.json file, you're right. Syntax highlighting was not working. This was already fixed in commit 9696673. In that commit I'm providing (basic) syntax highlighting for both .mm and .mmp files. Syntax highlighting is purely done in VsCode, so this shall work for you even if the LSP client-server link does not, and this shall be relatively easy to fix.

I've published a new version v0.0.2, which includes both this dependency fix and the syntax highlighting fix.
Since you have installed the extension, you can normally just update it from VsCode (no need to run the extension in an extension host anymore, this is the extension development environment).
I hope this will help!
_
Thierry

tirix · 2022-03-03T03:33:10Z

Hi @glacode,

I've tried on a blank installation and found another possible cause: the name of the LSP server executable is mm-lsp-server, however in the default configuration of the plugin was set to metamath-lsp.

In order to fix this, you have to go to "Settings", search settings for "metamath", and set the executable path to mm-lsp-server. In commit 0f07978, I've changed the default path configuration so that it shall not happen for new installations (once this change is published).
_
Thierry

glacode · 2022-03-03T22:54:43Z

In order to fix this, you have to go to "Settings", search settings for "metamath", and set the executable path to mm-lsp-server

@tirix now it works (mostly, see below), and it's supercool!

syntax highlighting was already working, it still works, for .mmp files (I guess this is not the semantic s. h. that LSP could provide, is it?)
hover works perfectly on labels (local .mmt are not considered, but it was expected); it doesn't work on constants, I don't know if you plan to add it later (I understand that some additional work is needed to get "useful" information and it would probably be a set.mm specific solution, so I don't know if it's worth it)
Go To Defiition works perfectly
but when set.mm has been opened , in the Ouput window there's this error message (I guess because no syntax highlighting is applied to .mm )
[Error - 11:38:22 PM] Request textDocument/documentHighlight failed.
Message: Not implemented
Code: -32601
'Go To References' returns this error (I guess it's not implemented, yet)
[Error - 11:46:24 PM] Request textDocument/references failed.
Message: Not implemented
Code: -32601
"Peek > Peed Definition" works perfectly and it's damn cool! :-)
'Peek > Peek References' returns this error (I guess it's not implemented, yet)
[Error - 11:49:06 PM] Request textDocument/references failed.
Message: Not implemented
Code: -32601
'FInd All References", same error:
[Error - 11:51:33 PM] Request textDocument/references failed.
Message: Not implemented
Code: -32601

Can't wait for next release! :-)

Glauco

tirix · 2022-03-04T01:58:21Z

Excellent! Thanks for your patience, being the first to try it out you're going to have a tougher ride...

Syntax highlighting is still very basic and only makes a difference for e.g. labels vs. formulas vs. comment. A semantic analysis would allow to have the same highlighting as the web page, with different colors for constants and set, class or wff variables.
When negotiating capabilities, the LSP server currently pretends it can do everything, but when the actual requests come its replies with "Not Implemented", therefore the errors. This is of course not the right way to do it, I'll fix the capabilities so that these errors disappear.
Hover and "definition" on formulas shall work with the latest commits, if you checkout the latest Git version of this repository and re-install the LSP server (cargo install --path metamath-vspa/metamath-lsp ), it shall work. However it's still not perfect,
What about "Show Proof", does it work well too?

glacode · 2022-03-05T23:33:35Z

I see nice progress here :-)

now also hover on variables works
I'm instead 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.
Now "Go to References" and "Peek References" both work! (is there any difference between the two?)
"Find all references" also works!!
in my previous post, I forgot to write about "Show Proof" : it opens an empty new tab

BR
Glauco

tirix · 2022-03-06T03:00:27Z

Hi Glauco!

Nice! In order to keep organized, let's keep one GitHub issue for one problem: If you agree I'd like to close this one, so as to show one problem is fixed ("Nothing happens"), and have two new issues for the new problems:

Crash when hovering on a constant (I could reproduce, it shall be relatively easy to fix)
"Show Proof" opens an empty tab

About the difference between "Peek References" and "Go to References", it looks like the result is the same when there are several references. However, when there is a single reference, with "Go to References" VsCode directly jumps to the position, but only gives a peek with "Peek References". This behaviour is part of VsCode anyway, the Metamath extension itself is only providing the list of references with their locations.

BR,
_
Thierry

glacode closed this as completed Mar 6, 2022

tirix mentioned this issue Mar 6, 2022

LSP server crashes when hovering on constants #6

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

trying to test it #2

trying to test it #2

glacode commented Feb 25, 2022

tirix commented Feb 26, 2022 •

edited

Loading

tirix commented Feb 27, 2022

glacode commented Feb 27, 2022

tirix commented Feb 27, 2022 •

edited

Loading

glacode commented Feb 28, 2022 •

edited by tirix

Loading

glacode commented Feb 28, 2022 •

edited by tirix

Loading

tirix commented Mar 1, 2022

tirix commented Mar 3, 2022

glacode commented Mar 3, 2022

tirix commented Mar 4, 2022

glacode commented Mar 5, 2022

tirix commented Mar 6, 2022

trying to test it #2

trying to test it #2

Comments

glacode commented Feb 25, 2022

tirix commented Feb 26, 2022 • edited Loading

tirix commented Feb 27, 2022

glacode commented Feb 27, 2022

tirix commented Feb 27, 2022 • edited Loading

glacode commented Feb 28, 2022 • edited by tirix Loading

glacode commented Feb 28, 2022 • edited by tirix Loading

tirix commented Mar 1, 2022

tirix commented Mar 3, 2022

glacode commented Mar 3, 2022

tirix commented Mar 4, 2022

glacode commented Mar 5, 2022

tirix commented Mar 6, 2022

tirix commented Feb 26, 2022 •

edited

Loading

tirix commented Feb 27, 2022 •

edited

Loading

glacode commented Feb 28, 2022 •

edited by tirix

Loading

glacode commented Feb 28, 2022 •

edited by tirix

Loading