proof-general
- Description
- A generic Emacs interface for proof assistants
- Latest
- proof-general-4.6snapshot0.20241004.113700.tar (.sig), 2024-Oct-04, 3.39 MiB
- Maintainer
- <proof-general-maintainers@groupes.renater.fr>
- Website
- https://proofgeneral.github.io/
- Browse ELPA's repository
- CGit or Gitweb
- Badge
- Manual
- ProofGeneral
To install this package from Emacs, use package-install
or list-packages
.
Full description
Proof General is a generic Emacs interface for proof assistants (also known as interactive theorem provers). It is supplied ready to use for the proof assistants Coq, EasyCrypt, qrhl-tool, and PhoX. See https://proofgeneral.github.io/ for installation instructions and online documentation. Or browse the accompanying info manual: (info-display-manual "ProofGeneral") Regarding the Coq proof assistant, you may be interested in the company-coq extension of ProofGeneral (also available in MELPA).
Old versions
proof-general-4.6snapshot0.20240912.155825.tar.lz | 2024-Sep-12 | 964 KiB |
proof-general-4.6snapshot0.20240909.140904.tar.lz | 2024-Sep-09 | 963 KiB |
proof-general-4.6snapshot0.20240902.112159.tar.lz | 2024-Sep-02 | 964 KiB |
proof-general-4.6snapshot0.20240708.152546.tar.lz | 2024-Jul-10 | 964 KiB |
proof-general-4.6snapshot0.20240619.120959.tar.lz | 2024-Jun-19 | 964 KiB |
proof-general-4.6snapshot0.20240513.72008.tar.lz | 2024-May-13 | 963 KiB |
proof-general-4.6snapshot0.20231219.82832.tar.lz | 2023-Dec-19 | 955 KiB |
proof-general-4.6snapshot0.20221130.94645.tar.lz | 2022-Nov-30 | 954 KiB |
proof-general-4.5.0.20220713.161818.tar.lz | 2022-Jul-13 | 952 KiB |
proof-general-4.5snapshot0.20220707.75856.tar.lz | 2022-Jul-07 | 951 KiB |
News
-*- outline -*- This is a summary of main changes. For details, please see the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG * Changes of Proof General 4.6 from Proof General 4.5 ** Generic changes *** Improve the omit-proofs feature to handle a number of cases where proofs must not be omitted. *** Renew support for proof-tree visualization via the external command prooftree, see http://askra.de/software/prooftree and Section 7 "Graphical Proof-Tree Visualization" in the Proof General manual. Proof-tree visualization is currently only supported for Coq. The prooftree support has been substantially rewritten, making use of the much better support since Coq version 8.11. *** New command `proof-check-report' to generates the proof status of all opaque proofs. Currently only available for Coq, see Coq changes below for more details. *** New command `proof-check-annotate' to annotate all failing proofs with FAIL comments. ** Coq changes *** support Coq 8.19 **** New option coq-compile-coqdep-warnings to configure the warning command line argument (-w) of coqdep. The default of this option is +module-not-found to let Proof General reliably detect missing modules as coqdep error. *** Renew support for proof-tree visualization, see description in generic changes above. *** New command `proof-check-report to generates the proof status of all opaque proofs. This command is useful for a development process where invalid proofs are permitted and vos compilation and the omit proofs feature are used to work at the most interesting or challenging point instead of on the first invalid proof. The command generates a list of all opaque proofs in the current buffer together with the information whether the proof script is currently valid or invalid. The command can also be run in batch mode, for instance in a continuous integration environment. *** New command `proof-check-annotate' to annotate all failing proofs with FAIL comments. Useful in the development process as described above to ensure all currently failing proofs are marked as such. *** flag Printing Parentheses and Printing Notations can be set/unset via menu and Coq keymap (C-c C-a C-9 and C-c C-a C-0 for Parentheses (optimized for British and American keyboards); C-c C-a n and C-c C-a N for Notations). *** New options coq-compile-extra-coqc-arguments and coq-compile-extra-coqdep-arguments to configure additional command line arguments to calls of, respetively, coqc and coqdep during auto compilation. *** Fix issues #687 and #688 where the omit-proofs feature causes errors on correct code. * Changes of Proof General 4.5 from Proof General 4.4 ** Generic changes *** License changed to GPLv3+ *** Remove support for the following systems: Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, Isabelle, HOL98. *** require GNU Emacs 25.2 or later The current policy aims at supporting multiple Emacs versions, including those available in distributions Debian Stable (https://packages.debian.org/stable/emacs) and Ubuntu LTS (https://packages.ubuntu.com/emacs), until their End-Of-Support (see also https://wiki.ubuntu.com/Releases). Support for Emacs 25 will be dropped in April 2023 when Ubuntu Bionic reaches end of standard support. *** new command and menu item to easily upgrade all packages - To upgrade all ELPA packages (including ProofGeneral if it was installed via MELPA), do "M-x proof-upgrade-elpa-packages RET" or use the "Proof-General > Upgrade ELPA packages..." menu item *** bug fixes - Using query-replace (or replace-string) in the processed region doesn't wrongly jump to the first match anymore. - cheat face (admit etc) now visible when locked. *** remove key-binding for proof-electric-terminator-toggle - The default key-binding for proof-electric-terminator-toggle (C-c .) was too easy to enter by mistake. And it was not that ... ...