gnu/packages/lean.scm

   1 ;;; GNU Guix --- Functional package management for GNU
   2 ;;; Copyright © 2019 Amin Bandali <bandali@gnu.org>
   3 ;;; Copyright © 2020 Brett Gilio <brettg@gnu.org>
   4 ;;;
   5 ;;; This file is part of GNU Guix.
   6 ;;;
   7 ;;; GNU Guix is free software; you can redistribute it and/or modify it
   8 ;;; under the terms of the GNU General Public License as published by
   9 ;;; the Free Software Foundation; either version 3 of the License, or (at
  10 ;;; your option) any later version.
  11 ;;;
  12 ;;; GNU Guix is distributed in the hope that it will be useful, but
  13 ;;; WITHOUT ANY WARRANTY; without even the implied warranty of
  14 ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15 ;;; GNU General Public License for more details.
  16 ;;;
  17 ;;; You should have received a copy of the GNU General Public License
  18 ;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
  19
  20 (define-module (gnu packages lean)
  21   #:use-module (gnu packages multiprecision)
  22   #:use-module (guix build-system cmake)
  23   #:use-module ((guix licenses) #:prefix license:)
  24   #:use-module (guix packages)
  25   #:use-module (guix git-download))
  26
  27 (define-public lean
  28   (package
  29     (name "lean")
  30     (version "3.17.1")
  31     (home-page "https://github.com/leanprover-community/lean")
  32     (source (origin
  33               (method git-fetch)
  34               (uri (git-reference (url home-page)
  35                                   (commit (string-append "v" version))))
  36               (file-name (git-file-name name version))
  37               (sha256
  38                (base32
  39                 "15yfryg98x9lvy00v1w5kg4hp921mpvlxx1ic3m08k1ls6p1gkj4"))))
  40     (build-system cmake-build-system)
  41     (inputs
  42      `(("gmp" ,gmp)))
  43     (arguments
  44      `(#:build-type "Release"           ; default upstream build type
  45        ;; XXX: Test phases currently fail on 32-bit sytems.
  46        ;; Tests for those architectures have been temporarily
  47        ;; disabled, pending further investigation.
  48        #:tests? ,(let ((arch (or (%current-target-system)
  49                               (%current-system))))
  50                    (not (or (string-prefix? "i686" arch)
  51                             (string-prefix? "armhf" arch))))
  52        #:phases
  53        (modify-phases %standard-phases
  54          (add-after 'patch-source-shebangs 'patch-tests-shebangs
  55            (lambda _
  56              (let ((sh (which "sh"))
  57                    (bash (which "bash")))
  58                (substitute* (find-files "tests/lean" "\\.sh$")
  59                  (("#![[:blank:]]?/bin/sh")
  60                   (string-append "#!" sh))
  61                  (("#![[:blank:]]?/bin/bash")
  62                   (string-append "#!" bash))
  63                  (("#![[:blank:]]?usr/bin/env bash")
  64                   (string-append "#!" bash)))
  65                #t)))
  66          (add-before 'configure 'chdir-to-src
  67            (lambda _ (chdir "src") #t)))))
  68     (synopsis "The Lean theorem prover and programming language")
  69     (description
  70      "Lean is a theorem prover and programming language with a small trusted
  71 core based on dependent typed theory, aiming to bridge the gap between
  72 interactive and automated theorem proving.")
  73     (license license:asl2.0)))