proofgeneral_4.4.1~pre170114-1_all.deb


Advertisement

Description

proofgeneral - generic frontend for proof assistants

Property Value
Distribution Ubuntu 17.10 (Artful Aardvark)
Repository Ubuntu Universe i386
Package name proofgeneral
Package version 4.4.1~pre170114
Package release 1
Package architecture all
Package type deb
Installed size 1.98 KB
Download size 529.89 KB
Official Mirror archive.ubuntu.com
Proof General is a major mode to turn Emacs into an interactive proof
assistant to write formal mathematical proofs using a variety of
theorem provers.
This package provides Proof General support for Coq. (There is no
other proof assistant that one could sensibly support.)

Alternatives

Package Version Architecture Repository
proofgeneral_4.4.1~pre170114-1_all.deb 4.4.1~pre170114 all Ubuntu Universe
proofgeneral - - -

Requires

Name Value
emacs24 -
emacs25 -
mmm-mode -

Conflicts

Name Value
proofgeneral-coq -
proofgeneral-minlog -
proofgeneral-misc -

Replaces

Name Value
proofgeneral-coq -
proofgeneral-misc -

Download

Type URL
Binary Package proofgeneral_4.4.1~pre170114-1_all.deb
Source Package proofgeneral

Install Howto

  1. Update the package index:
    # sudo apt-get update
  2. Install proofgeneral deb package:
    # sudo apt-get install proofgeneral

Files

Path
/etc/emacs/site-start.d/50proofgeneral.el
/usr/bin/coqtags
/usr/bin/proofgeneral
/usr/lib/emacsen-common/packages/compat/proofgeneral
/usr/lib/emacsen-common/packages/install/proofgeneral
/usr/lib/emacsen-common/packages/remove/proofgeneral
/usr/share/application-registry/proofgeneral.applications
/usr/share/applications/proofgeneral.desktop
/usr/share/doc/proofgeneral/AUTHORS
/usr/share/doc/proofgeneral/BUGS
/usr/share/doc/proofgeneral/COMPATIBILITY
/usr/share/doc/proofgeneral/FAQ.md.gz
/usr/share/doc/proofgeneral/README.Debian
/usr/share/doc/proofgeneral/README.md
/usr/share/doc/proofgeneral/REGISTER
/usr/share/doc/proofgeneral/changelog.Debian.gz
/usr/share/doc/proofgeneral/copyright
/usr/share/doc/proofgeneral/examples/coq_example.v
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-abbrev.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-autotest.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-compile-common.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-db.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-indent.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-local-vars.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-mmm.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-par-compile.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-par-test.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-seq-compile.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-smie.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-syntax.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-system.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq-unicode-tokens.el
/usr/share/emacs/site-lisp/proofgeneral/coq/coq.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-assoc.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-autotest.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-custom.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-goals.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-movie.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-pamacs.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-pbrpm.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-pgip.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-response.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-user.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-vars.el
/usr/share/emacs/site-lisp/proofgeneral/generic/pg-xml.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-autoloads.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-auxmodes.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-config.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-depends.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-easy-config.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-faces.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-indent.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-maths-menu.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-menu.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-mmm.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-script.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-shell.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-site.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-splash.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-syntax.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-toolbar.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-tree.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-unicode-tokens.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-useropts.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof-utils.el
/usr/share/emacs/site-lisp/proofgeneral/generic/proof.el
/usr/share/emacs/site-lisp/proofgeneral/hol-light/hol-light-autotest.el
/usr/share/emacs/site-lisp/proofgeneral/hol-light/hol-light-unicode-tokens.el
/usr/share/emacs/site-lisp/proofgeneral/hol-light/hol-light.el
/usr/share/emacs/site-lisp/proofgeneral/images/ProofGeneral-splash.png
/usr/share/emacs/site-lisp/proofgeneral/images/ProofGeneral.png
/usr/share/emacs/site-lisp/proofgeneral/images/README
/usr/share/emacs/site-lisp/proofgeneral/images/epg-abort.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-abort.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-command.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-command.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-context.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-context.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-find.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-find.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-goal.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-goal.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-goto.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-goto.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-help.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-help.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-home.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-home.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-info.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-info.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-interrupt.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-interrupt.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-next.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-next.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-prooftree.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-prooftree.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-qed.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-qed.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-restart.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-restart.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-retract.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-retract.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-state.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-state.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-undo.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-undo.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/epg-use.png
/usr/share/emacs/site-lisp/proofgeneral/images/epg-use.xpm
/usr/share/emacs/site-lisp/proofgeneral/images/hiddenproof.xpm
/usr/share/emacs/site-lisp/proofgeneral/lib/bufhist.el
/usr/share/emacs/site-lisp/proofgeneral/lib/holes.el
/usr/share/emacs/site-lisp/proofgeneral/lib/local-vars-list.el
/usr/share/emacs/site-lisp/proofgeneral/lib/maths-menu.el
/usr/share/emacs/site-lisp/proofgeneral/lib/pg-dev.el
/usr/share/emacs/site-lisp/proofgeneral/lib/pg-fontsets.el
/usr/share/emacs/site-lisp/proofgeneral/lib/proof-compat.el
/usr/share/emacs/site-lisp/proofgeneral/lib/scomint.el
/usr/share/emacs/site-lisp/proofgeneral/lib/span.el
/usr/share/emacs/site-lisp/proofgeneral/lib/texi-docstring-magic.el
/usr/share/emacs/site-lisp/proofgeneral/lib/unicode-chars.el
/usr/share/emacs/site-lisp/proofgeneral/lib/unicode-tokens.el
/usr/share/icons/hicolor/16x16/proofgeneral.png
/usr/share/icons/hicolor/32x32/proofgeneral.png
/usr/share/icons/hicolor/48x48/proofgeneral.png
/usr/share/man/man1/proofgeneral.1.gz
/usr/share/mime-info/proofgeneral.keys
/usr/share/mime-info/proofgeneral.mime
/usr/share/pixmaps/proofgeneral.png

Changelog

2017-01-16 - Hendrik Tews <hendrik@askra.de>
proofgeneral (4.4.1~pre170114-1) unstable; urgency=medium
* Imported Upstream version 4.4.1~pre170114
git hash 6d1f608c6e7c39eff89b9461a2f4ea7ff1b19899
* fix lintian copyright issue
* add patch fix-coqtags and install coqtags
* add emacsen compat file (Closes: #758968)
* add patch desktop-keyword-entry for desktop-entry-lacks-keywords-entry
lintian warning
* disable StartupWMClass towards a solution of #746466
* fix emacs warning inside emacsen-install
2016-12-30 - Richard B. Kreckel <kreckel@debian.org>
proofgeneral (4.4.1~pre161230-0.1) unstable; urgency=medium
* Non-maintainer upload.
* New upstream release.
* Make package work with emacs24 or emacs25 (Closes: #846990).
* debian/control: Remove ${shlib:Depends} for package proofgeneral.
* Drop debian/menu, following tech-ctte decision on #741573.
* debian/README.Debian: Remove special note about prooftree, which
is now a proper Debian package, and added HOL Light as prover.
* debian/*: Adapt to new upstream home at github.
* debian/patches/:
- drop smartly-enable-prooftree
- restrict-installed-provers.patch: added hol-light as prover
- refresh all others
2014-11-16 - intrigeri <intrigeri@debian.org>
proofgeneral (4.3~pre131011-0.2) unstable; urgency=medium
* Non-maintainer upload.
* Remove {build,runtime} alternative dependencies on emacs23*:
Emacs 23 is not in testing/sid anymore, and sbuild always picks
the first alternative, which made the package FTBFS (Closes: #768619).
2014-08-12 - Hideki Yamane <henrich@debian.org>
proofgeneral (4.3~pre131011-0.1) unstable; urgency=low
* Non-maintainer upload.
* New upstream release
* debian/patches
- drop fix-texinfo-5-1-bug.patch: unnecessary anymore
- drop pg-image-bug.patch: unnecessary (cause FTBFS)
2014-02-15 - Hideki Yamane <henrich@debian.org>
proofgeneral (4.3~pre130510-1.1) unstable; urgency=medium
* Non-maintainer upload.
* debian/control
- add "Build-Depends: texlive-fonts-recommended" to fix FTBFS
(Closes: #738392)
- remove unnecessary "Build-Depends: texi2html" due to transtion
(see https://wiki.debian.org/Texi2htmlTransition)
* debian/patches
- add transition_to_makeinfo.patch to use makeinfo, instead of texi2html
* also update debian/proofgeneral-doc.doc-base to deal with changes with
above
2013-05-15 - Hendrik Tews <hendrik@askra.de>
proofgeneral (4.3~pre130510-1) unstable; urgency=low
* New upstream release (Closes: #707331)
* improve watch file (thanks to Bart Martens for the uversionmangle hint)
* add new patch to install coq example and add hint in tutorial 
(Closes: #687977) 
* add new patch fix-texinfo-5-1-bug to fix a problem with texinfo 5.1
* add new patch pg-image-bug to rename ProofGeneral.jpg
* permit emacs24
* update README.Debian
* bump standards version to 3.9.4
* debhelper compat level 9
2012-12-04 - Hendrik Tews <hendrik@askra.de>
proofgeneral (4.2~pre120605-2) unstable; urgency=low
* add Breaks and Replaces dependencies for proofgeneral-doc (Closes: #694285)
* delete wrong info in README.Debian
2012-06-06 - Hendrik Tews <hendrik@askra.de>
proofgeneral (4.2~pre120605-1) unstable; urgency=low
* New upstream release (Closes: #669318)
* fix byte-compile-error-on-warn in emacsen-install, --no-site-file has
been dropped already in 4.2~pre120411-2 (Closes: #671583)
* use debian-emacs-flavor in emacsen-startup (see #662163)
* delete patch disable-proof-tree, add patch smartly-enable-prooftree
for enabling prooftree if Coq >= 8.4beta is detected
* fix package description
* add hints on Prooftree and incompatibility with manual Coq
installations to README.Debian
* new patch for using debian-pkg-add-load-path-item (see #670339), but
don't use it, because debian-pkg-add-load-path-item breaks Proof
General, see #676424

See Also

Package Description
prooftree_0.13-1build2_i386.deb proof-tree visualization for Proof General
proot_5.1.0-1.2_i386.deb emulate chroot, bind mount and binfmt_misc for non-root users
propaganda-debian_13.5.10_all.deb Propaganda background image volume for Debian
propellor_4.7.6-1_i386.deb property-based host configuration management in haskell
prosody-modules_0.0~hg20170123.3ed504b944e5+dfsg-1_all.deb Selection of community modules for Prosody
prosody_0.9.12-2_i386.deb Lightweight Jabber/XMPP server
prospector_0.12.7-1build1_all.deb comprehensive static Python code analyzer
prosper_2017.20170818-1_all.deb TeX Live: transitional dummy package
proteinortho_5.15+dfsg-1_i386.deb Detection of (Co-)orthologs in large-scale protein analysis
protobuf-c-compiler_1.2.1-2_i386.deb Protocol Buffers C compiler (protobuf-c)
protobuf-compiler-grpc_1.3.2-1_i386.deb high performance general RPC framework - protobuf plugin
protracker_2.3d.r10-1_i386.deb Amiga ProTracker v2.3D clone for modern computers
prottest_3.4.2+dfsg-2_all.deb selection of best-fit models of protein evolution
prov-tools_1.5.0-2_all.deb tools for prov
prover9-doc_0.0.200902a-2_all.deb documentation for Prover9 and associated programs
Advertisement
Advertisement