generic/proof-autoloads causes emacs startup error trying to load `../lib/holes`, which has been removed

[cxandru]

As described. My init.el file has the following lines related to Rocq:

(setq company-coq-live-on-the-edge t)
(use-package proof-general
  :hook (coq-mode . company-coq-mode)
  :custom (coq-compile-before-require t)
  )

[cxandru]

@Matafou

[Matafou]

Hello. Thnaks for reporting. Does it also happen when you remove company-coq?

[cxandru]

yes

[cxandru]

I mean that should be unsurprising, after all, the call to (autoload <...> ../lib/holes) is in generic/proof-autoloads.el, which is in this library

[Matafou]

It is true that the autoload should be removed and I will do it quickly. But I can't reproduce the bug myself. At least with an emacs with nothing more than use-package and the config you gave above.

[Matafou]

It occurs only if I call holes-mode by hand.

[cxandru]

Any update on this? I' sorry but I don't understand the rationale of 649f8f0 being merged while references remain in the codebase to a now-deleted file. If the intent was to remove this library, this should have been done project-wide. The fact that not every execution trace leads to an error seems immaterial to me. I will make a PR myself if you don't currently have the capacity to fix this

[Matafou]

Hello. Sorry I am very busy at the moment. Please feel free to do the PR if you have time. It is clearly an oversight.