如何在Mac上安装Emacs的验证通用？

Question

我是Emacs的新手，也许这就是问题所在，但我遵循了下面的说明：

https://github.com/ProofGeneral/PG

特别是在我将给定的行添加到我的.emacs文件之后，我做到了(M是alt/选项键)：

M-x package-refresh-contents RET

但我收到了错误信息：

[no match]

出什么问题了？

也许这是我做错的，是什么：

 M-x package-refresh-contents RET followed by M-x package-install RET proof-general RET

卑劣？

Answer 1

这就是对我(TM)有用的东西：

(require 'package)
(setq package-enable-at-startup nil)
(add-to-list 'package-archives
             '("melpa" . "https://melpa.org/packages/"))

(package-initialize)

;; Bootstrap use-package
(unless (package-installed-p 'use-package)
    (package-refresh-contents)
    (package-install 'use-package))

(use-package proof-general
  :no-require t
  :ensure t)

Answer 2

如果你有蜂巢作为你的包源，这条线就能工作。见ejgallego的回答：

 (require 'package)
 (setq package-enable-at-startup nil)
      (add-to-list 'package-archives
          '("melpa" . "https://melpa.org/packages/"))

 (package-initialize)

如果将这些行添加到.emacs文件中，然后

 M-x package-refresh-contents (followed by return)
 M-x package-install (followed by return and then `proof-general`)

然后，它将在不显式地将包添加到..emacs文件的情况下工作。