From 2d60af4d6d486591c5a6981659d1771b7c69781a Mon Sep 17 00:00:00 2001 From: zimoun Date: Tue, 16 Nov 2021 19:51:50 +0100 Subject: gnu: Add coq-semantics. * gnu/packages/coq.scm (coq-semantics): New variable. Signed-off-by: Julien Lepiller --- gnu/packages/coq.scm | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index dccb9bea4c..322bdb126e 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -7,6 +7,7 @@ ;;; Copyright © 2020 raingloom ;;; Copyright © 2020 Robin Green ;;; Copyright © 2021 Xinglu Chen +;;; Copyright © 2021 Simon Tournier ;;; ;;; This file is part of GNU Guix. ;;; @@ -573,6 +574,56 @@ and accessibility, providing a definitional extension to the Coq kernel.") (license license:lgpl2.1))) +(define-public coq-semantics + (package + (name "coq-semantics") + (version "8.13.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/coq-community/semantics") + (commit (string-append "v" version)))) + (modules '((guix build utils))) + (snippet + '(substitute* "Makefile.coq.local" + ;; Num was part of OCaml and now external + (("-libs nums") "-use-ocamlfind -pkg num -libs num"))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i")))) + (build-system gnu-build-system) + (native-inputs + `(("coq" ,coq) + ("ocaml" ,ocaml) + ("ocamlbuild" ,ocamlbuild) + ("ocaml-findlib" ,ocaml-findlib))) + (inputs + `(("ocaml-num" ,ocaml-num))) + (arguments + `(#:tests? #f ;included in Makefile + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) + #:phases + (modify-phases %standard-phases + (delete 'configure)))) + (home-page "https://github.com/coq-community/semantics") + (synopsis "Survey of semantics styles") + (description + "This package provides a survey of programming language semantics styles, +from natural semantics through structural operational, axiomatic, and +denotational semantics, for a miniature example of an imperative programming +language. Their encoding, the proofs of equivalence of different styles, +abstract interpretation, and the proof of soundess obtained from axiomatic +semantics or abstract interpretation is done in Coq. The tools can be run +inside Coq, thus making them available for proof by reflection. Code can also +be extracted and connected to a yacc-based parser, thanks to the use of a +functor parameterized by a module type of strings. A hand-written parser is +also provided in Coq, without associated proofs.") + (license license:expat))) + (define-public coq-stdpp (package (name "coq-stdpp") -- cgit v1.2.3 From 7b93c6d77786c27171900045f62be0fce69432f7 Mon Sep 17 00:00:00 2001 From: zimoun Date: Tue, 16 Nov 2021 19:51:51 +0100 Subject: gnu: coq-mathcomp: Adjust '#:make-flags'. * gnu/packages/coq.scm (coq-mathcomp)[arguments]<#:make-flags>: Set install destination. <#:phases>: Remove replace 'install. Signed-off-by: Julien Lepiller --- gnu/packages/coq.scm | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 322bdb126e..602a2d305d 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -326,17 +326,14 @@ assistant.") ("coq" ,coq))) (arguments `(#:tests? #f ; No tests. + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (delete 'configure) (add-before 'build 'chdir - (lambda _ (chdir "mathcomp") #t)) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (invoke "make" "-f" "Makefile.coq" - (string-append "COQLIB=" (assoc-ref outputs "out") - "/lib/coq/") - "install")))))) + (lambda _ (chdir "mathcomp") #t))))) (home-page "https://math-comp.github.io/") (synopsis "Mathematical Components for Coq") (description "Mathematical Components for Coq has its origins in the formal -- cgit v1.2.3 From 5d7d64ff8567abb32defbf00038fab789353a8d5 Mon Sep 17 00:00:00 2001 From: zimoun Date: Tue, 16 Nov 2021 19:51:52 +0100 Subject: gnu: coq-autosubst: Adjust '#:make-flags'. * gnu/packages/coq.scm (coq-autosubst)[arguments]<#:make-flags>: Set install destination. <#:phases>: Remove replace 'install. Signed-off-by: Julien Lepiller --- gnu/packages/coq.scm | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 602a2d305d..fc739a0475 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -502,16 +502,12 @@ Coq proof assistant.") (build-system gnu-build-system) (arguments `(#:tests? #f + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases - (delete 'configure) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/")) - (invoke "make" - (string-append "COQLIB=" (assoc-ref outputs "out") - "/lib/coq/") - "install")))))) + (delete 'configure)))) (native-inputs `(("coq" ,coq))) (home-page "https://www.ps.uni-saarland.de/autosubst/") -- cgit v1.2.3 From 4423caece69f6142eeff562007ce53b9144de334 Mon Sep 17 00:00:00 2001 From: zimoun Date: Tue, 16 Nov 2021 19:51:53 +0100 Subject: gnu: coq-equations: Adjust '#:make-flags'. * gnu/packages/coq.scm (coq-equations)[arguments]<#:make-flags>: Set install destination. <#:phases>: Remove replace 'install. Signed-off-by: Julien Lepiller --- gnu/packages/coq.scm | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index fc739a0475..aeba0eb5da 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -547,17 +547,14 @@ uses Ltac to synthesize the substitution operation.") `(("ocaml-zarith" ,ocaml-zarith))) (arguments `(#:test-target "test-suite" + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (replace 'configure (lambda* (#:key outputs #:allow-other-keys) - (invoke "sh" "./configure.sh"))) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (invoke "make" - (string-append "COQLIB=" (assoc-ref outputs "out") - "/lib/coq/") - "install")))))) + (invoke "sh" "./configure.sh")))))) (home-page "https://mattam82.github.io/Coq-Equations/") (synopsis "Function definition plugin for Coq") (description "Equations provides a notation for writing programs -- cgit v1.2.3 From 7537ec816ffe0aaa6677c53604ac12fe9d9ca250 Mon Sep 17 00:00:00 2001 From: zimoun Date: Tue, 16 Nov 2021 19:51:54 +0100 Subject: gnu: coq-stdpp: Adjust '#:make-flags'. * gnu/packages/coq.scm (coq-stdpp)[arguments]<#:make-flags>: Set install destination. <#:phases>: Remove replace 'install. Signed-off-by: Julien Lepiller --- gnu/packages/coq.scm | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index aeba0eb5da..a0579f8869 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -633,15 +633,12 @@ also provided in Coq, without associated proofs.") `(("coq" ,coq))) (arguments `(#:tests? #f ; Tests are executed during build phase. + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases - (delete 'configure) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (invoke "make" - (string-append "COQLIB=" (assoc-ref outputs "out") - "/lib/coq/") - "install")))))) + (delete 'configure)))) (description "This project contains an extended \"Standard Library\" for Coq called coq-std++. The key features are: @itemize -- cgit v1.2.3 From 5f7fb8bd37768174981e2e5c497bd01da3675f17 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sat, 20 Nov 2021 00:35:10 +0100 Subject: gnu: coq-flocq: Update home-page. * gnu/packages/coq.scm (coq-flocq)[home-page]: Update. --- gnu/packages/coq.scm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index a0579f8869..a53c63593b 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -237,7 +237,7 @@ provers.") (replace 'install (lambda _ (invoke "./remake" "install")))))) - (home-page "https://flocq.gforge.inria.fr/") + (home-page "https://flocq.gitlabpages.inria.fr/") (synopsis "Floating-point formalization for the Coq system") (description "Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix -- cgit v1.2.3 From d326fdb7af55dcfac696954d8663d95c849b8d09 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sat, 20 Nov 2021 00:36:57 +0100 Subject: gnu: coq-gappa: Update home-page. * gnu/packages/coq.scm (coq-gappa)[home-page]: Update. --- gnu/packages/coq.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index a53c63593b..d413beab26 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -237,7 +237,7 @@ provers.") (replace 'install (lambda _ (invoke "./remake" "install")))))) - (home-page "https://flocq.gitlabpages.inria.fr/") + (home-page "https://flocq.gitlabpages.inria.fr") (synopsis "Floating-point formalization for the Coq system") (description "Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix @@ -295,7 +295,7 @@ inside Coq.") ;; (lambda _ (invoke "./remake" "check"))) (replace 'install (lambda _ (invoke "./remake" "install")))))) - (home-page "https://gappa.gforge.inria.fr/") + (home-page "https://gappa.gitlabpages.inria.fr/") (synopsis "Verify and formally prove properties on numerical programs") (description "Gappa is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point -- cgit v1.2.3 From 27c701a17bd86b8fee5196013d3d17b401476be5 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sat, 20 Nov 2021 00:37:46 +0100 Subject: gnu: coq-interval: Update home-page. * gnu/packages/coq.scm (coq-interval)[home-page]: Update. --- gnu/packages/coq.scm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index d413beab26..91290c8584 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -476,7 +476,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (lambda _ (invoke "./remake" "check"))) (replace 'install (lambda _ (invoke "./remake" "install")))))) - (home-page "http://coq-interval.gforge.inria.fr/") + (home-page "https://coqinterval.gitlabpages.inria.fr/") (synopsis "Coq tactics to simplify inequality proofs") (description "Interval provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the -- cgit v1.2.3 From 45bc66dbe9cd7aa3f5d8189f3286867594768089 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 21 Nov 2021 16:48:35 +0100 Subject: gnu: coq-flocq: Update to 3.4.2. * gnu/packages/coq.scm (coq-flocq): Update to 3.4.2. --- gnu/packages/coq.scm | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 91290c8584..15b920af69 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -191,7 +191,7 @@ provers.") (define-public coq-flocq (package (name "coq-flocq") - (version "3.3.1") + (version "3.4.2") (source (origin (method git-fetch) @@ -201,7 +201,7 @@ provers.") (file-name (git-file-name name version)) (sha256 (base32 - "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl")))) + "0j7vq7ifqcdaj2x881aha2rl51l2p72y1cn7r2xya0fjgsssfigy")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -211,16 +211,10 @@ provers.") ("coq" ,coq))) (arguments `(#:configure-flags - (list (string-append "--libdir=" (assoc-ref %outputs "out") - "/lib/coq/user-contrib/Flocq")) + (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases - (add-after 'unpack 'remove-failing-examples - (lambda _ - (substitute* "Remakefile.in" - ;; Fails on a union error. - (("Double_rounding_odd_radix.v") "")) - #t)) (add-before 'configure 'fix-remake (lambda _ (substitute* "remake.cpp" -- cgit v1.2.3 From 67fbcd437c9906f52b5311058b1c6b48e4c94d02 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 21 Nov 2021 16:53:46 +0100 Subject: gnu: coq-gappa: Update to 1.5.0. * gnu/packages/coq.scm (coq-gappa): Update to 1.5.0. --- gnu/packages/coq.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 15b920af69..c31a1227cc 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -242,7 +242,7 @@ inside Coq.") (define-public coq-gappa (package (name "coq-gappa") - (version "1.4.6") + (version "1.5.0") (source (origin (method git-fetch) @@ -252,7 +252,7 @@ inside Coq.") (file-name (git-file-name name version)) (sha256 (base32 - "0492i0ksrz6dnc1d57jzsbmdlb9fp9hrh9ib5v8j0yqxpyi0x8f4")))) + "1ivh8xm1c8191rm4riamjzya2x6ls96qax5byir1fywf9hbxr1vg")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) -- cgit v1.2.3 From 698e5c38b44dad82b90c744b387486dec98e413f Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 21 Nov 2021 17:12:18 +0100 Subject: gnu: coq-mathcomp: Update to 1.13.0. * gnu/packages/coq.scm (coq-mathcomp): Update to 1.13.0. --- gnu/packages/coq.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index c31a1227cc..e88f2e6e29 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -303,7 +303,7 @@ assistant.") (define-public coq-mathcomp (package (name "coq-mathcomp") - (version "1.12.0") + (version "1.13.0") (source (origin (method git-fetch) @@ -312,7 +312,7 @@ assistant.") (commit (string-append "mathcomp-" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "12cgrmzlcjnp9kv9zxsk34fgf0qfa35jdb23cbf13kmg8dyfi3h5")))) + (base32 "0aj8hsdzzds5w0p1858s2b6k9zssjcxa6kgpi0q1nvaml4zfpkcc")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) -- cgit v1.2.3 From 5bcf0101b295a2d5e3f227b2f122cdff45294e58 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 21 Nov 2021 17:32:02 +0100 Subject: gnu: coq-coquelicot: Update to 3.2.0. * gnu/packages/coq.scm (coq-coquelicot): Update to 3.2.0. --- gnu/packages/coq.scm | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index e88f2e6e29..64ada8cace 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -342,7 +342,7 @@ part of the distribution.") (define-public coq-coquelicot (package (name "coq-coquelicot") - (version "3.1.0") + (version "3.2.0") (source (origin (method git-fetch) @@ -352,7 +352,7 @@ part of the distribution.") (file-name (git-file-name name version)) (sha256 (base32 - "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm")))) + "146s5y2xsc7wb43m1pq1n4p14hw99gqbzx0ic3a4naxq16v7cv4w")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -364,8 +364,8 @@ part of the distribution.") `(("mathcomp" ,coq-mathcomp))) (arguments `(#:configure-flags - (list (string-append "--libdir=" (assoc-ref %outputs "out") - "/lib/coq/user-contrib/Coquelicot")) + (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (add-before 'configure 'fix-remake -- cgit v1.2.3 From 07fc7046d2ca8c8a7574408c2e3ce9c1e1bb5ff6 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 21 Nov 2021 17:40:58 +0100 Subject: gnu: coq-interval: Update to 4.3.1. * gnu/packages/coq.scm (coq-interval): Update to 4.3.1. --- gnu/packages/coq.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 64ada8cace..5cfe0b1cf3 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -429,7 +429,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (define-public coq-interval (package (name "coq-interval") - (version "4.3.0") + (version "4.3.1") (source (origin (method git-fetch) @@ -439,7 +439,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (file-name (git-file-name name version)) (sha256 (base32 - "1jqvd17czhliscf40idhnxgrha620039ilrdyfahn71dg2jmzqnm")))) + "0sr9psildc0sda07r2r47rfgyry49yklk38bg04yyvry5j5pryb6")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) -- cgit v1.2.3 From 63d8c7a82f54a338b0ffb1d1b93faa1d44303bf9 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 21 Nov 2021 17:50:10 +0100 Subject: gnu: coq-stdpp: Update to 1.6.0. * gnu/packages/coq.scm (coq-stdpp): Update to 1.6.0. --- gnu/packages/coq.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 5cfe0b1cf3..1665afc5aa 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -611,7 +611,7 @@ also provided in Coq, without associated proofs.") (define-public coq-stdpp (package (name "coq-stdpp") - (version "1.5.0") + (version "1.6.0") (synopsis "Alternative Coq standard library std++") (source (origin (method git-fetch) @@ -621,7 +621,7 @@ also provided in Coq, without associated proofs.") (file-name (git-file-name name version)) (sha256 (base32 - "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf")))) + "1l1w6srzydjg0h3f4krrfgvz455h56shyy2lbcnwdbzjkahibl7v")))) (build-system gnu-build-system) (inputs `(("coq" ,coq))) -- cgit v1.2.3 From cb296dfa2e2938d18ae0ee347bed0cc94bc79cf8 Mon Sep 17 00:00:00 2001 From: zimoun Date: Wed, 10 Nov 2021 20:37:48 +0100 Subject: gnu: proof-general: Adjust autoloads for Emacs. Fixes . * gnu/packages/coq.scm (proof-general)[native-inputs]: Remove 'which'. [inputs]: Remove 'coq' and 'emacs'. [arguments]<#:make-flags>: Adjust to find 'emacs'. Set 'ELISP' and 'DEST_LISP'. <#:modules, #:imported-modules>: Remove. <#:phases>: Remove call to 'which' in Makefile. Add copy file allowing Emacs autoloads. Clean unnecessary code. Signed-off-by: Nicolas Goaziou --- gnu/packages/coq.scm | 95 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 55 insertions(+), 40 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 1665afc5aa..a27ec53ecb 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -136,50 +136,65 @@ It is developed using Objective Caml and Camlp5.") "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa")))) (build-system gnu-build-system) (native-inputs - `(("which" ,which) - ("emacs" ,emacs-minimal) + `(("emacs" ,emacs-minimal) ("texinfo" ,texinfo))) (inputs - `(("host-emacs" ,emacs) - ("perl" ,perl) - ("coq" ,coq))) + `(("perl" ,perl))) (arguments - `(#:tests? #f ; no check target - #:make-flags (list (string-append "PREFIX=" %output) - (string-append "DEST_PREFIX=" %output) - (string-append "ELISP_START=" %output - "/share/emacs/site-lisp/ProofGeneral")) - #: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)")))) - (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"))) + (let ((base-directory "/share/emacs/site-lisp/ProofGeneral")) + `(#:tests? #f ; no check target + #:make-flags (list (string-append "PREFIX=" %output) + (string-append "EMACS=" (assoc-ref %build-inputs "emacs") + "/bin/emacs") + (string-append "DEST_PREFIX=" %output) + (string-append "ELISP=" %output ,base-directory) + (string-append "DEST_ELISP=" %output ,base-directory) + (string-append "ELISP_START=" %output ,base-directory)) + #: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)")))) + (add-after 'unpack 'patch-hardcoded-paths + (lambda _ + (substitute* "Makefile" + (("/sbin/install-info") "install-info")))) + (add-after 'unpack 'remove-which + (lambda _ + (substitute* "Makefile" + (("`which perl`") "perl") + (("`which bash`") "bash")))) + (add-after 'unpack 'clean + (lambda _ + ;; Delete the pre-compiled elc files for Emacs 23. + (invoke "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" - (("/sbin/install-info") "install-info"))))) - (add-after 'unpack 'clean - (lambda _ - ;; Delete the pre-compiled elc files for Emacs 23. - (invoke "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") "")) - (apply invoke "make" "install-doc" make-flags)))))) + ((" [^ ]*\\.pdf") "")) + (apply invoke "make" "install-doc" make-flags))) + (add-after 'install 'allow-subfolders-autoloads + ;; Autoload cookies are present in sub-directories. A friendly + ;; wrapper proof-general.el around generic/proof-site.el is + ;; provided 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). + ;; + ;; The renaming to proof-general-autoloads.el is Guix + ;; specific. + (lambda* (#:key outputs #:allow-other-keys) + (let ((out (assoc-ref outputs "out"))) + (copy-file "proof-general.el" + (string-append out ,base-directory + "/proof-general-autoloads.el"))))))))) (home-page "https://proofgeneral.github.io/") (synopsis "Generic front-end for proof assistants based on Emacs") (description -- cgit v1.2.3