diff options
Diffstat (limited to 'gnu/packages/rocq.scm')
| -rw-r--r-- | gnu/packages/rocq.scm | 152 |
1 files changed, 152 insertions, 0 deletions
diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm new file mode 100644 index 00000000000..b75e6763aa2 --- /dev/null +++ b/gnu/packages/rocq.scm @@ -0,0 +1,152 @@ +;;; 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")))) |