;;; GNU Guix --- Functional package management for GNU
;;; 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.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (gnu packages lean)
  #:use-module (gnu packages multiprecision)
  #:use-module (guix build-system cmake)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (guix packages)
  #:use-module (guix git-download))

(define-public lean
  (package
    (name "lean")
    (version "3.23.0")
    (home-page "https://github.com/leanprover-community/lean")
    (source (origin
              (method git-fetch)
              (uri (git-reference (url home-page)
                                  (commit (string-append "v" version))))
              (file-name (git-file-name name version))
              (sha256
               (base32
                "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
           (lambda _
             (let ((sh (which "sh"))
                   (bash (which "bash")))
               (substitute* (find-files "tests/lean" "\\.sh$")
                 (("#![[:blank:]]?/bin/sh")
                  (string-append "#!" sh))
                 (("#![[:blank:]]?/bin/bash")
                  (string-append "#!" bash))
                 (("#![[:blank:]]?usr/bin/env bash")
                  (string-append "#!" bash)))
               #t)))
         (add-before 'configure 'chdir-to-src
           (lambda _ (chdir "src") #t)))))
    (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
interactive and automated theorem proving.")
    (license license:asl2.0)))
nu: node: Use more unbundled dependencies.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2018-03-12 18:04:05 +0100'>2018-03-12</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=f06e391338346cae54d23071f49e572b4b6e5bb3'>gnu: node: Update to 9.8.0.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2018-02-02 17:21:06 +0100'>2018-02-02</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=b0881e0b55bf15d8111625607eb92968b65979ff'>gnu: node: Update to 9.4.0.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2017-12-25 00:15:18 +0100'>2017-12-25</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=80f642acd48831b3459c99b53c23bbab462ed0e4'>gnu: node: Update to 9.3.0.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2017-11-28 10:04:26 +0100'>2017-11-28</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=797d238789f7635bdd55aae103db1a7c4ff33798'>gnu: node: Update to 8.9.1.</a><span class='msg-avail'>...</span></td><td>Mike Gerwitz</td></tr>
<tr><td><span title='2017-10-26 12:57:43 +0200'>2017-10-26</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=bc709e03770dbe97b5e88bd975dd160dc94a5d56'>gnu: node: Update to 8.7.0.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2017-09-02 22:59:18 +0200'>2017-09-02</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=448339709d85b77e89651a2f4facf57e31c79b4a'>gnu: node: Update to 8.4.0.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2017-07-18 17:49:02 +0200'>2017-07-18</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=45c18f8529ed25729e9cbdfeeda4aed3c965180d'>gnu: node: Add search path specification for 'NODE_PATH'.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2017-06-29 15:21:18 +0200'>2017-06-29</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=aafcfffd93250a2d92f34121c82b54c32797ef35'>gnu: node: Update to 8.1.2.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2017-05-23 18:27:35 +0200'>2017-05-23</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=ea584538ac8dc3ad7877b82a67fc3619f105ad70'>gnu: node: Use unbundled dependencies.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2017-05-23 17:55:59 +0200'>2017-05-23</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=1fdb883082385ac8c9200b831630bea069f2945d'>gnu: node: Update to 7.10.0.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2017-04-17 16:59:17 +0200'>2017-04-17</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=e5f0563d5d2cee21cd05b681e940af920f7ef979'>gnu: node: Actually set timeout to 1 h.</a><span class='msg-avail'>...</span></td><td>Danny Milosavljevic</td></tr>
<tr><td><span title='2017-04-17 14:55:16 +0200'>2017-04-17</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=3759deaba1413270e623be7b56b7a4b3856fb6e8'>gnu: node: Update to 7.8.0.</a><span class='msg-avail'>...</span></td><td>Jelle Licht</td></tr>
<tr><td><span title='2017-01-23 17:23:03 -0500'>2017-01-23</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=f2ea722ae731d6094948d58b8287213d056a178a'>gnu: node: Don't replace 'sh' reference with 'bash'.</a><span class='msg-avail'>...</span></td><td>Leo Famulari</td></tr>
<tr><td><span title='2016-10-17 11:55:49 +0200'>2016-10-17</span></td><td><a href='/guix/commit/gnu/packages/node.scm?id=dd04f56a2b25f6d32891bccd22a1315504257718'>gnu: node: Update to 6.8.0.</a><span class='msg-avail'>...</span></td><td>Al McElrath</td></tr>