;;; 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>
;;; Copyright © 2022 Pradana Aumars <paumars@courrier.dev>
;;; Copyright © 2023 Zhu Zihao <all_but_last@163.com>
;;; Copyright © 2024 Antero Mejr <mail@antr.me>
;;;
;;; 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 (guix build-system cmake)
  #:use-module (guix build-system emacs)
  #:use-module (guix build-system lean)
  #:use-module (guix build-system python)
  #:use-module (guix download)
  #:use-module (guix gexp)
  #:use-module (guix git-download)
  #:use-module (guix packages)
  #:use-module (guix platform)
  #:use-module (guix utils)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (gnu packages base)
  #:use-module (gnu packages graphviz)
  #:use-module (gnu packages libevent)
  #:use-module (gnu packages multiprecision)
  #:use-module (gnu packages perl)
  #:use-module (gnu packages python-build)
  #:use-module (gnu packages python-crypto)
  #:use-module (gnu packages python-web)
  #:use-module (gnu packages python-xyz)
  #:use-module (gnu packages version-control))

(define-public lean
  (package
    (name "lean")
    (version "4.10.0") ;TODO: when updating, update mathlib deps as well
    (source (origin
              (method git-fetch)
              (uri (git-reference
                    (url "https://github.com/leanprover/lean4")
                    (commit (string-append "v" version))))
              (file-name (git-file-name name version))
              (sha256
               (base32
                "1q0xfg0apzb0dwj71k46w5218hwm2k890cgslwzr4mlyhvrspmcl"))))
    (build-system cmake-build-system)
    (arguments
     (list #:build-type "Release" ;default upstream build type
           #:phases
           #~(modify-phases %standard-phases
               (add-after 'unpack 'patch
                 (lambda _
                   (substitute* "stage0/src/CMakeLists.txt"
                     (("set\\(LEAN_PLATFORM_TARGET.*$")
                      (format #f "\
set(LEAN_PLATFORM_TARGET \"~a-linux-gnu\" CACHE STRING \
\"LLVM triple of the target platform\")\n"
                              #$(platform-linux-architecture
                                 (lookup-platform-by-target-or-system
                                  (or (%current-target-system)
                                      (%current-system)))))))
                   (substitute* '("src/lean.mk.in"
                                  "src/stdlib.make.in"
                                  "stage0/src/lean.mk.in"
                                  "stage0/src/stdlib.make.in")
                     (("/usr/bin/env bash")
                      (which "bash")))
                   (substitute* "src/lake/examples/reverse-ffi/Makefile"
                     (("cc -o")
                      "gcc -o")))))))
    (native-search-paths
     (list (search-path-specification
            (variable "LEAN_PATH")
            (files (list (string-append "lib/lean"
                                        (version-major+minor version)
                                        "/packages"))))))
    (native-inputs (list diffutils git-minimal perl))
    (inputs (list gmp libuv))
    (synopsis "Theorem prover and programming language")
    (home-page "https://lean-lang.org")
    (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)))

(define-public lean3
  (package
    (inherit lean)
    (name "lean")
    (version "3.51.1")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                    (url "https://github.com/leanprover-community/lean")
                    (commit (string-append "v" version))))
              (file-name (git-file-name name version))
              (sha256
               (base32
                "17g4d3lqnbl1yfy2pjannf73v8qhc5003d2jkmrqiy05zkqs8d9n"))))
    (arguments
     (list #:build-type "Release"
           ;; XXX: Test phases currently fail on 32-bit sytems.
           ;; Tests for those architectures have been temporarily
           ;; disabled, pending further investigation.
           #:tests? (and (not (%current-target-system))
                         (let ((arch (%current-system)))
                           (not (or (string-prefix? "i686" arch)
                                    (string-prefix? "armhf" arch)))))
           #:phases #~(modify-phases %standard-phases
                        (add-before 'configure 'chdir-to-src
                          (lambda _ (chdir "src"))))))
    (inputs (list gmp))))

(define-public python-mathlibtools
  (package
    (name "python-mathlibtools")
    (version "1.1.1")
    (source (origin
              (method url-fetch)
              (uri (pypi-uri "mathlibtools" version))
              (sha256
               (base32
                "089pql105imx8z7ar1wiz9fn000jp6xqdfixw4jf2vric94vn9fj"))))
    (build-system python-build-system)
    (arguments
     '(#:phases (modify-phases %standard-phases
                  (add-before 'check 'fix-home-directory
                    (lambda _
                      (setenv "HOME" "/tmp"))))))
    (inputs (list python-toml
                  python-pygithub
                  python-certifi
                  python-gitpython
                  python-requests
                  python-click
                  python-tqdm
                  python-networkx
                  python-pydot
                  python-pyyaml
                  python-atomicwrites))
    (home-page "https://github.com/leanprover-community/mathlib-tools")
    (synopsis "Development tools for Lean mathlib")
    (description
     "This package contains @command{leanproject}, a supporting tool for Lean
mathlib, a mathematical library for the Lean theorem prover.")
    (license license:asl2.0)))

(define-public emacs-lean4-mode
  (let ((commit "da7b63d854d010d621e2c82a53d6ae2d94dd53b0") ;no releases
        (revision "0"))
    (package
      (name "emacs-lean4-mode")
      (version (git-version "0.1.0" revision commit))
      (source
       (origin
         (method git-fetch)
         (uri (git-reference
               (url "https://github.com/leanprover-community/lean4-mode")
               (commit commit)))
         (file-name (git-file-name name version))
         (sha256
          (base32 "0vj9vrfkgm7plp5mvq22fm9sln11j9763g3wd2w6c82rlsk6dhva"))))
      (build-system emacs-build-system)
      (home-page "https://github.com/leanprover-community/lean4-mode")
      (synopsis "Emacs major mode for the Lean 4 theorem prover")
      (description
       "This package provides a major mode and utilities for working with the
Lean 4 theorem prover.")
      (license license:asl2.0))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Please keep everything below here alphabetized.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-public lean-aesop
  (package
    (name "lean-aesop")
    (version "4.10.0") ;matches the version of lean package
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/leanprover-community/aesop")
             (commit (string-append "v" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32 "039rdy7lldkvbl8gvln4v912b9pyx0952mqad49g755yvhgq7zw0"))))
    (build-system lean-build-system)
    (propagated-inputs (list lean-batteries))
    (home-page
     "https://leanprover-community.github.io/mathlib4_docs/Aesop.html")
    (synopsis "Proof search tactic for the Lean theorem prover")
    (description
     "@acronym{Aesop,Automated Extensible Search for Obvious Proofs} is a
proof search tactic for Lean 4.  It is broadly similar to Isabelle's
@code{auto}.")
    (license license:asl2.0)))

(define-public lean-batteries
  (package
    (name "lean-batteries")
    (version "4.10.0") ;matches the version of lean package
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/leanprover-community/batteries")
             (commit (string-append "v" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32 "0q7wcbx3wl318k8x0hh846bdnh960kiqv9bvs83yzwlnqsvgiiga"))))
    (build-system lean-build-system)
    (home-page
     "https://leanprover-community.github.io/mathlib4_docs/Batteries.html")
    (synopsis "Extended standard library for the Lean theorem prover")
    (description
     "This package provides a a collection of data structures and tactics
intended for use by both computer-science applications and mathematics
applications of Lean 4.")
    (license license:asl2.0)))

(define-public lean-cli
  (let ((commit "2cf1030dc2ae6b3632c84a09350b675ef3e347d0")
        (revision "0"))
    (package
      (name "lean-cli")
      (version (git-version "4.10.0" revision commit)) ;matches lean version
      (source
       (origin
         (method git-fetch)
         (uri (git-reference
               (url "https://github.com/leanprover/lean4-cli")
               (commit commit)))
         (file-name (git-file-name name version))
         (sha256
          (base32 "0vj9vrfkgm7plp5mvq22fm9sln11j9763g3wd2w6c82rlsk6dhva"))))
      (build-system lean-build-system)
      (home-page "https://github.com/leanprover/lean4-cli")
      (synopsis "Lean library for creating command-line interfaces")
      (description
       "This package provides a Lean library for creating command-line
interfaces and argument parsing, using a @acronym{DSL, domain-specific
language}.")
      (license license:asl2.0))))

(define-public lean-importgraph
  (package
    (name "lean-importgraph")
    (version "4.10.0") ;matches the version of lean package
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/leanprover-community/import-graph")
             (commit (string-append "v" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32 "0vj9vrfkgm7plp5mvq22fm9sln11j9763g3wd2w6c82rlsk6dhva"))))
    (build-system lean-build-system)
    (propagated-inputs (list lean-batteries lean-cli))
    (home-page "https://github.com/leanprover-community/import-graph")
    (synopsis "Lean tool for generating import graphs of Lake packages")
    (description
     "This package provides a tool to generate import graphs of packages for
Lean's Lake package manager.")
    (license license:asl2.0)))

(define-public lean-mathlib
  (package
    (name "lean-mathlib")
    (version "4.10.0") ;matches the version of lean package
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/leanprover-community/mathlib4")
             (commit (string-append "v" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32 "0qxif7ldrcbd8mrmy6rsxig41jbvffhs6vab3bix15pbil5z4x6q"))))
    (build-system lean-build-system)
    (propagated-inputs (list lean-aesop
                             lean-batteries
                             lean-importgraph
                             lean-proofwidgets
                             lean-qq))
    (home-page "https://leanprover-community.github.io/mathlib4_docs/")
    (synopsis "Math library for the Lean theorem prover")
    (description
     "This package provides a Lean library with proofs and tactics for
programming and mathematics.")
    (license license:asl2.0)))

(define-public lean-proofwidgets
  (package
    (name "lean-proofwidgets")
    (version "0.0.41")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/leanprover-community/ProofWidgets4")
             (commit (string-append "v" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32 "0vj9vrfkgm7plp5mvq22fm9sln11j9763g3wd2w6c82rlsk6dhva"))))
    (build-system lean-build-system)
    (propagated-inputs (list lean-batteries))
    (home-page
     "https://leanprover-community.github.io/mathlib4_docs/ProofWidgets.html")
    (synopsis "User interface library for the Lean theorem prover")
    (description
     "This package provides a library of user interface components for Lean
4. It supports:
@itemize
@item{symbolic visualizations of mathematical objects and data structures}
@item{data visualization}
@item{interfaces for tactics and tactic modes}
@item{alternative and domain-specific goal state displays}
@item{user interfaces for entering expressions and editing proofs}
@end itemize")
    (license license:asl2.0)))

(define-public lean-qq
  (let ((commit "71f54425e6fe0fa75f3aef33a2813a7898392222") ;no tags
        (revision "0"))
    (package
      (name "lean-qq")
      (version (git-version "4.10.0" revision commit)) ;match lean version
      (source
       (origin
         (method git-fetch)
         (uri (git-reference
               (url "https://github.com/leanprover-community/quote4")
               (commit commit)))
         (file-name (git-file-name name version))
         (sha256
          (base32 "0d5qihwqh17ajld2lxjai2y0s0a5551y19da1y8azihlmy540nc8"))))
      (build-system lean-build-system)
      (arguments (list #:tests? #f)) ;no tests
      (home-page
       "https://leanprover-community.github.io/mathlib4_docs/Qq.html")
      (synopsis "Lean library for type-safe expression quotations")
      (description
       "This package provides a Lean library for type-safe expression
quotations, which are a particularly convenient way of constructing
object-level expressions (Expr) in meta-level code.")
      (license license:asl2.0))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; New Lean packages should be alphabetized above.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;