windows - 为什么 Proof General 在 Windows 10 中如此缓慢?
问题描述
我打开 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)
解决方案
推荐阅读
- javascript - 在 AngularJs 的 exportToExcel 过程中不显示加载程序(处理图标)
- c# - Unity2D:按顺序禁用实例化的预制件
- python - 如何在 matplotlib 中自定义每个子图的大小,以使所有子图具有相等的 x 轴比例?
- sql-server - 同时更新相同的行不同的列。僵局
- string - Vb.Net 从字符串中获取报告名称
- javascript - 另一个谷歌地图地理编码问题
- json - 如何在使用 AWS Database Migration Service 将 csv 从 S3 迁移到 RDS 时定义表结构
- javascript - 使用角色时如何正确注销
- typescript - Typescript redux 连接组件类型错误
- javascript - 如何在node.js中将对象存储在数据库中