gnu: coq: Update to 8.17.1.

* gnu/packages/coq.scm (coq): Update to 8.17.1 and merge with coq-core and coq-stdlib.
  [arguments] Merge with coq-core and coq-stdlib. Add pre-build phases and
  add a custom install phase. Remove unnecessary test-target.
  [source](patches): Remove.
  [native-search-paths]: Remove COQLIBPATH and COQCORELIB.
  (coq-core): Remove variable.
  (coq-stdlib): Remove variable.
  (coq-ide)[propagated-inputs]: Add zlib.
  (coq-mathcomp-bigenough)[propagated-inputs]: Remove coq-core.
  (coq-mathcomp-finmap)[inputs]: Remove coq-stdlib.
  (coq-equations): Update to 1.3-8.17.
* gnu/packages/patches/coq-fix-envvars.patch: Delete file.
* gnu/local.mk (dist_patch_DATA): Adjust accordingly.

Co-authored-by: Josselin Poiret <dev@jpoiret.xyz>
Signed-off-by: Julien Lepiller <julien@lepiller.eu>
Change-Id: I0a0d9f7a6e06dd19ce1b66051334476d85f4f195
This commit is contained in:
pukkamustard 2024-01-10 08:43:10 +01:00 committed by Julien Lepiller
parent c168dc5ad1
commit 4b941ab3d5
No known key found for this signature in database
GPG key ID: 53D457B2D636EE82
3 changed files with 32 additions and 111 deletions

View file

@ -1056,7 +1056,6 @@ dist_patch_DATA = \
%D%/packages/patches/converseen-hide-non-free-pointers.patch \ %D%/packages/patches/converseen-hide-non-free-pointers.patch \
%D%/packages/patches/cool-retro-term-wctype.patch \ %D%/packages/patches/cool-retro-term-wctype.patch \
%D%/packages/patches/coreutils-gnulib-tests.patch \ %D%/packages/patches/coreutils-gnulib-tests.patch \
%D%/packages/patches/coq-fix-envvars.patch \
%D%/packages/patches/cppcheck-disable-char-signedness-test.patch \ %D%/packages/patches/cppcheck-disable-char-signedness-test.patch \
%D%/packages/patches/cpuinfo-system-libraries.patch \ %D%/packages/patches/cpuinfo-system-libraries.patch \
%D%/packages/patches/cpulimit-with-glib-2.32.patch \ %D%/packages/patches/cpulimit-with-glib-2.32.patch \

View file

@ -31,6 +31,7 @@ (define-module (gnu packages coq)
#:use-module (gnu packages base) #:use-module (gnu packages base)
#:use-module (gnu packages bison) #:use-module (gnu packages bison)
#:use-module (gnu packages boost) #:use-module (gnu packages boost)
#:use-module (gnu packages compression)
#:use-module (gnu packages emacs) #:use-module (gnu packages emacs)
#:use-module (gnu packages flex) #:use-module (gnu packages flex)
#:use-module (gnu packages gawk) #:use-module (gnu packages gawk)
@ -51,10 +52,10 @@ (define-module (gnu packages coq)
#:use-module (guix utils) #:use-module (guix utils)
#:use-module ((srfi srfi-1) #:hide (zip))) #:use-module ((srfi srfi-1) #:hide (zip)))
(define-public coq-core (define-public coq
(package (package
(name "coq-core") (name "coq")
(version "8.16.1") (version "8.17.1")
(source (source
(origin (origin
(method git-fetch) (method git-fetch)
@ -64,28 +65,35 @@ (define-public coq-core
(file-name (git-file-name name version)) (file-name (git-file-name name version))
(sha256 (sha256
(base32 (base32
"0ljpqhh5lfsim29fcfp2xfcvm3j84pf1mb0gnpdr8vcqqw7mqwpf")) "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))))
(patches (search-patches "coq-fix-envvars.patch"))))
(native-search-paths (native-search-paths
(list (search-path-specification (list (search-path-specification
(variable "COQPATH") (variable "COQPATH")
(files (list "lib/ocaml/site-lib/coq/user-contrib" (files (list "lib/coq/user-contrib")))))
"lib/coq/user-contrib")))
(search-path-specification
(variable "COQLIBPATH")
(files (list "lib/ocaml/site-lib/coq")))
(search-path-specification
(variable "COQCORELIB")
(files (list "lib/ocaml/site-lib/coq-core"))
(separator #f))))
(build-system dune-build-system) (build-system dune-build-system)
(arguments
(list
#:package "coq-core,coq-stdlib,coq"
#:phases
#~(modify-phases %standard-phases
(add-before 'build 'configure
(lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out"))
(coqlib (string-append out "/lib/ocaml/site-lib/coq/")))
(invoke "./configure" "-prefix" out
"-libdir" coqlib))))
(add-before 'build 'make-dunestrap
(lambda _ (invoke "make" "dunestrap")))
(replace 'install
(lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out"))
(libdir (string-append out "/lib/ocaml/site-lib")))
(invoke "dune" "install" "--prefix" out
"--libdir" libdir "coq" "coq-core" "coq-stdlib")))))))
(inputs (inputs
(list gmp ocaml-zarith)) (list gmp ocaml-zarith))
(native-inputs (native-inputs
(list ocaml-ounit2 which)) (list ocaml-ounit2 which))
(arguments
`(#:package "coq-core"
#:test-target "."))
(properties '((upstream-name . "coq"))) ; also for inherited packages (properties '((upstream-name . "coq"))) ; also for inherited packages
(home-page "https://coq.inria.fr") (home-page "https://coq.inria.fr")
(synopsis "Proof assistant for higher-order logic") (synopsis "Proof assistant for higher-order logic")
@ -97,39 +105,6 @@ (define-public coq-core
;; Some of the documentation is distributed under opl1.0+. ;; Some of the documentation is distributed under opl1.0+.
(license (list license:lgpl2.1 license:opl1.0+)))) (license (list license:lgpl2.1 license:opl1.0+))))
(define-public coq-stdlib
(package
(inherit coq-core)
(name "coq-stdlib")
(arguments
`(#:package "coq-stdlib"
#:test-target "."
#:phases
(modify-phases %standard-phases
(add-before 'build 'fix-dune
(lambda _
(substitute* "user-contrib/Ltac2/dune"
(("coq-core.plugins.ltac2")
(string-join
(map (lambda (plugin) (string-append "coq-core.plugins." plugin))
'("ltac2" "number_string_notation" "tauto" "cc"
"firstorder"))
" "))))))))
(inputs
(list coq-core gmp ocaml-zarith))
(native-inputs '())))
(define-public coq
(package
(inherit coq-core)
(name "coq")
(arguments
`(#:package "coq"
#:test-target "."))
(propagated-inputs
(list coq-core coq-stdlib))
(native-inputs '())))
(define-public coq-ide-server (define-public coq-ide-server
(package (package
(inherit coq) (inherit coq)
@ -148,7 +123,7 @@ (define-public coq-ide
`(#:tests? #f `(#:tests? #f
#:package "coqide")) #:package "coqide"))
(propagated-inputs (propagated-inputs
(list coq coq-ide-server)) (list coq coq-ide-server zlib))
(inputs (inputs
(list lablgtk3 ocaml-lablgtk3-sourceview3)))) (list lablgtk3 ocaml-lablgtk3-sourceview3))))
@ -582,16 +557,16 @@ (define-public coq-autosubst
(define-public coq-equations (define-public coq-equations
(package (package
(name "coq-equations") (name "coq-equations")
(version "1.3") (version "1.3-8.17")
(source (origin (source (origin
(method git-fetch) (method git-fetch)
(uri (git-reference (uri (git-reference
(url "https://github.com/mattam82/Coq-Equations") (url "https://github.com/mattam82/Coq-Equations")
(commit (string-append "v" version "-8.16")))) (commit (string-append "v" version))))
(file-name (git-file-name name version)) (file-name (git-file-name name version))
(sha256 (sha256
(base32 (base32
"08f756vgdd1wklkarg0b93j4n5mhkqm5ixxrhyb23dcv2dwhc8yg")))) "0g68h4c1ijpphixvl9wkd7sibds38v4236dpvvh194j5ii42vnn8"))))
(build-system gnu-build-system) (build-system gnu-build-system)
(native-inputs (native-inputs
(list ocaml coq camlp5)) (list ocaml coq camlp5))
@ -743,7 +718,7 @@ (define-public coq-mathcomp-finmap
"/lib/coq/user-contrib")) "/lib/coq/user-contrib"))
#:phases (modify-phases %standard-phases #:phases (modify-phases %standard-phases
(delete 'configure)))) (delete 'configure))))
(inputs (list coq coq-stdlib coq-mathcomp which)) (inputs (list coq coq coq-mathcomp which))
(synopsis "Finite sets and finite types for coq-mathcomp") (synopsis "Finite sets and finite types for coq-mathcomp")
(description (description
"This library is an extension of coq-mathcomp which supports finite sets "This library is an extension of coq-mathcomp which supports finite sets
@ -774,7 +749,7 @@ (define-public coq-mathcomp-bigenough
;; by the packaged project in the future. ;; by the packaged project in the future.
#:tests? #f #:tests? #f
#:make-flags ,#~(list (string-append "COQBIN=" #:make-flags ,#~(list (string-append "COQBIN="
#$(this-package-input "coq-core") #$(this-package-input "coq")
"/bin/") "/bin/")
(string-append "COQMF_COQLIB=" (string-append "COQMF_COQLIB="
(assoc-ref %outputs "out") (assoc-ref %outputs "out")
@ -784,7 +759,7 @@ (define-public coq-mathcomp-bigenough
"/lib/coq/user-contrib")) "/lib/coq/user-contrib"))
#:phases (modify-phases %standard-phases #:phases (modify-phases %standard-phases
(delete 'configure)))) (delete 'configure))))
(propagated-inputs (list coq coq-core coq-mathcomp which)) (propagated-inputs (list coq coq-mathcomp which))
(home-page "https://math-comp.github.io/") (home-page "https://math-comp.github.io/")
(synopsis "Small library to do epsilon - N reasoning") (synopsis "Small library to do epsilon - N reasoning")
(description (description

View file

@ -1,53 +0,0 @@
From 0e76cda958a4d3e4bcbb96e171c26b6b3478c6c2 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Thu, 10 Feb 2022 16:44:10 +0100
Subject: [PATCH] Fix environment variable usage.
---
boot/env.ml | 26 +++++++++++++++++++-------
1 file changed, 19 insertions(+), 7 deletions(-)
diff --git a/boot/env.ml b/boot/env.ml
index e8521e7..d834a3a 100644
--- a/boot/env.ml
+++ b/boot/env.ml
@@ -32,17 +32,29 @@ let fail_msg =
let fail s = Format.eprintf "%s@\n%!" fail_msg; exit 1
+let path_to_list p =
+ let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
+ String.split_on_char sep p
+
(* This code needs to be refactored, for now it is just what used to be in envvars *)
let guess_coqlib () =
Util.getenv_else "COQLIB" (fun () ->
let prelude = "theories/Init/Prelude.vo" in
- Util.check_file_else
- ~dir:Coq_config.coqlibsuffix
- ~file:prelude
- (fun () ->
- if Sys.file_exists (Filename.concat Coq_config.coqlib prelude)
- then Coq_config.coqlib
- else fail ()))
+ let coqlibpath = Util.getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in
+ let paths = path_to_list coqlibpath in
+ let valid_paths =
+ List.filter
+ (fun dir -> (Util.check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "")
+ paths in
+ match valid_paths with
+ | [] ->
+ if Sys.file_exists (Filename.concat Coq_config.coqlib prelude)
+ then Coq_config.coqlib
+ else
+ fail "cannot guess a path for Coq libraries; please use -coqlib option \
+ or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) \
+ If you intend to use Coq without a standard library, the -boot -noinit options must be used."
+ | p::_ -> p)
(* Build layout uses coqlib = coqcorelib *)
let guess_coqcorelib lib =
--
2.34.0