First contribution: up to checking non-determinism in build.

* doc/contributing.texi: Notes on a dev env with manifest.scm.
* gnu/packages/rocq.scm: Styling and linting.
* manifest.scm: Adding fontconfig for build in dev env.
* patch-checklist.bash: Script to run checks in contribution guidelines.

Change-Id: I29366066947bc30040f591b9f4fdc21fdf277adc

4 files changed, 118 insertions, 23 deletions

diff --git a/doc/contributing.texi b/doc/contributing.texi
index bf375f9ef5c..9a73e4c5442 100644
--- a/doc/contributing.texi
+++ b/doc/contributing.texi
@@ -193,6 +193,19 @@ Most of the test suite runs without an internet connection. The @option{-N}
 (short for @option{--network}) can be added to the @code{guix shell} command
 to run the tests that require internet access.
 
+Another option is to use the @option{-m} (short for @option{--manifest})
+and the @file{manifest.scm} provided in the Guix repository.
+
+@example
+guix shell --pure -m manifest.scm
+@end example
+
+Here, we recommend the @option{--pure} to let Guix reset all your
+environment variables. This solves an issue where on some systems, the
+version of Guile cannot be inferred from its install path and causes the
+configuration to fail. It should also solve the @code{aclocal} issue
+described below.
+
 If you are unable to use Guix when building Guix from a checkout, the
 following are the required packages in addition to those mentioned in the
 installation instructions (@pxref{Requirements}).
diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
index c485df7740f..d07e0788bc6 100644
--- a/gnu/packages/rocq.scm
+++ b/gnu/packages/rocq.scm
@@ -29,11 +29,14 @@
   #:use-module (guix gexp)
   #:use-module (guix git-download)  
   #:use-module (guix licenses)
-  #:use-module (guix packages))
+  #:use-module (guix packages)
+  #:use-module (srfi srfi-207)
+  #:use-module (guix base32))
 
+;; 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") ;; not changed as of V9.2.0.
+(define rocqide-server-pkg "coqide-server")
 
 (define (rocq-build-phases packages-to-install)
   ;; Run "make help-install" in rocq to see instructions for "final users".
@@ -52,8 +55,9 @@
 	(replace 'build
 	  (lambda _ (invoke "dune" "build" "-p"
 			    (string-join '#$all-packages ","))))
-	(replace 'check
-	  (lambda _ (invoke "dune" "build" "@check")))
+        (replace 'check (lambda* (#:key tests? #:allow-other-keys)
+                          (if tests?
+                              (invoke "dune" "build" "@check"))))
 	(replace 'install
 	  (lambda* (#:key outputs #:allow-other-keys)
 	    (let* ((out (assoc-ref outputs "out"))
@@ -68,14 +72,17 @@
     (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))
+       (method url-fetch)
+       (uri (string-join `("https://github.com"
+                           "rocq-prover/rocq/releases/download"
+                           ,(string-append "V" version)
+                           ,(string-append "rocq-" version ".tar.gz")) "/"))
+       ;; using sha256 hex published on github release
        (sha256
-        (base32
-         "1rxq2cfqlbp8vzygmk6cwszbsn5l2vka0syhrafrnpn2rpyivya9"))))
+        (let* ((hex
+                "a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20")
+               (bv (hex-string->bytevector hex)))
+          (base32 (bytevector->nix-base32-string bv))))))
     (native-search-paths
      (list (search-path-specification
             (variable "ROCQPATH")
@@ -83,21 +90,18 @@
     (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
+      #: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 
+     "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+.
@@ -107,6 +111,10 @@ development of machine-checked proofs.")
   (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))))))
@@ -115,6 +123,10 @@ development of machine-checked proofs.")
   (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))))))
diff --git a/manifest.scm b/manifest.scm
index 681749a9f41..3938802ef12 100644
--- a/manifest.scm
+++ b/manifest.scm
@@ -35,6 +35,9 @@
                              (replace "graphviz"
                                (specification->package "graphviz")))))))
 
+       ;; For graphviz. (building service-graph.png)
+       (specifications->manifest (list "fontconfig"))
+
        ;; Extra packages used by unit tests.
        (specifications->manifest (list "gnupg"))
 
diff --git a/patch-checklist.bash b/patch-checklist.bash
new file mode 100644
index 00000000000..be2d83ec1bf
--- /dev/null
+++ b/patch-checklist.bash
@@ -0,0 +1,67 @@
+# Script to run through package checklist
+# (ideally a part of CI for new PRs)
+
+while getopts :p: OPT; do
+    case $OPT in
+	p|+p)
+	    PACKAGE=$OPTARG
+	    ;;
+	*)
+	    echo "usage: ${0##*/} [+-p ARG} [--] ARGS..."
+	    exit 2
+    esac
+done
+shift $(( OPTIND - 1 ))
+OPTIND=1
+
+if [ ! $PACKAGE ]
+then
+    echo "Specify a package to test with -p"
+    exit 1
+fi
+
+DEVGUIX="./pre-inst-env guix"
+
+# 1. Check the cryptographic signature
+# (use the hash and link maintainers provide in the build)
+
+# 2. Take time to edit synopsis
+
+# 3. Lint
+$DEVGUIX lint $PACKAGE
+
+# 4. Style
+$DEVGUIX style $PACKAGE
+
+# 5. Build
+$DEVGUIX build $PACKAGE
+
+# 6. Build dependents
+$DEVGUIX build --dependents=1 $PACKAGE
+
+# 7. Check package does not install bundled copies of software
+
+# 8. Check size (avoid texlive)
+$DEVGUIX size $PACKAGE
+
+# 9. Check dependent packages are not affected
+$DEVGUIX refresh --list-dependent $PACKAGE
+
+# 10. Check if build is deterministic
+$DEVGUIX build --rounds=2 --check $PACKAGE
+
+# 11. Gender neutral wording.
+
+# 12. Make sure your patch only contains related changes.
+
+# 13. Style (repeated)
+
+# 14. Use mirrors of github repos: don't use GitHub archives.
+
+# 15. Check if Guix builds (see building from Git)
+autoreconf -vif
+./configure
+make -j 4
+
+# 16. Run a guix pull
+$DEVGUIX pull --url=$PWD --profile=/tmp/guix.temp --disable-authentication