;;; 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)))
s-qcow2-image): New variables.

* gnu/system/images/hurd.scm (hurd64-barebones-os): New variable.
</span></span></td><td>Janneke Nieuwenhuizen</td></tr>
<tr><td><span title='2024-11-11 07:28:33 +0100'>2024-11-11</span></td><td><a href='/guix/commit/gnu/system/images?id=6dbfe1a118dcded3a9d77f8321aa43fbdd255011'>system: hurd: Remove qemu networking from %base-services/hurd.</a><span class='msg-avail'>...<span class='msg-tooltip'>This allows us to use %base-services/hurd for services in a Hurd config for a
real machine without removing static-networking.

* gnu/system/hurd.scm (%base-services/hurd): Factor networking out to...
(%base-services+qemu-networking/hurd): ..this new variable.
* gnu/system/examples/bare-hurd.tmpl (%hurd-os): Use it.
* gnu/services/virtualization.scm (%hurd-vm-operating-system): Use it.
* gnu/system/images/hurd.scm (hurd-barebones-os): Use it.  Add comment about
QEMU and networking for a real machine.

Change-Id: I777a63410383b9bf8b5740e4513dbc1e9fb0fd41
</span></span></td><td>Janneke Nieuwenhuizen</td></tr>
<tr><td><span title='2024-09-08 02:00:00 +0200'>2024-09-08</span></td><td><a href='/guix/commit/gnu/system/images?id=7eddfea4a01e95a58a2c18f71bc4a345a1ad378f'>images: wsl2: Update comment.</a><span class='msg-avail'>...<span class='msg-tooltip'>* gnu/system/images/wsl2.scm (wsl-boot-program): Update privileged
program directory in a comment.

Change-Id: I65906cbfbcd17ff164837ad293dc4324314bfcf1
</span></span></td><td>Tobias Geerinckx-Rice</td></tr>
<tr><td><span title='2024-05-22 11:15:30 +0800'>2024-05-22</span></td><td><a href='/guix/commit/gnu/system/images?id=327a1f0779a5df8ebb57e39d4a44e040a5d0bdfe'>system: images: Add visionfive2 module.</a><span class='msg-avail'>...<span class='msg-tooltip'>* gnu/system/images/visionfive2.scm: New file.
* gnu/local.mk (GNU_SYSTEM_MODULES): Add it.

Change-Id: I8831f1148bcddb0d604e1174034fca85cd2887a1
</span></span></td><td>Zheng Junjie</td></tr>
<tr><td><span title='2024-04-18 10:43:06 -0400'>2024-04-18</span></td><td><a href='/guix/commit/gnu/system/images?id=65e8472a4b6fc6f66871ba0dad518b7d4c63595e'>system: Remove nss-certs from OS templates, adjust doc.</a><span class='msg-avail'>...<span class='msg-tooltip'>This is a follow-up to commit 86afaadb51 ("system: Add 'nss-certs' to
%base-packages-networking.")

* doc/guix-cookbook.texi (Running Guix on a Linode Server): Remove nss-certs
from operating system's packages field.
(Running Guix on a Kimsufi Server): Likewise.
* doc/guix.texi (Using the Configuration System): Likewise.
(X.509 Certificates): Adjust to mention nss-certs *is* part of %base-packages.
* gnu/installer/services.scm (%system-services): Remove recommendation to
install nss-certs.
* gnu/system/examples/bare-bones.tmpl (host-name): Remove obsolete comments.
* gnu/system/examples/desktop.tmpl (packages): Remove nss-certs.
* gnu/system/examples/lightweight-desktop.tmpl (packages): Likewise.
* gnu/system/examples/plasma.tmpl (packages): Likewise.
* gnu/system/examples/raspberry-pi-64-nfs-root.tmpl (packages): Likewise.
* gnu/system/examples/raspberry-pi-64.tmpl (packages): Likewise.
* gnu/system/examples/vm-image.tmpl (packages): Likewise.
* gnu/system/images/orangepi-r1-plus-lts-rk3328.scm (packages): Likewise.
* gnu/system/images/pine64.scm (packages): Likewise.
* gnu/system/install.scm (installation-os) [packages]: Likewise.

Change-Id: If09123a69b987178bcb0aab61c4570c14fc1286f
</span></span></td><td>Maxim Cournoyer</td></tr>
<tr><td><span title='2023-12-22 16:06:15 -0800'>2023-12-22</span></td><td><a href='/guix/commit/gnu/system/images?id=ab1ff7ca40b0a2d935f715dcf64f0f3128632d3d'>images: Add orangepi-r1-plus-lts image.</a><span class='msg-avail'>...<span class='msg-tooltip'>* gnu/local.mk: Register image.
* gnu/system/images/orangepi-r1-plus-lts-rk3328.scm: New file.
* gnu/system/install.scm (orangepi-r1-plus-lts-rk3328-installation-os):
  New variable.

Signed-off-by: Vagrant Cascadian &lt;vagrant@debian.org&gt;
</span></span></td><td>Herman Rimm</td></tr>