;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2026 Dan Rostovtsev <dan@rostovtsev.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 rocq)
  #:use-module (gnu packages base)
  #:use-module (gnu packages gawk)
  #:use-module (gnu packages gtk)
  #:use-module (gnu packages multiprecision)
  #:use-module (gnu packages ocaml)
  #:use-module (guix build-system dune)
  #:use-module (guix gexp)
  #:use-module (guix git-download)
  #:use-module (guix licenses)
  #:use-module (guix packages))

;; coq-core and coqide-server target names not chagned as of V9.2.0.
(define rocq-essential-pkgs '("rocq-core" "rocq-runtime" "coq-core"))
(define rocqide-pkg "rocqide")
(define rocqide-server-pkg "coqide-server")

(define (rocq-build-phases packages-to-install)
  ;; Run "make help-install" in Rocq to see project install instructions.
  ;; We build all final user targets, but only install a subset.
  ;; This is to allow the main language, the IDE and the IDE server to be
  ;; installed separately.

  ;; Dune parallel build is not reproducible (in rocq and camlp-streams,
  ;; at least).
  ;; First observed in Rocq in 2019 by bmwiedemann at OpenSUSE.
  ;; - https://github.com/rocq-prover/rocq/issues/11229
  ;; Was escalated to a specific package by Rocq team in 2023.
  ;; - https://github.com/ocaml/camlp-streams/issues/9
  ;; Was escalated to Dune by Xavier Leroy in 2023.
  ;; - https://github.com/ocaml/dune/issues/9152
  ;; AFAIK, no patches addressing this in any project circa 2026.
  (let ((all-packages
	 `(,@rocq-essential-pkgs ,rocqide-pkg ,rocqide-server-pkg)))
    #~(modify-phases %standard-phases
	(add-before 'build 'configure
          (lambda* (#:key outputs #:allow-other-keys)
            (let* ((out (assoc-ref outputs "out")))
	      (invoke "./configure" "-prefix" out))))
	(add-before 'build 'make-dunestrap
          (lambda _ (invoke "make" "DUNEOPT=-j1" "dunestrap")))
	(replace 'build
	  (lambda _ (invoke "dune" "build" "-j1" "-p"
			    (string-join '#$all-packages ","))))
        (replace 'check
          ;; Targets built for check can get included in install ...
          ;; ... and can also cause indeterminacy. "-j1" necessary here.
          (lambda* (#:key tests? #:allow-other-keys)
                          (if tests?
                              (invoke "dune" "build" "-j1" "@check"))))
	(replace 'install
	  (lambda* (#:key outputs #:allow-other-keys)
	    (let* ((out (assoc-ref outputs "out"))
		   (libdir (string-append out "/lib/ocaml/site-lib")))
	      (primitive-eval
	       (cons* invoke "dune" "install"
		      "--prefix" out '#$packages-to-install))))))))

(define-public rocq
  (package
    (name "rocq")
    (version "9.2.0")
    (source
     (origin
       (method git-fetch)
       ;; Opted to use github uri as recommended by "Contributing" docs.
       ;; Signed by Nicolas Tabareau (GPG: 5F6E82ADF36B53F6)
       (uri (git-reference
             (url "https://github.com/rocq-prover/rocq")
             (commit "V9.2.0")))
       (sha256
        (base32 "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
    (native-search-paths
     (list (search-path-specification
            (variable "ROCQPATH")
            (files (list "lib/rocq/user-contrib")))))
    (build-system dune-build-system)
    (arguments
     (list
      #:phases (rocq-build-phases rocq-essential-pkgs)))
    (propagated-inputs (list ocaml-zarith camlzip ocaml-lablgtk3-sourceview3
                             ocaml-yojson))
    (inputs (list gmp))
    (native-inputs (list ocaml-ounit2 which))
    (properties '((upstream-name . "rocq")))
    (home-page "https://rocq-prover.org/")
    (synopsis "Proof assistant for higher-order logic")
    (description
     "The Rocq Prover is an interactive theorem prover, or proof assistant.
It provides a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for semi-interactive
development of machine-checked proofs.")
    ;; The source code is distributed under lgpl2.1.
    ;; Some of the documentation is distributed under opl1.0+.
    (license (list lgpl2.1 opl1.0+))))

(define-public rocqide-server
  (package
    (inherit rocq)
    (name "rocqide-server")
    (synopsis "The Rocq Prover XML Language Server")
    (description
     "A language server for the Rocq language and interactive theorem
prover. An implementation of Rocq's XML protocol.")
    (arguments
     (list
      #:phases (rocq-build-phases `(,rocqide-server-pkg))))))

(define-public rocqide
  (package
    (inherit rocq)
    (name "rocqide")
    (synopsis "The Rocq Prover --- GTK3 IDE")
    (description
     "The Rocq Prover graphical user interface for interactive proof
development.")
    (arguments
     (list
      #:phases (rocq-build-phases `(,rocqide-pkg))))))