From 237529c9dc8b267175a3879cf23a77487611ca91 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 12 Jan 2019 21:24:35 +0100 Subject: Rename pg-init.el to proof-general.el Close ProofGeneral/PG#385 and close ProofGeneral/PG#398 --- pg-init.el | 69 -------------------------------------------------------- proof-general.el | 69 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 69 insertions(+), 69 deletions(-) delete mode 100644 pg-init.el create mode 100644 proof-general.el diff --git a/pg-init.el b/pg-init.el deleted file mode 100644 index 0634de0b..00000000 --- a/pg-init.el +++ /dev/null @@ -1,69 +0,0 @@ -;;; pg-init.el --- PG init file for package.el and ELPA compatibility -*- lexical-binding:t; -*- - -;; This file is part of Proof General. - -;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003-2019 Free Software Foundation, Inc. -;; Portions © Copyright 2001-2017 Pierre Courtieu -;; Portions © Copyright 2010, 2016 Erik Martin-Dorel -;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews -;; Portions © Copyright 2015-2017 Clément Pit-Claudel - -;; Author: Clément Pit-Claudel -;; URL: https://proofgeneral.github.io/ -;; Package-Requires: ((emacs "24.3")) -;; Version: 4.5-git - -;; This program is free software; you can redistribute it and/or modify -;; it under the terms of the GNU General Public License as published by -;; the Free Software Foundation, either version 3 of the License, or -;; (at your option) any later version. - -;; This program is distributed in the hope that it will be useful, -;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -;; GNU General Public License for more details. - -;; You should have received a copy of the GNU General Public License -;; along with this program. If not, see . - -;;; Commentary: -;; -;; Proof General's initialization code (in generic/proof-site) is relatively -;; complex, in part because it was written before package.el existed, and in -;; part because package.el still doesn't look for autoloads in subdirectories. -;; This file is a thin, package.el-friendly wrapper around generic/proof-site, -;; suitable for execution on Emacs start-up. It serves two purposes: -;; -;; * Setting up the load path when byte-compiling PG. -;; * Loading a minimal PG setup on startup (not all of Proof General, of course; -;; mostly mode hooks and autoloads). - -;;; Code: - -;;;###autoload -(if t (require 'proof-site - (expand-file-name "generic/proof-site" - (file-name-directory - (or load-file-name buffer-file-name))))) - -(eval-when-compile - ;; FIXME: This is used during installation of the ELPA package: - ;; we presume that this file will be compiled before any of the files in - ;; sub-directories and we presume that all files are compiled within the same - ;; session, so we here add to load-path all the subdirectories so - ;; that files in (say) coq/ can (require 'coq-foo) and the compiler will find - ;; the corresponding file. - (let ((byte-compile-directories - '("generic" "lib" - "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox" - ;; FIXME: These dirs used to not be listed, but I needed to add - ;; them for the compilation to succeed for me. --Stef - "isar" "lego" "twelf" "obsolete/plastic")) - (root (file-name-directory - (or load-file-name byte-compile-current-file buffer-file-name)))) - (dolist (dir byte-compile-directories) - (add-to-list 'load-path (expand-file-name dir root))))) - -(provide 'pg-init) -;;; pg-init.el ends here diff --git a/proof-general.el b/proof-general.el new file mode 100644 index 00000000..73820f9e --- /dev/null +++ b/proof-general.el @@ -0,0 +1,69 @@ +;;; proof-general.el --- PG init file for package.el and ELPA compatibility -*- lexical-binding: t; -*- + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003-2019 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;; Author: Clément Pit-Claudel +;; URL: https://proofgeneral.github.io/ +;; Package-Requires: ((emacs "24.3")) +;; Version: 4.5-git + +;; This program is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation, either version 3 of the License, or +;; (at your option) any later version. + +;; This program is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;; You should have received a copy of the GNU General Public License +;; along with this program. If not, see . + +;;; Commentary: +;; +;; Proof General's initialization code (in generic/proof-site) is relatively +;; complex, in part because it was written before package.el existed, and in +;; part because package.el still doesn't look for autoloads in subdirectories. +;; This file is a thin, package.el-friendly wrapper around generic/proof-site, +;; suitable for execution on Emacs start-up. It serves two purposes: +;; +;; * Setting up the load path when byte-compiling PG. +;; * Loading a minimal PG setup on startup (not all of Proof General, of course; +;; mostly mode hooks and autoloads). + +;;; Code: + +;;;###autoload +(if t (require 'proof-site + (expand-file-name "generic/proof-site" + (file-name-directory + (or load-file-name buffer-file-name))))) + +(eval-when-compile + ;; FIXME: This is used during installation of the ELPA package: + ;; we presume that this file will be compiled before any of the files in + ;; sub-directories and we presume that all files are compiled within the same + ;; session, so we here add to load-path all the subdirectories so + ;; that files in (say) coq/ can (require 'coq-foo) and the compiler will find + ;; the corresponding file. + (let ((byte-compile-directories + '("generic" "lib" + "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox" + ;; FIXME: These dirs used to not be listed, but I needed to add + ;; them for the compilation to succeed for me. --Stef + "isar" "lego" "twelf" "obsolete/plastic")) + (root (file-name-directory + (or load-file-name byte-compile-current-file buffer-file-name)))) + (dolist (dir byte-compile-directories) + (add-to-list 'load-path (expand-file-name dir root))))) + +(provide 'proof-general) +;;; proof-general.el ends here -- cgit v1.2.3 From beebf0f144a04190c0f0910860f603a14f937b6b Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 12 Jan 2019 21:35:30 +0100 Subject: Fix the license notice in proof-general.el as PG master is still under GPLv2 (while PG async already switched to GPLv3+) href: https://github.com/ProofGeneral/PG/tree/fb3b75dab55b6e6befffc53e136422558be5faa0#contributing --- proof-general.el | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/proof-general.el b/proof-general.el index 73820f9e..fac8f5ac 100644 --- a/proof-general.el +++ b/proof-general.el @@ -14,10 +14,9 @@ ;; Package-Requires: ((emacs "24.3")) ;; Version: 4.5-git -;; This program is free software; you can redistribute it and/or modify -;; it under the terms of the GNU General Public License as published by -;; the Free Software Foundation, either version 3 of the License, or -;; (at your option) any later version. +;; This software is free software; you can redistribute it and/or +;; modify it under the terms of the GNU General Public License +;; version 2, as published by the Free Software Foundation. ;; This program is distributed in the hope that it will be useful, ;; but WITHOUT ANY WARRANTY; without even the implied warranty of -- cgit v1.2.3 From 97e8558810c93fd2f8eb7983d7c1ed3cfa7a038b Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 12 Jan 2019 22:02:55 +0100 Subject: Update the commentary section in proof-general.el as this text should document the whole package and will be shown at http://www.melpa.org/#/proof-general href: https://github.com/ProofGeneral/PG/issues/198#issuecomment-419741803 --- proof-general.el | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/proof-general.el b/proof-general.el index fac8f5ac..a2f8c6fa 100644 --- a/proof-general.el +++ b/proof-general.el @@ -9,7 +9,7 @@ ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews ;; Portions © Copyright 2015-2017 Clément Pit-Claudel -;; Author: Clément Pit-Claudel +;; Authors: (see the AUTHORS file distributed along the sources) ;; URL: https://proofgeneral.github.io/ ;; Package-Requires: ((emacs "24.3")) ;; Version: 4.5-git @@ -28,6 +28,21 @@ ;;; Commentary: ;; +;; 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, 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). + +;;; Code: + ;; Proof General's initialization code (in generic/proof-site) is relatively ;; complex, in part because it was written before package.el existed, and in ;; part because package.el still doesn't look for autoloads in subdirectories. @@ -38,8 +53,6 @@ ;; * Loading a minimal PG setup on startup (not all of Proof General, of course; ;; mostly mode hooks and autoloads). -;;; Code: - ;;;###autoload (if t (require 'proof-site (expand-file-name "generic/proof-site" -- cgit v1.2.3