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