Skip to content

Couldn't enable opam-switch-mode in Coq projects #8085

@lzy0505

Description

@lzy0505

I confirm that...

  • I have searched the issue tracker, documentation, FAQ, Discourse, and Google, in case this issue has already been reported/resolved.

  • I have read "How to Debug Issues", and will use it to provide as much information about this issue as possible.

  • The issue can be reproduced on the latest available commit of Doom.

  • The issue can be reproduced on a stable release of Emacs, such as 27, 28, or 29. (Unstable versions end in .50, .60, or .9x)

Expected behavior

When I enable opam-switch-mode in a Coq project, there shouldn't be any errors.

Current behavior

I got opam-switch-set-switch: Symbol’s function definition is void: tuareg-opam-current-compiler.

This bug seems to have been introduced after #7806, which calls this function when first loading opam-switch-mode, regardless of whether the tuareg package (the OCaml mode) is loaded.

While opam is commonly used for OCaml projects, it is also used in some Coq projects.

Steps to reproduce

  1. Enable coq module config.el
  2. Open a .v file in a Coq project
  3. M-x opam-switch-mode

System Information

https://pastebin.com/fEe1nJcK

Metadata

Metadata

Assignees

No one assigned

    Labels

    is:bugSomething isn't working as intendedneeds-triageIssue hasn't been assessed yet

    Type

    Open to PRs

    None yet

    Priority

    None yet

    Projects

    Status
    No status

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions