Runtime profiles fixed. Package definitions cleaned up.

* RocqExample.v: An example Rocq file to test the REPL.
* gnu/packages/rocq.scm: Reflected Rocq opam package defintitions in Guix
definitions. Used propogated-inputs and native-search-paths. Led to several
simplifications. Added clearer synopses.
* test-rocq.bash: Exercises the build and simple usage of rocq.

Change-Id: Ia9fb52b54219de666fff27511c71f642c18ff845
Signed-off-by: Dan Rostovtsev <dan@rostovtsev.org>

3 files changed, 98 insertions, 42 deletions

diff --git a/RocqExample.v b/RocqExample.v
new file mode 100644
index 00000000000..4ce1aec016d
--- /dev/null
+++ b/RocqExample.v
@@ -0,0 +1,4 @@
+Inductive term : Type :=
+| var (n: nat)
+| app (u: term) (v: term)
+| lambda (u: term).
diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index 9116da97430..c5f5b6628da 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -28,9 +28,7 @@
   #:use-module (guix licenses)
   #:use-module (guix packages))
 
-(define (rocq-package-arguments package-name)
-  ;; Run "make help-install" in Rocq to see project install instructions.
-
+(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.
@@ -43,12 +41,23 @@
   (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")
+    (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)
@@ -59,24 +68,19 @@
               (commit "V0.9.2")))
        (sha256
         (base32 "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
-    (native-search-paths
-     (list (search-path-specification
-             (variable "ROCQPATH")
-             (files (list "lib/rocq/user-contrib")))))
     (build-system dune-build-system)
-    (arguments (rocq-package-arguments "rocq-runtime"))
-    (propagated-inputs (list ocaml-zarith camlzip ocaml-lablgtk3-sourceview3
-                             ocaml-yojson))
+    (arguments (rocq-arguments "rocq-runtime"))
+    (propagated-inputs (list ocaml-zarith camlzip ocaml-yojson))
     (inputs (list gmp))
     (native-inputs (list ocaml-ounit2 which))
-    (properties '((upstream-name . "rocq-core")))
-    (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.")
+    (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+))))
@@ -84,42 +88,65 @@ development of machine-checked proofs.")
 (define-public rocq-core
   (package
     (inherit rocq-runtime)
-    (name "rocq-core")
-    (inputs (modify-inputs (package-inputs rocq-runtime)
-              (append 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-package-arguments "rocq-core")
+      (rocq-arguments "rocq-core")
       (list
        #:phases
-       ;; this is the only phase that needs a "dunestrap"
-       ;; it needs to pick up the rocq-runtime dependency
+       ;; 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")))))))))
+               (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")
-    (inputs (modify-inputs (package-inputs rocq-runtime)
-              (append rocq-runtime)))
-    ;; opam-name note changed as of V9.2.0
-    (arguments (rocq-package-arguments "coqide-server"))))
+    (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")
-    (inputs (modify-inputs (package-inputs rocqide-server)
-              (append rocqide-server)))
-    (arguments (rocq-package-arguments "rocqide"))))
+    (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.
 
-;; Last piece:
-;; To run, the ROCQRUNTIMELIB and ROCQLIB need to be set in the profile.
-;; In the current configuration, they do not do so.
-;; The user needs to run
-;; ROCQRUNTIMELIB=... ROCQLIB=... rocq top
-;; to get a rocq repl.
-;; See "propagated inputs" and "profiles" to understand this more clearly.
+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"))))
diff --git a/test-rocq.bash b/test-rocq.bash
new file mode 100644
index 00000000000..4159d21f0c8
--- /dev/null
+++ b/test-rocq.bash
@@ -0,0 +1,25 @@
+set -e
+
+# clean up before starting
+echo cleaning rocq builds
+guix gc -D $(find /gnu/store -maxdepth 1 -name "*rocq*")
+
+# copy to temp to keep avoid recompiling unnecessary files
+TMP=`mktemp -t -d test-rocq.bash.XXXXXX`
+mkdir -p $TMP/gnu/packages
+cp gnu/packages/rocq.scm $TMP/gnu/packages
+
+for PKG in rocq-runtime rocq-core rocqide rocqide-server
+do
+    echo building $PKG ...
+    guix build -L $TMP $PKG
+    echo ... success
+done
+
+echo testing repl ...
+guix shell -L scratch/ rocq-runtime rocq-core  -- rocq top < RocqExample.v
+echo ... success
+
+echo rocq tests finished successfully
+
+trap "rm -rf $TMP* 2>EXIT" 0