Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Bug?] Incorrect activation events #737

Closed
kands-code opened this issue May 31, 2024 · 4 comments · Fixed by #741
Closed

[Bug?] Incorrect activation events #737

kands-code opened this issue May 31, 2024 · 4 comments · Fixed by #741
Labels
kind: bug Something isn't working part: client (VSCode)
Milestone

Comments

@kands-code
Copy link

Describe the bug

For most plugins in vscode, specific language plugins, such as Java, or Python, the activation events is generally onLanguage:xxx, where xxx represents this language, such as Java:

Screenshot of plugin interface

image

including VsCoq:

Screenshot of plugin interface

image

But the activation events of CoqLSP are markdown and latex:

Screenshot of plugin interface

image

As a result, in some projects not related to Coq, there may be a README.md in the project, and then CoqLSP is activated.

To Reproduce

Steps to reproduce the behavior:

  1. Go to 'Extensions'
  2. Click on 'Coq LSP'
  3. Scroll down to 'Activation Events'

Expected behavior

The activation event of the plugin should be onLanguage:coq

Desktop (please complete the following information):

  • Operating system: macOS 14.5 arm64
  • coq-lsp version: 0.1.8
  • VS Code version:
@kands-code kands-code added the kind: bug Something isn't working label May 31, 2024
@kands-code
Copy link
Author

If you want to add support for "literate coq", I think you can refer to Agda's approach.

{
  // ...
  "contributes": {
    // ...
    "languages": [
      {
        "id": "agda",
        "extensions": [".agda"],
        "aliases": ["Agda"],
        "configuration": "./language-configuration.json",
        "icon": {
          "dark": "./asset/dark.png",
          "light": "./asset/light.png"
        }
      },
      {
        "id": "lagda-md",
        "extensions": [".lagda.md"],
        "aliases": ["Literate Agda (markdown)"],
        "configuration": "./language-configuration.json",
        "icon": {
          "dark": "./asset/dark.png",
          "light": "./asset/light.png"
        }
      },
      {
        "id": "lagda-tex",
        "extensions": [".lagda.tex", ".lagda"],
        "aliases": ["Literate Agda (TeX)"],
        "configuration": "./language-configuration.json",
        "icon": {
          "dark": "./asset/dark.png",
          "light": "./asset/light.png"
        }
      },
      {
        "id": "lagda-rst",
        "extensions": [".lagda.rst"],
        "aliases": ["Literate Agda (reStructuredText)"],
        "configuration": "./language-configuration.json",
        "icon": {
          "dark": "./asset/dark.png",
          "light": "./asset/light.png"
        }
      }
    ]
    // ...
  }
  // ...
}

For example:

{
  // ...
  "contributes": {
    // ...
    "languages": [
      {
        "id": "coq",
        "extensions": [".v"],
        "aliases": ["Coq"],
        "configuration": "./language-configuration.json"
      },
      {
        "id": "coq-md",
        "extensions": [".mv", ".lcoq.md"],
        "aliases": ["Literate Coq (markdown)"],
        "configuration": "./language-configuration.json"
      },
      {
        "id": "coq-tex",
        "extensions": [".lv", ".lcoq.tex"],
        "aliases": ["Literate Coq (TeX)"],
        "configuration": "./language-configuration.json"
      }
    ]
    // ...
  }
  // ...
}

However, I don't know the details of the implementation, so it's just a suggestion.

@ejgallego
Copy link
Owner

Hi @kands-code ,

thanks for the report, the code you quote is for 0.1.9, so indeed the behavior will differ greatly from 0.1.8.

Activaton is a bit complex, as indeed, coq-lsp does want to be activated for some buffers, including those that are literate markdown or LaTeX, but only when the extension is .mv or .lv / .v.tex.

A few comments:

  • In newer VSCode versions, activation events for extensions that contribute a language are implicit, so no need for onLanguage: coq, that's inferred automatically
  • This doesn't work well for extensions that need to improve an extension, in this case, the contributes is not enough, VSCode devs confirmed that activation should be like this, then filter the extensions with a document selector.
  • Even if the extension is activated, nothing should happen in buffers that are not caught by the document selector.

Thanks for the Agda example, we used this approach in the past, however we had the problem
that regular markdown editing facilities are not available, are they in Agda case?

But indeed, in the Agda code, as the extension does contribute the language, the onLanguage event is not needed, but automatically inferred.

See microsoft/vscode#198295 for discussion about this topic.

Any help with this is much appreciated.

@ejgallego
Copy link
Owner

Things seems to work fine in 0.1.9, except for a little detail:

  • indeed, when a .md file is open, the extension is activated, however it correctly does nothing with files that are not in its scope
  • however I see a bug here, the goals windows is created on activation. This is a bug, I will fix it ASAP. The goals window should be created only when goals are to be displayed, or when the language server client is started.

We will release a 0.1.9.1 bugfix ASAP (also to tweak a few other things).

@ejgallego
Copy link
Owner

@kands-code , the 0.1.10 version of the extension should behave much better, thanks for the report and testing.

Don't hesitate to reopen if the coq-lsp extension gets in the way again.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Something isn't working part: client (VSCode)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants