From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:46708) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1il5bx-0006wL-8c for guix-patches@gnu.org; Sat, 28 Dec 2019 01:30:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1il5bv-0002Xm-0r for guix-patches@gnu.org; Sat, 28 Dec 2019 01:30:05 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:51954) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1il5bu-0002XK-TF for guix-patches@gnu.org; Sat, 28 Dec 2019 01:30:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1il5bu-0002qG-M0 for guix-patches@gnu.org; Sat, 28 Dec 2019 01:30:02 -0500 Subject: [bug#38770] [PATCH] gnu: Add lean. Resent-Message-ID: Received: from eggs.gnu.org ([2001:470:142:3::10]:40845) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1il5az-0006tG-TM for guix-patches@gnu.org; Sat, 28 Dec 2019 01:29:09 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:58387) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1il5az-0001ec-MG for guix-patches@gnu.org; Sat, 28 Dec 2019 01:29:05 -0500 Received: from [2607:fea8:3b80:1ea:24cc:f790:26ad:3307] (port=60144 helo=localhost) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1il5ax-00060N-CH for guix-patches@gnu.org; Sat, 28 Dec 2019 01:29:04 -0500 From: Amin Bandali Date: Sat, 28 Dec 2019 01:29:01 -0500 Message-ID: <87tv5l9d5e.fsf@gnu.org> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="==-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: 38770@debbugs.gnu.org --==-=-= Content-Type: multipart/mixed; boundary="=-=-=" --=-=-= Content-Type: text/plain 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 --=-=-= Content-Type: text/x-diff; charset=utf-8 Content-Disposition: inline; filename=0001-gnu-Add-lean.patch Content-Transfer-Encoding: quoted-printable From=20b48eb1c6d876ec16df098d2373c30b43fb07aef7 Mon Sep 17 00:00:00 2001 From: Amin Bandali 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. =2D-- 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 =2D-- a/gnu/local.mk +++ b/gnu/local.mk @@ -25,6 +25,7 @@ # Copyright =C2=A9 2019 Jonathan Brielmaier # Copyright =C2=A9 2019 Evan Straw # Copyright =C2=A9 2019 Brett Gilio +# Copyright =C2=A9 2019 Amin Bandali # # This file is part of GNU Guix. # @@ -289,6 +290,7 @@ GNU_SYSTEM_MODULES =3D \ %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 =2D-- /dev/null +++ b/gnu/packages/lean.scm @@ -0,0 +1,65 @@ +;;; GNU Guix --- Functional package management for GNU +;;; Copyright =C2=A9 2019 Amin Bandali +;;; +;;; 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 . + +(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 trust= ed +core based on dependent typed theory, aiming to bridge the gap between +interactive and automated theorem proving.") + (license license:asl2.0))) =2D-=20 2.23.0 --=-=-= Content-Type: text/plain Content-Transfer-Encoding: quoted-printable =2D-=20 Amin Bandali Free Software Activist | GNU Maintainer & Webmaster GPG: BE62 7373 8E61 6D6D 1B3A 08E8 A21A 0202 4881 6103 https://bandali.eu.org --=-=-=-- --==-=-= Content-Type: application/pgp-signature; name="signature.asc" -----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----- --==-=-=--