* [PATCH] gnu: Add proof-general
@ 2015-06-08 9:18 Mark H Weaver
2015-06-08 19:20 ` Ludovic Courtès
0 siblings, 1 reply; 2+ messages in thread
From: Mark H Weaver @ 2015-06-08 9:18 UTC (permalink / raw)
To: guix-devel
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: [PATCH] gnu: Add proof-general --]
[-- Type: text/x-patch, Size: 4744 bytes --]
From e9d66801024e66c39b8ee0d84a10ddc4e6b7a18b Mon Sep 17 00:00:00 2001
From: Mark H Weaver <mhw@netris.org>
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
^ permalink raw reply related [flat|nested] 2+ messages in thread
* Re: [PATCH] gnu: Add proof-general
2015-06-08 9:18 [PATCH] gnu: Add proof-general Mark H Weaver
@ 2015-06-08 19:20 ` Ludovic Courtès
0 siblings, 0 replies; 2+ messages in thread
From: Ludovic Courtès @ 2015-06-08 19:20 UTC (permalink / raw)
To: Mark H Weaver; +Cc: guix-devel
Mark H Weaver <mhw@netris.org> skribis:
> From e9d66801024e66c39b8ee0d84a10ddc4e6b7a18b Mon Sep 17 00:00:00 2001
> From: Mark H Weaver <mhw@netris.org>
> Date: Mon, 8 Jun 2015 05:05:23 -0400
> Subject: [PATCH] gnu: Add proof-general.
>
> * gnu/packages/ocaml.scm (proof-general): New variable.
Sure, thank you!
Ludo’.
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2015-06-08 19:20 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2015-06-08 9:18 [PATCH] gnu: Add proof-general Mark H Weaver
2015-06-08 19:20 ` Ludovic Courtès
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.