gnu: libdvdcss: Update to 1.4.3.

[jackhill/guix/guix.git] / gnu / packages / lean.scm

diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm
index e71b4c9..cc59329 100644 (file)
--- a/gnu/packages/lean.scm
+++ b/gnu/packages/lean.scm
@@ -1,5 +1,7 @@
 ;;; GNU Guix --- Functional package management for GNU
-;;; Copyright © 2019 Amin Bandali <mab@gnu.org>
+;;; Copyright © 2019 Amin Bandali <bandali@gnu.org>
+;;; Copyright © 2020 Brett Gilio <brettg@gnu.org>
+;;; Copyright © 2020 Tobias Geerinckx-Rice <me@tobias.gr>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -26,7 +28,7 @@
 (define-public lean
   (package
     (name "lean")
-    (version "3.5.0")
+    (version "3.23.0")
     (home-page "https://github.com/leanprover-community/lean")
     (source (origin
               (method git-fetch)
@@ -35,12 +37,19 @@
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1fdblq8ckrv6wqxfl4ybcs3ybfq7y096c9f5j4j75ymb14r401lr"))))
+                "09mklc1p6ms1jayg2f89hqfmhca3h5744lli936l38ypn1d00sxx"))))
     (build-system cmake-build-system)
     (inputs
      `(("gmp" ,gmp)))
     (arguments
      `(#:build-type "Release"           ; default upstream build type
+       ;; XXX: Test phases currently fail on 32-bit sytems.
+       ;; Tests for those architectures have been temporarily
+       ;; disabled, pending further investigation.
+       #:tests? ,(let ((arch (or (%current-target-system)
+                              (%current-system))))
+                   (not (or (string-prefix? "i686" arch)
+                            (string-prefix? "armhf" arch))))
        #:phases
        (modify-phases %standard-phases
          (add-after 'patch-source-shebangs 'patch-tests-shebangs
@@ -57,7 +66,7 @@
                #t)))
          (add-before 'configure 'chdir-to-src
            (lambda _ (chdir "src") #t)))))
-    (synopsis "The Lean theorem prover and programming language")
+    (synopsis "Theorem prover and programming language")
     (description
      "Lean is a theorem prover and programming language with a small trusted
 core based on dependent typed theory, aiming to bridge the gap between