blob: 5874a8228f204898583ee5ff1d541cca94a42596 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(define-module (gnu packages rocq)
#:use-module (gnu packages autotools)
#: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)
#:use-module (guix git-download)
#: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+)))
|
