company-coq giving company-math not found

company-coq giving company-math not found

[Heime]

I want to use company-coq but getting the error

Debugger entered--Lisp error: 
(file-missing "Cannot open load file" 
  "No such file or directory" "company-math")
  require(company-math) 

with

    (add-to-list 'load-path "~/contrib/company-coq-2016")
    (require 'company-coq)

What could be the problem ?

Re: company-coq giving company-math not found

[Stefan Monnier via Users list for the GNU Emacs text editor]

> What could be the problem ?

Emacs told you the problem:

    "No such file or directory" "company-math"


- Stefan

Re: company-coq giving company-math not found

[Heime]

On Monday, May 6th, 2024 at 3:14 PM, Stefan Monnier via Users list for the GNU Emacs text editor <help-gnu-emacs@gnu.org> wrote:

> > What could be the problem ?
 
> Emacs told you the problem:
> 
> "No such file or directory" "company-math" - Stefan

Have looked at the code and company-math is not a feature defined in
company.  Could be an outside program actually.

Re: company-coq giving company-math not found

[Heime]

Sent with Proton Mail secure email.

On Monday, May 6th, 2024 at 10:37 PM, Heime <heimeborgia@protonmail.com> wrote:

> On Monday, May 6th, 2024 at 3:14 PM, Stefan Monnier via Users list for the GNU Emacs text editor help-gnu-emacs@gnu.org wrote:
>
> > > What could be the problem ?
>
> > Emacs told you the problem:
> >
> > "No such file or directory" "company-math" - Stefan
>
>
> Have looked at the code and company-math is not a feature defined in
> company. Could be an outside program actually.

What is the best thing to do, consider company-math closer to company,
or closer to company-coq (i.e. as a dependency of company-coq) ?

Re: company-coq giving company-math not found

[Stefan Monnier]

>> > What could be the problem ?
>> Emacs told you the problem:
>> "No such file or directory" "company-math" - Stefan
> Have looked at the code and company-math is not a feature defined in
> company.  Could be an outside program actually.

Yes, it's a separate package.  Normally if you installed `company-coq`
via a package manager, `company-math` should have been installed
automatically for you at the same time.

You can install `company-math` via `M-x package-list RET`.


        Stefan