Giter Club home page Giter Club logo

pg's Introduction

Proof General โ€” Organize your proofs!

CI NonGNU ELPA MELPA MELPA Stable
ProofGeneral doc PG-adapting doc

Overview

Proof General is a generic Emacs interface for proof assistants. The aim of the Proof General project is to provide a powerful, generic environment for using interactive proof assistants.

This is version 4.6-git of Proof General.

About Proof General branches

Two editions of Proof General are currently available:

  • the (standard) REPL-based, stable version of Proof General, gathered in the master branch;
  • the (unmaintained) Coq-specific, experimental version of Proof General, supporting asynchronous proof processing, gathered in the async branch.

Installing Proof General

Proof General requires GNU Emacs 25.2 or later.

The current policy aims at supporting multiple Emacs versions, including those available in Debian Stable as well as in Ubuntu LTS distributions until their End-Of-Support.

Using NonGNU ELPA

NonGNU ELPA is the sister repository of GNU ELPA and enabled by default from Emacs 28 onwards. You can directly install Proof General from NonGNU ELPA if the repository is enabled.

Using MELPA

MELPA is a repository of Emacs packages. Skip this step if you already use MELPA. Otherwise, add the following to your .emacs and restart Emacs:

(require 'package)
;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)

Remark: If you have Emacs 26.1 (which is precisely the packaged version in Debian 10), you may get the error message Failed to download 'melpa' archive during the package refresh step. This is a known bug (debbug #34341) which has been fixed in Emacs 26.3 and 27.1, while a simple workaround consists in uncommenting the line (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") above in your .emacs.

Note: If you switch to MELPA from a previously manually-installed Proof General, make sure you removed the old versions of Proof General from your Emacs context (by removing from your .emacs the line loading PG/generic/proof-site, or by uninstalling the proofgeneral package provided by your OS package manager).

Then, run M-x package-refresh-contents RET followed by M-x package-install RET proof-general RET to install and byte-compile proof-general.

You can now open a Coq file (.v), an EasyCrypt file (.ec), a qrhl-tool file (.qrhl), or a PhoX file (.phx) to automatically load the corresponding major mode.

Using Git (manual compilation procedure)

Remove old versions of Proof General, clone the PG repo from GitHub and byte-compile the sources:

git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make

Then add the following to your .emacs:

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

If Proof General complains about a version mismatch, make sure that the shell's emacs is indeed your usual Emacs. If not, run the Makefile again with an explicit path to Emacs. On macOS in particular you'll probably need something like

make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

Keeping Proof General up-to-date

Using MELPA

As explained in the MELPA documentation, updating all MELPA packages in one go is as easy as typing M-x package-list-packages RET then r (refresh the package list), U (mark Upgradable packages), and x (execute the installs and deletions).

Using Git

Assuming you have cloned the repo in ~/.emacs.d/lisp/PG, you would have to run:

cd ~/.emacs.d/lisp/PG
make clean
git pull
make

More info

See:

Links:

Supported proof assistants:

Proof General used to support other proof assistants, but those instances are no longer maintained nor available in the MELPA package:

  • Experimental support of: Shell
  • Obsolete instances: Demoisa
  • Removed instances: Twelf, CCC, Hol-Light, ACL2, Plastic, Lambda-Clam, HOL98, LEGO, Isabelle

A few example proofs are included in each prover subdirectory.

pg's People

Contributors

amahboubi avatar chobbes avatar cpitclaudel avatar craff avatar cyrilanac avatar davidaspinall avatar dominique-unruh avatar dymil avatar eggert avatar erikmd avatar fuyu0425 avatar haselwarter avatar hendriktews avatar jasongross avatar jfehrle avatar liyishuai avatar lsf37 avatar makarius avatar marsam avatar matafou avatar monnier avatar phikal avatar psteckler avatar rgrinberg avatar skyskimmer avatar strub avatar tbrk avatar tchajed avatar vzaliva avatar yuvallanger avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.