Почему Proof General так медленно работает в Windows 10? - PullRequest
Новая
       61

Почему Proof General так медленно работает в Windows 10?

0 голосов
/ 17 февраля 2020

Я открываю emacs, а затем файл .v, чтобы вызвать Proof General. Тем не менее, один это сделано, IDE очень медленный, и требуются годы, чтобы прокрутить доказательство. Любая идея о том, почему это может происходить?

Файл конфигурации: 

;; use standard keys for undo cut copy paste
(cua-mode 1)

;; disable bell sound
(setq ring-bell-function 'ignore)

(defun proof-retract-buffer-stay ()
  "Call proof-retract-buffer, but retain position"
  (interactive)
  (proof-retract-buffer nil)
  )

;; keybindings for forward and backward Coq
;; disable C-c C-v from ProofGeneral
(eval-after-load "proof-script" '(progn
  (define-key proof-mode-map (kbd "C-M-<down>") 'proof-assert-next-command-interactive)
  (define-key proof-mode-map (kbd "C-M-<up>") 'proof-undo-last-successful-command)
  (define-key proof-mode-map (kbd "C-M-<left>") 'proof-retract-buffer-stay)
  (define-key proof-mode-map (kbd "C-M-<right>") 'proof-goto-point)
  (define-key proof-mode-map (kbd "C-c C-v") nil)
  (set-face-background 'proof-locked-face "#88D9FF")
))

(eval-after-load "coq" '(progn
  (set-face-background 'coq-cheat-face "#ffe87a")
  (set-face-foreground 'coq-cheat-face "#ff141d")
))

;; start maximized
(toggle-frame-maximized)

;; disable Proof General splash screen
(setq proof-splash-enable nil)

;; disable emacs splash screen
(setq inhibit-startup-screen t)

;; forces hybrid mode for displaying Coq buffers
(setq proof-three-window-mode-policy 'hybrid)

;; MELA repo
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)

;; company-coq!
(add-hook 'coq-mode-hook #'company-coq-mode)
(setq company-coq-live-on-the-edge t)
...