GNU bug report logs -
#76150
[PATCH 00/16] More patches towards SageMath.
Previous Next
Reported by: Vinicius Monego <monego <at> posteo.net>
Date: Sun, 9 Feb 2025 01:51:01 UTC
Severity: normal
Tags: patch
Done: Andreas Enge <andreas <at> enge.fr>
Bug is archived. No further changes may be made.
Full log
Message #53 received at 76150 <at> debbugs.gnu.org (full text, mbox):
* gnu/packages/maths.scm (glucose): New variable.
Change-Id: I8e9031db55aa98ddde82ea676d3287656f7c4288
---
Is it OK to use -DCMAKE_BUILD_RPATH here? I don't see anyone doing it this way, it usually has a dedicated phase but it's more verbose that way.
gnu/packages/maths.scm | 39 +++++++++++++++++++++++++++++++++++++++
1 file changed, 39 insertions(+)
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index cd0a0828e1..1856a68d10 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -2899,6 +2899,45 @@ (define-public libfixmath
fixed point (16.16) format.")
(license license:expat))))
+(define-public glucose
+ (package
+ (name "glucose")
+ (version "4.2.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/audemard/glucose")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0zrn4hnkf8k95dc3s3acydl1bqkr8a0axw56g7n562lx7zj7sd62"))))
+ (build-system cmake-build-system)
+ (arguments
+ (list
+ #:tests? #f ; there are no tests
+ #:configure-flags
+ #~(list "-DBUILD_SHARED_LIBS=ON"
+ (string-append "-DCMAKE_BUILD_RPATH=" #$output "/lib"))
+ #:phases #~(modify-phases %standard-phases
+ (replace 'install
+ (lambda _
+ (for-each
+ (lambda (bin)
+ (install-file bin (string-append #$output "/bin")))
+ '("glucose-simp" "glucose-syrup"))
+ (for-each
+ (lambda (lib)
+ (install-file lib (string-append #$output "/lib")))
+ '("libglucose.so" "libglucosep.so")))))))
+ (inputs (list zlib))
+ (home-page "https://www.labri.fr/perso/lsimon/research/glucose/")
+ (synopsis "SAT Solver")
+ (description "Glucose is a SAT solver based on a scoring scheme introduced
+in 2009 for the clause learning mechanism of so called “Modern” SAT solvers.
+It is designed to be parallel.")
+ (license license:expat)))
+
(define-public libflame
;; The latest release (5.2.0) dates back to 2019. Use a newer one, which
;; among other things provides extra LAPACK symbols, such as 'dgemlq_'
--
2.48.1
This bug report was last modified 101 days ago.
Previous Next
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.