;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2019 Amin Bandali <bandali@gnu.org>
;;; Copyright © 2020 Brett Gilio <brettg@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.17.1")
    (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
                "15yfryg98x9lvy00v1w5kg4hp921mpvlxx1ic3m08k1ls6p1gkj4"))))
    (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 "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)))
ithout to-version"): Change
URLs from https to http, and from libuv.org to libuv.example.org.
Parameterize ‘current-http-proxy’.

Reported-by: Janneke Nieuwenhuizen &lt;janneke@gnu.org&gt;
</span></span></td><td>Ludovic Courtès</td></tr>
<tr><td><span title='2023-08-26 11:38:56 -0400'>2023-08-26</span></td><td><a href='/guix/commit/tests/gnu-maintenance.scm?id=1dce88777691b7a38ad66ba58b17a9b368c11e07'>gnu-maintenance: Consider Qt source tarballs as "release files".</a><span class='msg-avail'>...<span class='msg-tooltip'>* guix/gnu-maintenance.scm (release-file?): Use positive logic in doc.
Add a special case for Qt source archives.
* tests/gnu-maintenance.scm ("release-file?"): Update test.
</span></span></td><td>Maxim Cournoyer</td></tr>
<tr><td><span title='2023-08-26 11:38:56 -0400'>2023-08-26</span></td><td><a href='/guix/commit/tests/gnu-maintenance.scm?id=6953fb924111c400a064255d8274a2caa68f7436'>gnu-maintenance: Add support to rewrite version in URL path.</a><span class='msg-avail'>...<span class='msg-tooltip'>Fixes &lt;https://issues.guix.gnu.org/64015&gt;.
Fixes &lt;https://issues.guix.gnu.org/65304&gt;.

Previously, the generic HTML updater would only look for the list of files
found at the parent of its current source URL, ignoring that the URL may embed
the version elsewhere in its path.  This could cause 'guix refresh' to report
no updates available, while in fact there were, such as for 'libuv'.

* guix/gnu-maintenance.scm (strip-trailing-slash): New procedure.
(%version-rx): New variable.
(rewrite-url): New procedure.
(import-html-release): New rewrite-url? argument.  When true, use the above
procedure.
(import-html-updatable-release): Call import-html-release with #:rewrite-url
set to #t.
* tests/gnu-maintenance.scm ("rewrite-url, to-version specified")
("rewrite-url, without to-version"): New tests.
</span></span></td><td>Maxim Cournoyer</td></tr>
<tr><td><span title='2023-01-02 00:06:51 +0100'>2023-01-02</span></td><td><a href='/guix/commit/tests/gnu-maintenance.scm?id=d7a9d72bb02a2a3b1a99183655bf878547116032'>tests: Fix gnu-maintenance tests.</a><span class='msg-avail'>...<span class='msg-tooltip'>The regression was introduce with commit
a274a6a1acb99738f02de7b226e6a0d3883ec353 ("upstream-updater: Rename record
field.")

* tests/tests/gnu-maintenance.scm: ("latest-html-release, scheme-less URIs",
  "latest-html-release, no signature", "latest-html-release, signature"):
  Replace upstream-updater-latest by upstream-updater-import.

Reported-by: Ricardo Wurmus &lt;rekado@elephly.net&gt;
</span></span></td><td>Hartmut Goebel</td></tr>