projects/guix·blob java-team · refs

166 lines · 7.1 KiB

1;;; GNU Guix --- Functional package management for GNU
2;;; Copyright © 2018-2021 Julien Lepiller <[email protected]>
3;;; Copyright © 2018, 2019 Tobias Geerinckx-Rice <[email protected]>
4;;; Copyright © 2019 Dan Frumin <[email protected]>
5;;; Copyright © 2020 Brett Gilio <[email protected]>
6;;; Copyright © 2020 Björn Höfling <[email protected]>
7;;; Copyright © 2020 raingloom <[email protected]>
8;;; Copyright © 2020 Robin Green <[email protected]>
9;;; Copyright © 2021 Xinglu Chen <[email protected]>
10;;; Copyright © 2021 Simon Tournier <[email protected]>
11;;; Copyright © 2022 Garek Dyszel <[email protected]>
12;;; Copyright © 2024 Foundation Devices, Inc. <[email protected]>
13;;; Copyright © 2024 Zheng Junjie <[email protected]>
14;;; Copyright © 2026 Dan Rostovtsev <[email protected]>
15;;; Copyright © 2026 Jason Conroy <[email protected]>
16;;;
17;;; This file is part of GNU Guix.
18;;;
19;;; GNU Guix is free software; you can redistribute it and/or modify it
20;;; under the terms of the GNU General Public License as published by
21;;; the Free Software Foundation; either version 3 of the License, or (at
22;;; your option) any later version.
23;;;
24;;; GNU Guix is distributed in the hope that it will be useful, but
25;;; WITHOUT ANY WARRANTY; without even the implied warranty of
26;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
27;;; GNU General Public License for more details.
28;;;
29;;; You should have received a copy of the GNU General Public License
30;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
31
32(define-module (gnu packages rocq)
33 #:use-module (gnu packages base)
34 #:use-module (gnu packages gawk)
35 #:use-module (gnu packages gtk)
36 #:use-module (gnu packages multiprecision)
37 #:use-module (gnu packages ocaml)
38 #:use-module (guix build-system dune)
39 #:use-module (guix gexp)
40 #:use-module (guix git-download)
41 #:use-module (guix licenses)
42 #:use-module (guix packages))
43
44(define (rocq-arguments opam-package-name)
45 ;; Dune parallel build is not reproducible (in rocq and camlp-streams,
46 ;; at least).
47 ;; First observed in Rocq in 2019 by bmwiedemann at OpenSUSE.
48 ;; - https://github.com/rocq-prover/rocq/issues/11229
49 ;; Was escalated to a specific package by Rocq team in 2023.
50 ;; - https://github.com/ocaml/camlp-streams/issues/9
51 ;; Was escalated to Dune by Xavier Leroy in 2023.
52 ;; - https://github.com/ocaml/dune/issues/9152
53 ;; AFAIK, no patches addressing this in any project circa 2026.
54 (list #:package opam-package-name
55 #:build-flags ''("-j1")
56 ;; The tests must be serial as well for reproducible builds.
57 #:test-flags ''("-j1")))
58
59(define-public rocq-runtime
60 (package
61 (name "rocq-runtime") ;see rocq-runtime.opam in rocq's git
62 (version "9.2.0")
63 (source
64 (origin
65 (method git-fetch)
66 ;; Use github uri as recommended by "Contributing" docs.
67 ;; Signed by Nicolas Tabareau (GPG: 5F6E82ADF36B53F6)
68 (uri (git-reference
69 (url "https://github.com/rocq-prover/rocq")
70 (commit (string-append "V" version))))
71 (file-name (git-file-name name version))
72 (sha256
73 (base32 "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
74 (build-system dune-build-system)
75 (arguments
76 (rocq-arguments "rocq-runtime"))
77 (propagated-inputs (list ocaml-zarith camlzip ocaml-yojson))
78 (inputs (list gmp))
79 (native-inputs (list ocaml-ounit2 which))
80 (native-search-paths
81 (list
82 (search-path-specification
83 (variable "ROCQLIB")
84 (files (list "lib/ocaml/site-lib/coq")))
85 (search-path-specification
86 (variable "ROCQRUNTIMELIB")
87 (files (list "lib/ocaml/site-lib/rocq-runtime")))))
88 (home-page "https://rocq-prover.org/")
89 (synopsis "Core Binaries and Tools for the Rocq Prover")
90 (description
91 "Rocq is an interactive theorem prover, or proof assistant. It provides
92a formal language to write mathematical definitions, executable algorithms
93and theorems together with an environment for semi-interactive development
94of machine-checked proofs.
95
96This package includes the Rocq Prover core binaries, plugins, and tools, but
97not the language's standard library implementation.")
98 ;; The source code is distributed under lgpl2.1.
99 ;; Some of the documentation is distributed under opl1.0+.
100 (license (list lgpl2.1 opl1.0+))))
101
102(define-public rocq-core
103 (package
104 (inherit rocq-runtime)
105 (name "rocq-core") ;see rocq-core.opam in rocq's git
106 (arguments
107 (append (rocq-arguments "rocq-core")
108 (list #:phases
109 ;; this is the only package in rocq that /needs/ a "dunestrap"
110 #~(modify-phases %standard-phases
111 (add-before 'build 'make-dunestrap
112 (lambda _
113 (invoke "make" "DUNEOPT=-j1" "COQ_SPLIT=1"
114 "dunestrap")))))))
115 (propagated-inputs (modify-inputs (package-propagated-inputs rocq-runtime)
116 (append rocq-runtime)))
117 (synopsis "Standard library modules for Rocq Prover")
118 (description
119 "Rocq is an interactive theorem prover, or proof assistant. It provides
120 a formal language to write mathematical definitions, executable algorithms
121and theorems together with an environment for semi-interactive development
122of machine-checked proofs.
123
124This package includes the Rocq standard library some other core language
125libraries.")))
126
127; The Rocq project refers to the pacakge as the "RocqIDE server," but has not
128; yet changed the name of the opam package.
129; https://rocq-prover.org/install
130(define-public rocqide-server
131 (package
132 (inherit rocq-runtime)
133 (name "rocqide-server") ;see coqide-server.opam in rocq's git
134 (propagated-inputs (modify-inputs (package-propagated-inputs rocq-runtime)
135 (append rocq-runtime)))
136 (arguments
137 (rocq-arguments "coqide-server"))
138 (synopsis "Rocq's XML protocol server")
139 (description
140 "Rocq is an interactive theorem prover, or proof assistant. It provides
141 a formal language to write mathematical definitions, executable algorithms
142and theorems together with an environment for semi-interactive development
143of machine-checked proofs.
144
145This package provides the @code{coqidetop} language server, an implementation of
146Rocq's XML protocol which allows clients, such as RocqIDE, to interact with
147the Rocq Prover in a structured way.")))
148
149(define-public rocqide
150 (package
151 (inherit rocq-runtime)
152 (name "rocqide") ;see rocqide.opam in rocq's git
153 (propagated-inputs (modify-inputs (package-propagated-inputs
154 rocqide-server)
155 (append rocqide-server ocaml-lablgtk3-sourceview3)))
156 (arguments
157 (rocq-arguments "rocqide"))
158 (synopsis "Rocq's IDE")
159 (description
160 "Rocq is an interactive theorem prover, or proof assistant. It provides
161 a formal language to write mathematical definitions, executable algorithms
162and theorems together with an environment for semi-interactive development
163of machine-checked proofs.
164
165This package provides the RocqIDE, a graphical user interface for the
166development of interactive proofs.")))