* company-coq giving company-math not found
@ 2024-05-05 22:50 Heime
2024-05-06 3:14 ` Stefan Monnier via Users list for the GNU Emacs text editor
0 siblings, 1 reply; 5+ messages in thread
From: Heime @ 2024-05-05 22:50 UTC (permalink / raw)
To: Heime via Users list for the GNU Emacs text editor
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 ?
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: company-coq giving company-math not found
2024-05-05 22:50 company-coq giving company-math not found Heime
@ 2024-05-06 3:14 ` Stefan Monnier via Users list for the GNU Emacs text editor
2024-05-06 10:37 ` Heime
0 siblings, 1 reply; 5+ messages in thread
From: Stefan Monnier via Users list for the GNU Emacs text editor @ 2024-05-06 3:14 UTC (permalink / raw)
To: help-gnu-emacs
> What could be the problem ?
Emacs told you the problem:
"No such file or directory" "company-math"
- Stefan
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: company-coq giving company-math not found
2024-05-06 3:14 ` Stefan Monnier via Users list for the GNU Emacs text editor
@ 2024-05-06 10:37 ` Heime
2024-05-06 12:43 ` Heime
2024-05-06 13:48 ` Stefan Monnier
0 siblings, 2 replies; 5+ messages in thread
From: Heime @ 2024-05-06 10:37 UTC (permalink / raw)
To: Stefan Monnier; +Cc: help-gnu-emacs
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.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: company-coq giving company-math not found
2024-05-06 10:37 ` Heime
@ 2024-05-06 12:43 ` Heime
2024-05-06 13:48 ` Stefan Monnier
1 sibling, 0 replies; 5+ messages in thread
From: Heime @ 2024-05-06 12:43 UTC (permalink / raw)
To: Heime; +Cc: Stefan Monnier, help-gnu-emacs
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) ?
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: company-coq giving company-math not found
2024-05-06 10:37 ` Heime
2024-05-06 12:43 ` Heime
@ 2024-05-06 13:48 ` Stefan Monnier
1 sibling, 0 replies; 5+ messages in thread
From: Stefan Monnier @ 2024-05-06 13:48 UTC (permalink / raw)
To: Heime; +Cc: help-gnu-emacs
>> > 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
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2024-05-06 13:48 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2024-05-05 22:50 company-coq giving company-math not found Heime
2024-05-06 3:14 ` Stefan Monnier via Users list for the GNU Emacs text editor
2024-05-06 10:37 ` Heime
2024-05-06 12:43 ` Heime
2024-05-06 13:48 ` Stefan Monnier
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).