diff options
Diffstat (limited to 'gnu/packages')
| -rw-r--r-- | gnu/packages/rocq.scm | 144 |
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+))) |