From 5d20910b93da145ff16a811dd50a9fdba33fa27d Mon Sep 17 00:00:00 2001 From: Dan Rostovtsev Date: Tue, 7 Apr 2026 18:36:12 -0400 Subject: 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 --- RocqExample.v | 4 ++ gnu/packages/rocq.scm | 111 +++++++++++++++++++++++++++++++------------------- test-rocq.bash | 25 ++++++++++++ 3 files changed, 98 insertions(+), 42 deletions(-) create mode 100644 RocqExample.v create mode 100644 test-rocq.bash 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 -- cgit v1.3