;;; 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))

(define (rocq-arguments package-name)
  ;; 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.
  (list
   #:package package-name
   #:build-flags ''("-j1")
   ;; The tests must be serial as well for reproducible builds.
   #:test-flags ''("-j1")))

(define-public rocq-runtime
  (package
    (name "rocq-runtime") ; see rocq-runtime.opam in rocq's git
    (version "9.2.0")
    (home-page "https://rocq-prover.org/")
    (synopsis "The Rocq Prover -- Core Binaries and Tools")
    (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.

This package includes the Rocq Prover core binaries, plugins, and tools, but
not the vernacular standard library.")
    (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 "V0.9.2")))
       (sha256
        (base32 "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
    (build-system dune-build-system)
    (arguments (rocq-arguments "rocq-runtime"))
    (propagated-inputs (list ocaml-zarith camlzip ocaml-yojson))
    (inputs (list gmp))
    (native-inputs (list ocaml-ounit2 which))
    (native-search-paths
     (map
      (lambda (pair)
        (let ((env (car pair))
              (path (cdr pair)))
          (search-path-specification (variable env) (files (list path)))))
      '(("ROCQLIB" . "lib/ocaml/site-lib/coq")
        ("ROCQRUNTIMELIB" . "lib/ocaml/site-lib/rocq-runtime"))))
    ;; 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 rocq-core
  (package
    (inherit rocq-runtime)
    (name "rocq-core") ; see rocq-core.opam in rocq's git
    (synopsis "The Rocq Prover with its standard modules")
    (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.

This package includes the Rocq prelude, that is loaded automatically
by Rocq in every .v file, as well as other modules bound to the
Corelib.* and Ltac2.* namespaces.")
    (arguments
     (append
      (rocq-arguments "rocq-core")
      (list
       #:phases
       ;; this is the only package in rocq that /needs/ a "dunestrap"
       #~(modify-phases %standard-phases
           (add-before 'build 'make-dunestrap
             (lambda _
               (invoke "make" "DUNEOPT=-j1" "COQ_SPLIT=1" "dunestrap")))))))
    (propagated-inputs
     (modify-inputs (package-propagated-inputs rocq-runtime)
       (append rocq-runtime)))))

(define-public rocqide-server
  (package
    (inherit rocq-runtime)
    (name "rocqide-server") ; see coqide-server.opam in rocq's git
    (synopsis "The Rocq Prover, XML protocol server")
    (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.

This package provides the `coqidetop` language server, an implementation of
Rocq's XML protocol which allows clients, such as RocqIDE, to interact with
the Rocq Prover in a structured way.")
    (propagated-inputs
     (modify-inputs (package-propagated-inputs rocq-runtime)
       (append rocq-runtime)))
    (arguments (rocq-arguments "coqide-server"))))

(define-public rocqide
  (package
    (inherit rocq-runtime)
    (name "rocqide") ; see rocqide.opam in rocq's git
    (synopsis "The Rocq Prover --- GTK3 IDE")
    (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.

This package provides the RocqIDE, a graphical user interface for the
development of interactive proofs.")
    (propagated-inputs
     (modify-inputs
         (package-propagated-inputs rocqide-server)
       (append rocqide-server ocaml-lablgtk3-sourceview3)))
    (arguments (rocq-arguments "rocqide"))))