From f68203c2ef892700ffac254b1ef95f627f0e06ea Mon Sep 17 00:00:00 2001 From: Henrik Lissner Date: Thu, 3 Oct 2019 11:43:16 -0400 Subject: [PATCH] lang/coq: fix file-missing proof-site errors Occasionally happens after the first time running `doom refresh` (after installing proof-general). --- modules/lang/coq/autoload.el | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/modules/lang/coq/autoload.el b/modules/lang/coq/autoload.el index 624185018..988b0558e 100644 --- a/modules/lang/coq/autoload.el +++ b/modules/lang/coq/autoload.el @@ -1,4 +1,15 @@ ;;; lang/coq/autoload.el -*- lexical-binding: t; -*- +;; HACK `proof-general' ascertains its own library path at compile time in its +;; autoloads file using `byte-compile-current-file' (and stores it in +;; `pg-init--script-full-path'). This means that when +;; `doom-package-autoload-file' is created and byte-compiled, +;; `pg-init--script-full-path' will be wrong, causing file-missing errors as it +;; tries to load `proof-site'. We prevent this by defining these two variables +;; early, in our own autoloads file. +;;;###autoload +(setq pg-init--script-full-path (locate-library "proof-general") + pg-init--pg-root (file-name-directory pg-init--script-full-path)) + ;;;###autoload (add-hook 'coq-mode-hook #'company-coq-mode)