;;; GNU Guix --- Functional package management for GNU
;;; 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 (guix build lean-build-system)
  #:use-module ((guix build gnu-build-system) #:prefix gnu:)
  #:use-module (guix build utils)
  #:use-module (ice-9 match)
  #:use-module (ice-9 ftw)
  #:use-module (ice-9 format)
  #:use-module (srfi srfi-1)
  #:use-module (srfi srfi-26)
  #:export (%standard-phases
            add-installed-lean-path
            lean-build))

(define (lean-version lean)
  (let* ((version     (last (string-split lean #\-)))
         (components  (string-split version #\.))
         (major+minor (take components 2)))
    (string-join major+minor ".")))

(define (lib-dir inputs outputs)
  "Return the path of the current output's Lean package directory."
  (let ((out (assoc-ref outputs "out"))
        (lean (assoc-ref inputs "lean")))
    (string-append out "/lib/lean" (lean-version lean) "/packages")))

(define (add-installed-lean-path inputs outputs)
  "Prepend the site-package of OUTPUT to LEAN_PATH.  This is useful when
running checks after installing the package."
  (let ((path-env (getenv "LEAN_PATH")))
    (if path-env
        (setenv "LEAN_PATH" (string-append (lib-dir inputs outputs) ":"
                                           path-env))
        (setenv "LEAH_PATH" (string-append (lib-dir inputs outputs))))))

(define* (build #:key lean-lake-targets #:allow-other-keys)
  "Build a given Lean 4 package."
  (let ((call (cons* "lake" "build" lean-lake-targets)))
    (format #t "running: ~s\n" call)
    (apply invoke call)))

(define* (check #:key tests? #:allow-other-keys)
  "Run all the tests"
  (when tests?
    (let ((call '("lake" "test")))
      (format #t "running: ~s\n" call)
      (apply invoke call))))

(define* (install #:key inputs outputs #:allow-other-keys)
  "Install a given Lean 4 package."
  (let ((out (lib-dir inputs outputs)))
    (format #t "installing Lean library to: ~s\n" out)
    (copy-recursively ".lake/build/lib" out)))

(define* (wrap #:key inputs outputs #:allow-other-keys)
  (define (list-of-files dir)
    (find-files dir (lambda (file stat)
                      (and (eq? 'regular (stat:type stat))
                           (not (wrapped-program? file))))))

  (define bindirs
    (append-map (match-lambda
                  ((_ . dir)
                   (list (string-append dir "/bin")
                         (string-append dir "/sbin"))))
                outputs))

  ;; Do not require "bash" to be present in the package inputs
  ;; even when there is nothing to wrap.
  ;; Also, calculate (sh) only once to prevent some I/O.
  (define %sh (delay (search-input-file inputs "bin/bash")))
  (define (sh) (force %sh))

  (let* ((var `("LEAN_PATH" prefix
                ,(search-path-as-string->list
                  (or (getenv "LEAN_PATH") "")))))
    (for-each (lambda (dir)
                (let ((files (list-of-files dir)))
                  (for-each (cut wrap-program <> #:sh (sh) var)
                            files)))
              bindirs)))

(define* (add-install-to-lean-path #:key inputs outputs #:allow-other-keys)
  "A phase that just wraps the 'add-installed-lean-path' procedure."
  (add-installed-lean-path inputs outputs))

(define %standard-phases
  (modify-phases gnu:%standard-phases
    (delete 'bootstrap)
    (delete 'configure)
    (replace 'build build)
    (replace 'check check)
    (replace 'install install)
    (add-after 'install 'add-install-to-lean-path add-install-to-lean-path)
    (add-after 'add-install-to-lean-path 'wrap wrap)))

(define* (lean-build #:key inputs (phases %standard-phases)
                     #:allow-other-keys #:rest args)
  "Build the given Lean package, applying all of PHASES in order."
  (apply gnu:gnu-build #:inputs inputs #:phases phases args))