Cannot find Proof General Directory on Windows 10

[luochen1990]

trafficstars

File error: Cannot open load file, No such file or directory, /usr/local/share/emacs/site-lisp/proof-general/generic/proof-site

[njmaeff]

I was able to fix this by updating the config.el file. I use .spacemacs.d for my configuration and I downloaded proof-general to %USERPROFILE%\.spacemacs.d\bin.

diff --git a/config.el b/config.el
index c243f3d..b678634 100644
--- a/config.el
+++ b/config.el
@@ -9,6 +9,6 @@
 ;;
 ;;; License: GPLv3

-(defvar proof-general-path "/usr/local/share/emacs/site-lisp/proof-general/generic/proof-site"
+(defvar proof-general-path (concat (getenv "USERPROFILE") "\\.spacemacs.d\\bin\\proof-general-20190523.740\\generic\\proof-site.el")
   "The path to proof general")

[CJex]

The path can be set in ~/.spacemacs section dotspacemacs/user-init:

(defun dotspacemacs/user-init ()
  (setq proof-general-path ("/your/local/git/PG/generic/proof-site")))

The cons is that we have to clone and make PG manually, add proof-general to dotspacemacs-additional-packages seems not work.

My emacs config: https://github.com/CJex/syslocal/tree/master/etc/emacs