Coq学习——Proof-General使用

Using Proof General

Proof General Home

Features

  • Script management
    • Script file <--> Interactive proof process
    • Colours a script script to show the state in the proof assistant. Hide the completed proofs or undo already processed parts.
  • Simplified interaction model
    • By using PG, the proof assistant's shell is hidden from the user.
    • Via 3 buffers shown as Emacs widgets.
  • Multiple files

Install

This an install tutorial using Spacemacs config personal repository.

original

  • Install Proof General

    1
    2
    3
    4
    mkdir ~/dotspacemacs/private/local
    cd ~/dotspacemacs/private/local
    git clone git@github.com:ProofGeneral/PG.git ProofGeneral
    cd ProofGeneral

  • Install Spacemacs layer from mbrcknl/spacemacs-coq

    1
    2
    cd ~/dotspacemacs/private
    git clone git@github.com:mbrcknl/spacemacs-coq coq