From patchwork Sat Dec 28 06:29:01 2019 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Amin Bandali X-Patchwork-Id: 19460 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 6C7D71795E; Sat, 28 Dec 2019 06:30:22 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id 2F46417929 for ; Sat, 28 Dec 2019 06:30:12 +0000 (GMT) Received: from localhost ([::1]:41376 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1il5c3-0006wR-Hu for patchwork@mira.cbaines.net; Sat, 28 Dec 2019 01:30:11 -0500 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 X-Loop: help-debbugs@gnu.org Subject: [bug#38770] [PATCH] gnu: Add lean. Resent-From: Amin Bandali Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 28 Dec 2019 06:30:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 38770 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 38770@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.157751455310819 (code B ref -1); Sat, 28 Dec 2019 06:30:02 +0000 Received: (at submit) by debbugs.gnu.org; 28 Dec 2019 06:29:13 +0000 Received: from localhost ([127.0.0.1]:57927 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1il5b6-0002oP-QS for submit@debbugs.gnu.org; Sat, 28 Dec 2019 01:29:13 -0500 Received: from lists.gnu.org ([209.51.188.17]:53693) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1il5b3-0002oC-JV for submit@debbugs.gnu.org; Sat, 28 Dec 2019 01:29:11 -0500 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> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (gnu/linux) MIME-Version: 1.0 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches 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 From b48eb1c6d876ec16df098d2373c30b43fb07aef7 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. --- 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 # Copyright © 2019 Evan Straw # Copyright © 2019 Brett Gilio +# Copyright © 2019 Amin Bandali # # 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 +;;; +;;; 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 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