;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2019 Amin Bandali <bandali@gnu.org>
;;; Copyright © 2020 Brett Gilio <brettg@gnu.org>
;;; Copyright © 2020 Tobias Geerinckx-Rice <me@tobias.gr>
;;;
;;; 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.23.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
                "09mklc1p6ms1jayg2f89hqfmhca3h5744lli936l38ypn1d00sxx"))))
    (build-system cmake-build-system)
    (inputs
     `(("gmp" ,gmp)))
    (arguments
     `(#:build-type "Release"           ; default upstream build type
       ;; XXX: Test phases currently fail on 32-bit sytems.
       ;; Tests for those architectures have been temporarily
       ;; disabled, pending further investigation.
       #:tests? ,(let ((arch (or (%current-target-system)
                              (%current-system))))
                   (not (or (string-prefix? "i686" arch)
                            (string-prefix? "armhf" arch))))
       #: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 "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)))
f.in, etc/guix-daemon.service.in,
etc/init.d/guix-daemon.in: Add an explicit ‘--substitute-urls’ option.

Change-Id: Ie491b7fab5c42e54dca582801c03805a85de2bf9
</span></span></td><td>Ludovic Courtès</td></tr>
<tr><td><span title='2024-04-03 17:18:38 +0100'>2024-04-03</span></td><td><a href='/guix/commit/config-daemon.ac?id=ac19e038b457d0585812091200005befd9b29259'>Switch order of the default substitute servers.</a><span class='msg-avail'>...<span class='msg-tooltip'>The aim here is to improve the user experience.  There's anecdotal evidence
that the network performance for bordeaux is better compared to ci at least
for some users, and I don't know of any issues with rate limiting or access
restriction for bordeaux compared to ci.  It also has IPv6 support.

Additionally, bordeaux generally had more substitutes than ci, particularly
for aarch64-linux and armhf-linux.  This change will offer a very slight
speedup for those substitutes that only bordeaux has.

Bordeaux has been a default substitute server for nearly 3 years now and I
think this change is overdue.  I'm also hopeful that we'll be able to build on
the testing regarding mirrors for bordeaux, and that'll allow potentially
improving the hosting setup (through providing more redundancy) and further
improving substitute fetching for users who currently have issues with
substitute access.

* config-daemon.ac: Switch substitute urls order.
* doc/guix.texi: Ditto.
* etc/guix-install.sh: Ditto.
* gnu/installer/newt/network.scm (wait-service-online): Ditto.
* guix/store.scm (%default-substitute-urls): Ditto.

Change-Id: I4f6d93ae1fc8b03d80b47b18b5749a51f1fde17b
Signed-off-by: Christopher Baines &lt;mail@cbaines.net&gt;
</span></span></td><td>Christopher Baines</td></tr>