From mboxrd@z Thu Jan 1 00:00:00 1970 From: Mark H Weaver Subject: [PATCH] gnu: Add proof-general Date: Mon, 08 Jun 2015 05:18:40 -0400 Message-ID: <87r3pm1rtb.fsf@netris.org> Mime-Version: 1.0 Content-Type: text/x-patch Return-path: Received: from eggs.gnu.org ([2001:4830:134:3::10]:33174) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Z1tCv-0004p3-6f for guix-devel@gnu.org; Mon, 08 Jun 2015 05:19:03 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1Z1tCj-0004Z5-Mg for guix-devel@gnu.org; Mon, 08 Jun 2015 05:19:01 -0400 Received: from world.peace.net ([50.252.239.5]:33379) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Z1tCj-0004Yo-Ir for guix-devel@gnu.org; Mon, 08 Jun 2015 05:18:49 -0400 Content-Disposition: inline; filename=0001-gnu-Add-proof-general.patch Content-Description: [PATCH] gnu: Add proof-general List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org Sender: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org To: guix-devel@gnu.org >From e9d66801024e66c39b8ee0d84a10ddc4e6b7a18b Mon Sep 17 00:00:00 2001 From: Mark H Weaver Date: Mon, 8 Jun 2015 05:05:23 -0400 Subject: [PATCH] gnu: Add proof-general. * gnu/packages/ocaml.scm (proof-general): New variable. --- gnu/packages/ocaml.scm | 81 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 81 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 5a86b79..5baf24c 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -24,6 +24,9 @@ #:use-module (guix utils) #:use-module (guix build-system gnu) #:use-module (gnu packages) + #:use-module (gnu packages base) + #:use-module (gnu packages emacs) + #:use-module (gnu packages texinfo) #:use-module (gnu packages pkg-config) #:use-module (gnu packages compression) #:use-module (gnu packages commencement) @@ -304,3 +307,81 @@ It is developed using Objective Caml and Camlp5.") ;; The code is distributed under lgpl2.1. ;; Some of the documentation is distributed under opl1.0+. (license (list lgpl2.1 opl1.0+)))) + +(define-public proof-general + (package + (name "proof-general") + (version "4.2") + (source (origin + (method url-fetch) + (uri (string-append + "http://proofgeneral.inf.ed.ac.uk/releases/" + "ProofGeneral-" version ".tgz")) + (sha256 + (base32 + "09qb0myq66fw17v4ziz401ilsb5xlxz1nl2wsp69d0vrfy0bcrrm")))) + (build-system gnu-build-system) + (native-inputs + `(("which" ,which) + ("emacs" ,emacs-no-x) + ("texinfo" ,texinfo))) + (inputs + `(("host-emacs" ,emacs) + ("perl" ,perl) + ("coq" ,coq))) + (arguments + `(#:tests? #f ; no check target + #:make-flags (list (string-append "PREFIX=" %output) + (string-append "DEST_PREFIX=" %output)) + #:modules ((guix build gnu-build-system) + (guix build utils) + (guix build emacs-utils)) + #:imported-modules (,@%gnu-build-system-modules + (guix build emacs-utils)) + #:phases + (modify-phases %standard-phases + (delete 'configure) + (add-after 'unpack 'disable-byte-compile-error-on-warn + (lambda _ + (substitute* "Makefile" + (("\\(setq byte-compile-error-on-warn t\\)") + "(setq byte-compile-error-on-warn nil)")) + #t)) + (add-after 'unpack 'patch-hardcoded-paths + (lambda* (#:key inputs outputs #:allow-other-keys) + (let ((out (assoc-ref outputs "out")) + (coq (assoc-ref inputs "coq")) + (emacs (assoc-ref inputs "host-emacs"))) + (define (coq-prog name) + (string-append coq "/bin/" name)) + (emacs-substitute-variables "coq/coq.el" + ("coq-prog-name" (coq-prog "coqtop")) + ("coq-compiler" (coq-prog "coqc")) + ("coq-dependency-analyzer" (coq-prog "coqdep"))) + (substitute* "Makefile" + (("/sbin/install-info") "install-info")) + (substitute* "bin/proofgeneral" + (("^PGHOMEDEFAULT=.*" all) + (string-append all + "PGHOME=$PGHOMEDEFAULT\n" + "EMACS=" emacs "/bin/emacs"))) + #t))) + (add-after 'unpack 'clean + (lambda _ + ;; Delete the pre-compiled elc files for Emacs 23. + (zero? (system* "make" "clean")))) + (add-after 'install 'install-doc + (lambda* (#:key make-flags #:allow-other-keys) + ;; XXX FIXME avoid building/installing pdf files, + ;; due to unresolved errors building them. + (substitute* "Makefile" + ((" [^ ]*\\.pdf") "")) + (zero? (apply system* "make" "install-doc" + make-flags))))))) + (home-page "http://proofgeneral.inf.ed.ac.uk/") + (description "Generic front-end for proof assistants based on Emacs") + (synopsis + "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.") + (license gpl2+))) -- 2.2.1