(address . guix-patches@gnu.org)
87tv5l9d5e.fsf@gnu.org
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].
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
Toggle diff (93 lines)
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
--
Amin Bandali
Free Software Activist | GNU Maintainer & Webmaster
GPG: BE62 7373 8E61 6D6D 1B3A 08E8 A21A 0202 4881 6103
-----BEGIN PGP SIGNATURE-----
iQJEBAEBCAAuFiEEObM8jZRIDS3cwqSYi0Sgzce5VvIFAl4G9i0QHGJhbmRhbGlA
Z251Lm9yZwAKCRCLRKDNx7lW8kSdD/9DY1kGIk6L9i/7wGThY24CX1DFc37P4Wnm
3Vg6WIr2qW2v9rjGdLpmvWS2atJ32GcTiP2zs8q3guZM5ZQoN6TJmtbULKqkROFj
8HP64p1r7xl2lmwyIwdVbrBfvNpExahKF0Rm/RibCx5ih2IdSF4RteX4Bo3Ks02V
BFQFfPlucbVjmDT7Mmd+Cf3mDcpSf1EdGJI2IoB4ZO5NUS2hcxFaDbDpTScKZ4kn
Ekzo0F1/HV0towR3xPAFpXI2rcoj1hb/VQvMoQZIo+skPt78LVDAM5qGPb478Oio
x1ED8oifRCEdHxduFuQSeT/kokVCF9HRkRFMdRskjifV2T1CGYw51R+u/FBu5u27
VAWaarQwQ+KutdRVTB5TpItogM0Pm7KXd/jurEhAiFY5rm96InVcDEuVq7Or4WPu
eMG8WdLi9YQcP7FcRg/a9w+zfXe5gYJ9PnqHdJ9JL09dvSfWg9LMUfYf+HrUb62r
HIRU+/CI2z2n9PCzdZMlCfzxhm/gprALaTnZa41THtxgM/uH4WqlNDcaBmfvlveU
lk6J/kxSDqsgPYBR9/BwQFk2NJ0MW4ByO2NmyKYFiUENVuSVk/EVS1IbakoSYCns
hfrvYcKhKqBUho5fnap4P7P9ItVFUnVK2Le6GxAkiAo0Ve6BdmjuxbLVfdVoPZ14
whpbyG5MLQ==
=tsr2
-----END PGP SIGNATURE-----