How To Install emacs-common-proofgeneral on Fedora 36

In this tutorial we learn how to install emacs-common-proofgeneral in Fedora 36. emacs-common-proofgeneral is Emacs mode for standard interaction interface for proof assistants

Introduction

In this tutorial we learn how to install emacs-common-proofgeneral on Fedora 36.

What is `emacs-common-proofgeneral`

Proof General is a generic front-end for proof assistants (also known as interactive theorem provers) based on Emacs. Proof General allows one to edit and submit a proof script to a proof assistant in an interactive manner - It tracks the goal state, and the script as it is submitted, and allows for easy backtracking and block execution. - It adds toolbars and menus to Emacs for easy access to proof assistant features. - It integrates with Emacs Unicode support for some provers to provide output using proper mathematical symbols. - It includes utilities for generating Emacs tags for proof scripts, allowing for easy navigation. Proof General supports a number of different proof assistants (Isabelle, Coq, PhoX, and LEGO to name a few) and is designed to be easily extendable to work with others.

We can use yum or dnf to install emacs-common-proofgeneral on Fedora 36. In this tutorial we discuss both methods but you only need to choose one of method to install emacs-common-proofgeneral.

Install emacs-common-proofgeneral on Fedora 36 Using dnf

Update yum database with dnf using the following command.

sudo dnf makecache --refresh

After updating yum database, We can install emacs-common-proofgeneral using dnf by running the following command:

sudo dnf -y install emacs-common-proofgeneral

Install emacs-common-proofgeneral on Fedora 36 Using yum

Update yum database with yum using the following command.

sudo yum makecache --refresh

After updating yum database, We can install emacs-common-proofgeneral using yum by running the following command:

sudo yum -y install emacs-common-proofgeneral

How To Uninstall emacs-common-proofgeneral on Fedora 36

To uninstall only the emacs-common-proofgeneral package we can use the following command:

sudo dnf remove emacs-common-proofgeneral

emacs-common-proofgeneral Package Contents on Fedora 36

/usr/bin/coqtags
/usr/bin/isartags
/usr/bin/legotags
/usr/bin/proofgeneral
/usr/share/application-registry/proofgeneral.applications
/usr/share/applications/proofgeneral.desktop
/usr/share/doc/proofgeneral
/usr/share/doc/proofgeneral/AUTHORS
/usr/share/doc/proofgeneral/BUGS
/usr/share/doc/proofgeneral/CHANGES
/usr/share/doc/proofgeneral/COMPATIBILITY
/usr/share/doc/proofgeneral/PG-adapting.pdf
/usr/share/doc/proofgeneral/ProofGeneral.pdf
/usr/share/doc/proofgeneral/REGISTER
/usr/share/doc/proofgeneral/acl2
/usr/share/doc/proofgeneral/acl2/example.acl2
/usr/share/doc/proofgeneral/acl2/root2.acl2
/usr/share/doc/proofgeneral/hol98
/usr/share/doc/proofgeneral/hol98/example.sml
/usr/share/doc/proofgeneral/hol98/root2.sml
/usr/share/doc/proofgeneral/isar
/usr/share/doc/proofgeneral/isar/Example-Tokens.thy
/usr/share/doc/proofgeneral/isar/Example.thy
/usr/share/doc/proofgeneral/lego
/usr/share/doc/proofgeneral/lego/example.l
/usr/share/doc/proofgeneral/lego/example2.l
/usr/share/doc/proofgeneral/lego/root2.l
/usr/share/doc/proofgeneral/pgshell
/usr/share/doc/proofgeneral/pgshell/example.pgsh
/usr/share/doc/proofgeneral/phox
/usr/share/doc/proofgeneral/phox/sqrt2.phx
/usr/share/doc/proofgeneral/twelf
/usr/share/doc/proofgeneral/twelf/example.elf
/usr/share/icons/hicolor/128x128/apps/proofgeneral.png
/usr/share/icons/hicolor/16x16/apps/proofgeneral.png
/usr/share/icons/hicolor/256x256/apps/proofgeneral.png
/usr/share/icons/hicolor/32x32/apps/proofgeneral.png
/usr/share/icons/hicolor/48x48/apps/proofgeneral.png
/usr/share/icons/hicolor/64x64/apps/proofgeneral.png
/usr/share/icons/hicolor/96x96/apps/proofgeneral.png
/usr/share/info/PG-adapting.info.gz
/usr/share/info/ProofGeneral.info.gz
/usr/share/licenses/emacs-common-proofgeneral
/usr/share/licenses/emacs-common-proofgeneral/COPYING
/usr/share/man/man1/proofgeneral.1.gz
/usr/share/metainfo/io.github.proofgeneral.metainfo.xml
/usr/share/mime-info/proofgeneral.keys
/usr/share/mime-info/proofgeneral.mime

References

emacs-common-proofgeneral website

Summary

In this tutorial we learn how to install emacs-common-proofgeneral on Fedora 36 using yum and [dnf]((/fedora/36/dnf/).