[bug#38770] [PATCH] gnu: Add lean.

[Amin Bandali <bandali@gnu.org>]

[-- Attachment #1.1: Type: text/plain, Size: 502 bytes --]

This patch adds v3.5.0 of the community fork of the Lean Prover.  The
reason for adding a new (gnu packages lean) module is having a dedicated
place for all Lean-related packages, as I will be working on packaging
various Lean libraries and projects next.

This patch is the first of hopefully many to come, motivated by the
recent proposal for The Formal Methods in GNU Guix Working Group
submitted to guix-devel earlier this month [0].

[0]: https://lists.gnu.org/r/guix-devel/2019-12/msg00177.html


[-- Attachment #1.2: 0001-gnu-Add-lean.patch --]
[-- Type: text/x-diff, Size: 4124 bytes --]

From b48eb1c6d876ec16df098d2373c30b43fb07aef7 Mon Sep 17 00:00:00 2001
From: Amin Bandali <bandali@gnu.org>
Date: Sat, 28 Dec 2019 00:41:49 -0500
Subject: [PATCH] gnu: Add lean.

* gnu/local.mk (GNU_SYSTEM_MODULES): Add lean.scm.
* gnu/packages/lean.scm: New file.
---
 gnu/local.mk          |  2 ++
 gnu/packages/lean.scm | 65 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 gnu/packages/lean.scm

diff --git a/gnu/local.mk b/gnu/local.mk
index 61dfbb9d5b..98ba88b193 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -25,6 +25,7 @@
 # Copyright © 2019 Jonathan Brielmaier <jonathan.brielmaier@web.de>
 # Copyright © 2019 Evan Straw <evan.straw99@gmail.com>
 # Copyright © 2019 Brett Gilio <brettg@gnu.org>
+# Copyright © 2019 Amin Bandali <bandali@gnu.org>
 #
 # This file is part of GNU Guix.
 #
@@ -289,6 +290,7 @@ GNU_SYSTEM_MODULES =				\
   %D%/packages/key-mon.scm			\
   %D%/packages/kodi.scm				\
   %D%/packages/language.scm			\
+  %D%/packages/lean.scm				\
   %D%/packages/lego.scm				\
   %D%/packages/less.scm				\
   %D%/packages/lesstif.scm			\
diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm
new file mode 100644
index 0000000000..235113d475
--- /dev/null
+++ b/gnu/packages/lean.scm
@@ -0,0 +1,65 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2019 Amin Bandali <bandali@gnu.org>
+;;;
+;;; 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.5.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
+                "1fdblq8ckrv6wqxfl4ybcs3ybfq7y096c9f5j4j75ymb14r401lr"))))
+    (build-system cmake-build-system)
+    (inputs
+     `(("gmp" ,gmp)))
+    (arguments
+     `(#:build-type "Release"           ; default upstream build type
+       #: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 "The Lean 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)))
-- 
2.23.0


[-- Attachment #1.3: Type: text/plain, Size: 155 bytes --]


-- 
Amin Bandali
Free Software Activist | GNU Maintainer & Webmaster
GPG: BE62 7373 8E61 6D6D 1B3A  08E8 A21A 0202 4881 6103
https://bandali.eu.org

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 857 bytes --]