summaryrefslogtreecommitdiff
path: root/gnu/packages/rocq.scm
diff options
context:
space:
mode:
Diffstat (limited to 'gnu/packages/rocq.scm')
-rw-r--r--gnu/packages/rocq.scm19
1 files changed, 19 insertions, 0 deletions
diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index e3a9509b93d..846a9ac4f85 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -110,3 +110,22 @@ of machine-checked proofs.
This package includes the Rocq standard library some other core language
libraries.")))
+
+(define-public rocqide-server
+ (package
+ (inherit rocq-runtime)
+ (name "rocqide-server") ;see coqide-server.opam in rocq's git
+ (propagated-inputs (modify-inputs (package-propagated-inputs rocq-runtime)
+ (append rocq-runtime)))
+ (arguments
+ (rocq-arguments "coqide-server"))
+ (synopsis "Rocq's XML protocol server")
+ (description
+ "Rocq 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 @code{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.")))