Added rocq, along with ide and ide-server.HEADmain

1 files changed, 120 insertions, 24 deletions

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index d0837b4..5874a82 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -3,6 +3,11 @@
   #:use-module (gnu packages base)  
   #:use-module (gnu packages coq)
   #:use-module (gnu packages gawk)
+  #:use-module (gnu packages gtk)  
+  #:use-module (gnu packages multiprecision)
+  #:use-module (gnu packages ocaml)
+  #:use-module (gnu packages version-control)
+  #:use-module (guix build-system dune)  
   #:use-module (guix build-system gnu)
   #:use-module (guix download)
   #:use-module (guix gexp)
@@ -10,29 +15,120 @@
   #:use-module (guix licenses)
   #:use-module (guix packages))
 
+
+(define rocq-essential-pkgs '("rocq-core" "rocq-runtime" "coq-core"))
+(define rocqide-pkg "rocqide")
+(define rocqide-server-pkg "coqide-server") ;; not changed as of V9.2.0.
+
+(define (rocq-build-phases packages-to-install)
+  ;; Run "make help-install" in rocq to see instructions for "final users".
+  ;; 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.
+  (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"))
+                   (rocqlib (string-append out "/lib/ocaml/site-lib/rocq/")))
+              (invoke "./configure" "-prefix" out
+                      "-libdir" rocqlib))))
+	(add-before 'build 'make-dunestrap
+          (lambda _ (invoke "make" "dunestrap")))
+	(replace 'build
+	  (lambda _ (invoke "dune" "build" "-p"
+			    (string-join '#$all-packages ","))))
+	(replace 'check
+	  (lambda _ (invoke "dune" "build" "@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)
+       (uri (git-reference
+             (url "https://github.com/rocq-prover/rocq.git")
+             (commit (string-append "V" version))))
+       (file-name (git-file-name name version))
+       (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"))) ; also for inherited packages
+    (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")
+    (arguments
+     (list
+      #:phases (rocq-build-phases `(,rocqide-server-pkg))))))
+
+(define-public rocqide
+  (package
+    (inherit rocq)
+    (name "rocqide")
+    (arguments
+     (list
+      #:phases (rocq-build-phases `(,rocqide-pkg))))))
+
 (define-public lambda
   (package
-   (name "lambda")
-   (version "0.0.1")
-   (source (origin
-	     (method git-fetch)
-	     (uri (git-reference
-			(url "git://git.rostovtsev.org/lambda")
-			(commit "v0.0.1")))
-	    (sha256
-	     (base32 ;; nix32
-	      "0yk1shd3d6kz8pdbv11fg462kcvxvsw6lvmp7plqiiqicm4fbir4"))))
-   (build-system gnu-build-system)
-   (native-inputs (list coq
-			autoconf
-			automake ; alocal used here for some reason
-			which    ; used in autoconf step
-			gawk     ; used in autoconf step
-			))
-   (synopsis "Fundamental objects and results in the untyped lambda calculus.")
-   (description
-    (string-append
-     "A Rocq library for working with a weak call-by-value lambda calculus."
-     "Provides proofs of the Church-Rosser Properties and Uniform Confluence."))
-   (home-page "https://git.rostovtsev.org/lambda")
-   (license gpl3+)))
+    (name "lambda")
+    (version "0.0.1")
+    (source (origin
+	      (method git-fetch)
+	      (uri (git-reference
+		     (url "git://git.rostovtsev.org/lambda")
+		     (commit "v0.0.1")))
+	      (sha256
+	       (base32 ;; nix32
+		"0yk1shd3d6kz8pdbv11fg462kcvxvsw6lvmp7plqiiqicm4fbir4"))))
+    (build-system gnu-build-system)
+    (native-inputs (list coq
+			 autoconf
+			 automake   ; alocal used here for some reason
+			 which	    ; used in autoconf step
+			 gawk	    ; used in autoconf step
+			 ))
+    (synopsis "Fundamental objects and results in the untyped lambda calculus.")
+    (description
+     (string-append
+      "A Rocq library for working with a weak call-by-value lambda calculus."
+      "Provides proofs of the Church-Rosser Properties and Uniform Confluence."))
+    (home-page "https://git.rostovtsev.org/lambda")
+    (license gpl3+)))