[bug#73237] [PATCH] gnu: Add coq-ceres.

[Antero Mejr]

* gnu/packages/coq.scm (coq-ceres): New variable.

Change-Id: I366aa3ad38a25bbcbaa70874241a22fb45d41938
---
 gnu/packages/coq.scm | 54 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 31d1e8d51d..6417b3ea48 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -777,3 +777,57 @@ (define-public coq-mathcomp-bigenough
 purposes as @code{bigenough} will be subsumed by the near tactics.  The
 formalization is based on the Mathematical Components library.")
     (license license:cecill-b)))
+
+(define-public coq-ceres
+  (package
+    (name "coq-ceres")
+    (version "0.4.1")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/Lysxia/coq-ceres";)
+                    (commit version)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "080nldsxmrxdan6gd0dvdgswn3gkwpy5hdqwra6wlmh8zzrs9z7n"))))
+    (build-system gnu-build-system)
+    (arguments
+     (list #:test-target "test"
+           #:make-flags #~(list "-f" "Makefile.coq"
+                                (string-append "COQLIBINSTALL=" #$output
+                                               "/lib/coq/user-contrib")
+                                "NO_TEST=1"
+                                "COQTOP=coqtop")
+           #:phases #~(modify-phases %standard-phases
+                        ;; Need to generate Makefile.coq
+                        (replace 'configure
+                          (lambda _
+                            (invoke "coq_makefile" "-f" "_CoqProject.classic"
+                                    "-o" "Makefile.coq")))
+                        (add-after 'build 'build-doc
+                          (lambda* (#:key make-flags #:allow-other-keys)
+                            (apply invoke "make" "html" make-flags)))
+                        (replace 'check
+                          (lambda* (#:key tests? test-target parallel-build?
+                                    make-flags #:allow-other-keys)
+                            (when tests?
+                              (apply invoke "make"
+                                     "-j" (number->string
+                                           (if parallel-build?
+                                               (parallel-job-count)
+                                               1))
+                                     test-target make-flags))))
+                        (add-after 'install 'install-doc
+                          (lambda _
+                            (let ((doc (string-append #$output
+                                                      "/share/doc/ceres")))
+                              (mkdir-p doc)
+                              (copy-recursively "html" doc)))))))
+    (propagated-inputs (list coq))
+    (home-page "https://gitlab.mpi-sws.org/iris/actris";)
+    (synopsis "Coq library for serialization to S-expressions")
+    (description
+     "This package provides a Coq library that allows for serialization and
+deserialization of S-expression data.")
+    (license license:bsd-3)))

base-commit: 0e0d9bc91f20ac6dda439ab09330f0163eb9bf42
-- 
2.46.0