使用 Homebrew 安装 proof-general

项目链接

• 主页
• 仓库
• 软件包管理器页面

命令和别名

• coqtags

项目历史

The project began in 1994 as Thomas Kleymann's LEGO mode, influenced by David Aspinall's earlier Isamode interface for Isabelle. Script management and proof-by-pointing work made the implementation increasingly generic.

After substantial re-engineering for multiple proof systems, the interface was renamed Proof General. Proof General 2.0 became the first official release under the improved, prover-independent design in December 1998.

采用历史

Proof General grew from an interface for LEGO into a generic environment supporting multiple proof assistants. Its history records use by about 50 students working with Coq, Isabelle, and LEGO at the 1999 Types Summer School.

Its enduring niche is the Emacs-based formal-methods community, where proof scripts can be edited, incrementally submitted to a prover, and replayed through a common interface.

使用方式

Open a supported proof-script file in Emacs, then use Proof General's commands, menus, or toolbar to submit regions incrementally to the proof assistant and inspect its responses.

Proof General can be loaded and customized through `~/.emacs`; its Customize interface also saves user preferences there. The prover executable can be selected through assistant-specific settings.

为什么软件包爱好者会关心

Proof General is an early and influential example of separating a proof-assistant user interface from the underlying prover. Package enthusiasts care about its long Emacs lineage, multi-prover architecture, and role in making interactive theorem proving feel like an editor-integrated development workflow.

时间线

• 1994: Development began as an Emacs interface called LEGO mode.
• May 1995: The last official LEGO mode release appeared.
• November 1996: Work on proof-by-pointing accelerated the interface's generalization.
• December 1998: Proof General 2.0 became the first official release under the new name.
• August 1999: Proof General 2.1 was released and subsequently used at the Types Summer School.

Related projects

• Proof General is implemented as an extension to GNU Emacs and includes modes for proof assistants such as Coq and EasyCrypt. Its documentation also describes adapting the generic framework to additional provers.

来源

• https://proofgeneral.github.io/about/
• https://proofgeneral.github.io/doc/master/userman/History-of-Proof-General/
• https://proofgeneral.github.io/doc/master/userman/Obtaining-and-Installing/