[Bug?] Incorrect activation events

[kands-code]

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


including VsCoq:

Screenshot of plugin interface


But the activation events of CoqLSP are markdown and latex:

Screenshot of plugin interface


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]

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]

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 https://github.com/microsoft/vscode/issues/198295 for discussion about this topic.

Any help with this is much appreciated.

[ejgallego]

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]

@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.