Hello all, Ive made some progress updating Coq to Rocq.
Similarly, Ive managed to package Iris (version 4-3.0)(with props to Antero Mejr for submitting a (uncommitted?) patch for a previous version:
https://yhetil.org/guix-patches/[email protected]/) However, Im having problems installing Katamaran (which is my priority): https://github.com/katamaran-project/katamaran I get this feedback regarding the failed building: ```Error: The package rocq-core does not have any user defined stanzas attached to it. If this is intentional, add (allow_empty) to the package definition in
the dune-project file -> required by _build/default/rocq-core.install -> required by alias installError: The package rocq-test-suite does not have any user defined stanzas
attached to it. If this is intentional, add (allow_empty) to the package definition in the dune-project file -> required by _build/default/rocq-test-suite.install -> required by alias install(cd _build/default && /gnu/store/k66i68s5l93n1lgxp29vn2292nsywp1v-bash-minimal-5.2.37/bin/bash -e -u -o pipefail -c dev/tools/make_git_revision.sh) > _build/default/revision
skipping make_git_revision: git dir not found error: in phase 'build': uncaught exception:%exception #<&invoke-error program: "dune" arguments: ("build" "@install" "--release") exit-status: 1 term-signal: #f stop-signal: #f>
phase `build' failed after 57.9 seconds command "dune" "build" "@install" "--release" failed with status 1 ```I recognise it is expecting rocq-core (which I perceive as a subset of rocq). However, my under developed attempt to package rocq-core separately has not been successful. I could try to strip back the rocq which worked but Im worried about burning more time this week.
As somebody trying to experiment with Coq, Im not sure how to interpret such details about stanzas.
Finally, the failed attempt to resolve the issues with make_git_revision.sh have been unsuccessful (either Im missing a trick with Dune's plumbing or else Im lacking a bit of GuixFOO).
Attached is my WIP file and a recent log from rocq-runtime (apologies for the clutter).
Anybody able to resolve this (soonish, if possible)? Kind regards, Jonathan
;; ~/6q50oqo-nq_operating-systems/oq_guix/guix/gnu/packages
(define-module (kay packages coqu)
#:use-module (gnu packages)
#:use-module (gnu packages autotools)
#:use-module (gnu packages base)
#:use-module (gnu packages bison)
#:use-module (gnu packages boost)
#:use-module (gnu packages compression)
#:use-module (gnu packages coq)
#:use-module (gnu packages emacs)
#:use-module (gnu packages flex)
#:use-module (gnu packages gawk)
#:use-module (gnu packages gnome) ;
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ocaml)
#:use-module (gnu packages perl)
#:use-module (gnu packages python)
#:use-module (gnu packages python-xyz) ;
#:use-module (gnu packages rsync)
#:use-module (gnu packages tex) ;
#:use-module (gnu packages texinfo)
#:use-module (gnu packages m4) ;
#:use-module (gnu packages version-control) ;
#:use-module (gnu packages pkg-config) ;
#:use-module (guix build-system ocaml) ;
#:use-module (guix build-system dune)
#:use-module (guix build-system gnu)
#:use-module (guix build-system texlive) ;
#:use-module (gnu packages emacs) ;
#:use-module (guix build-system trivial)
#:use-module (guix download)
#:use-module (guix gexp)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
#:use-module (guix packages)
#:use-module (guix utils)
#:use-module ((srfi srfi-1) #:hide (zip)))
(define-public rocq
(package
(name "rocq")
(version "9.1.1")
(source
(origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/rocq-prover/rocq";)
(commit (string-append "V" version))))
(file-name (git-file-name name version))
(sha256
(base32
"0ndmpyrbzl3vb5n729l1ac01gm3gaxglmi5s2j4xa0az3b76025f"))
(snippet
#~(begin
(use-modules (guix build utils))
(substitute* "./dev/ci/scripts/ci-waterproof.sh"
(("#!/usr/bin/env/") "#!/usr/bin/env"))))))
(native-search-paths
(list (search-path-specification
(variable "ROCQPATH")
(files (list "lib/rocq/user-contrib")))))
(build-system dune-build-system)
(arguments
(list
#:package "rocq-runtime,coq-core,rocq-core"
#~(modify-phases %standard-phases
(add-before 'build 'set-home-env
(lambda _
;; No such file or directory: '/homeless-shelter/....'
(setenv "HOME" "/tmp")))
(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 'install
(lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out"))
(libdir (string-append out "/lib/ocaml/site-lib")))
(invoke "dune"
"install"
"--prefix" out "rocq-runtime" "coq-core"
"rocq-core")))))))
(propagated-inputs
(list ocaml-zarith))
(inputs
(list gmp))
(native-inputs
(list ocaml-ounit2 which))
(properties '((upstream-name . "coq"))) ; also for inherited packages
(home-page "https://coq.inria.fr";)
(synopsis "Proof assistant for higher-order logic")
(description
"Rocq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
specification.
It is developed using Objective Caml and Camlp5.")
;; The source code is distributed under lgpl2.1.
;; Some of the documentation is distributed under opl1.0+.
(license (list license:lgpl2.1 license:opl1.0+))))
(define-public ocaml-rocq-runtime
(package
(name "rocq-runtime")
(version "9.1.1")
(source
(origin
(method url-fetch)
;; (method git-fetch)
(uri
;; (git-reference
;; (url
;; "https://github.com/rocq-prover/rocq";)
;;))
;;(commit version)))
;; (commit (string-append "V" version))))
;; (file-name (git-file-name name version))
"https://github.com/rocq-prover/rocq/releases/download/V9.1.1/rocq-9.1.1.tar.gz";)
(sha256
(base32 "0nc726z86jzzdng2l902iyxc2af1wm006681rqf9p5lk87y07k9m"))
;; (patches (local-file (search-patch "0001-jz-rqr_remove-test.patch")))
(snippet
#~(begin
(use-modules (guix build utils))
;; (mkdir-p "/homeless-shelter/.cache/dune/db/temp")
(substitute* "./dev/ci/scripts/ci-waterproof.sh"
(("#!/usr/bin/env/") "#!/usr/bin/env"))
;; ))))
(substitute* "./doc/tools/coqrst/notations/fontsupport.py"
;; (substitute*
"./doc/tools/coqrst/notations/fontsupport.py"
(("#!/usr/bin/env/ python2") "#!/usr/bin/env python3"))
;; (delete-file "dev/tools/make_git_revision.sh")
;; (delete-file "_build/default/dev/tools/make_git_revision.sh")
))))
(build-system dune-build-system)
(arguments
(list
;; #:tests? #f
#:phases
'(modify-phases %standard-phases
(add-before 'build 'set-home-env
(lambda _
;; No such file or directory: '/homeless-shelter/....'
(setenv "HOME" "/tmp")))
(add-after 'unpack 'fix-race
(lambda _
;; ;; There's a race between bng.o and bng_generic.c. Both depend
on
;; ;; the architecture specific bng.c, but only the latter declares
;; ;; the dependency.
(mkdir-p "_build/default/src")
(for-each
(lambda (f)
(copy-file f (string-append "_build/default/" f)))
(find-files "src" "bng_.*\\.c"))))
)))
(inputs (list git))
(native-inputs
(list perl
git
pkg-config))
(propagated-inputs
(list ocaml-zarith
;; glibc
;; glibc-bootstrap
;; gcc-toolchain
;; linux-libc-dev
ocaml-lablgtk3-sourceview3
python
;; python2
;; python3
ocaml-odoc
ocaml-yojson
git
camlzip
gmp))
(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.
Typical applications include the certification of properties of
programming
languages (e.g. the @code{CompCert} compiler certification project,
or the Bedrock verified low-level programming library), the formalization
of mathematics (e.g. the full formalization of the Feit-Thompson theorem
or homotopy type theory) and teaching.
This package includes the Rocq Prover core binaries, plugins, and tools,
but not the vernacular standard library. Note that in this setup,
Rocq needs to be started with the -boot and -noinit options, as will
otherwise fail to find the regular Rocq prelude, now living in the
rocq-core
package.")
(license license:lgpl2.1)))
(define-public ocaml-findlib
(package
(name "ocaml-findlib")
(version "1.9.8")
(source
(origin
(method url-fetch)
(uri
"https://github.com/ocaml/ocamlfind/archive/refs/tags/findlib-1.9.8.tar.gz";)
(sha256
(base32 "1783rrlqfjgz0gx4iihkbl3i1qwlipwg7wwsg837zxmbrhsrk2fn"))))
;; (build-system ocaml-build-system)
(build-system gnu-build-system)
(native-inputs
(list m4
ocaml))
(arguments
`(#:tests? #f ; no test suite
#:parallel-build? #f
#:make-flags
(list "all"
"opt")
#:phases
(modify-phases %standard-phases
(replace
'configure
(lambda* (#:key inputs outputs #:allow-other-keys)
(let ((out (assoc-ref outputs "out")))
(invoke
"./configure"
"-bindir" (string-append out "/bin")
"-config" (string-append out "/etc/ocamfind.conf")
"-mandir" (string-append out "/share/man")
"-sitelib" (string-append out "/lib/ocaml/site-lib")
"-with-toolbox"))))
(replace 'install
(lambda* (#:key outputs #:allow-other-keys)
(let ((out (assoc-ref outputs "out")))
(invoke "make" "install"
(string-append "OCAML_CORE_STDLIB="
out "/lib/ocaml/site-lib"))))))))
(properties
`((upstream-name . "ocamlfind")))
(home-page "http://projects.camlcity.org/projects/findlib.html";)
(synopsis "A library manager for OCaml")
(description
"Findlib is a library manager for OCaml. It provides a convention how to
store
libraries, and a file format (\"META\") to describe the properties of
libraries.
There is also a tool (ocamlfind) for interpreting the META files, so that
it is
very easy to use libraries in programs and scripts.")
(license license:expat)))
(define-public ocaml-coqide-server
(package
(name "ocaml-coqide-server")
(version "9.1.1")
(source
(origin
(method url-fetch)
(uri
"https://github.com/rocq-prover/rocq/releases/download/V9.1.1/rocq-9.1.1.tar.gz";)
(sha256
(base32 "0nc726z86jzzdng2l902iyxc2af1wm006681rqf9p5lk87y07k9m"))))
(build-system dune-build-system)
(propagated-inputs
(list ocaml-rocq-runtime
ocaml-odoc))
(home-page "https://rocq-prover.org/";)
(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](https://github.com/rocq-prover/rocq/blob/master/dev/doc/xml-protocol.md)
which allows clients, such as @code{RocqIDE}, to interact with the Rocq
Prover
in a structured way.")
(license license:lgpl2.1)))
(define-public ocaml-rocqide
(package
(name "ocaml-rocqide")
(version "9.1.1")
(source
(origin
(method url-fetch)
(uri
"https://github.com/rocq-prover/rocq/releases/download/V9.1.1/rocq-9.1.1.tar.gz";)
(sha256
(base32 "0nc726z86jzzdng2l902iyxc2af1wm006681rqf9p5lk87y07k9m"))))
(build-system dune-build-system)
(propagated-inputs
(list adwaita-icon-theme
ocaml-coqide-server
ocaml-cairo2
ocaml-lablgtk3-sourceview3
ocaml-odoc))
(native-inputs
(list ocaml-findlib findutils))
(home-page "https://rocq-prover.org/";)
(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. This package provides the
@code{RocqIDE}, a graphical user interface for the development of
interactive
proofs.")
(license license:lgpl2.1)))
(define-public coq-stdpp
(package
(name "coq-stdpp")
(version "1.12.0")
(synopsis "Alternative Coq standard library std++")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://gitlab.mpi-sws.org/iris/stdpp.git";)
(commit (string-append "coq-stdpp-" version))))
(file-name (git-file-name name version))
(sha256
(base32
"118h3kf7g4il39ydx4srsvc7w6dz53893sfpqa3v4plv88r1i3ys"))))
;; "0lnvdfn4qq2lyabiq4ikb5ya46f4jp59dynyprnhki0ay9xagz3d"))))
(build-system gnu-build-system)
(inputs
(list coq))
(arguments
`(#:tests? #f ; Tests are executed during build phase.
#:make-flags
(list (string-append "COQLIBINSTALL="
(assoc-ref %outputs "out")
"/lib/coq/user-contrib"))
#:phases
(modify-phases %standard-phases
(delete 'configure))))
(description
"This project contains an extended \"Standard Library\" for Coq called
coq-std++.
The key features are:
@itemize
@item Great number of definitions and lemmas for common data structures
such
as lists, finite maps, finite sets, and finite multisets.
@item Type classes for common notations (like â
, âª, and
Haskell-style monad
notations) so that these can be overloaded for different data
structures.
@item It uses type classes to keep track of common properties of types,
like
it having decidable equality or being countable or finite.
@item Most data structures are represented in canonical ways so that
Leibniz
equality can be used as much as possible (for example, for maps we have
m1 =
m2 iff â i, m1 !! i = m2 !! i). On top of that, the library provides
setoid
instances for most types and operations.
@item Various tactics for common tasks, like an ssreflect inspired done
tactic
for finishing trivial goals, a simple breadth-first solver
naive_solver, an
equality simplifier simplify_eq, a solver solve_proper for proving
compatibility of functions with respect to relations, and a solver
set_solver
for goals involving set operations.
@item The library is dependency- and axiom-free.
@end itemize")
(home-page "https://gitlab.mpi-sws.org/iris/stdpp";)
(license license:bsd-3)))
;; https://yhetil.org/guix-patches/[email protected]/
;; original +
"1wr1jigzgl4fajl5jv4lanmb8nk4k6wdakakmxhfp5drxwhqgs0y"))))
;; 1yz8f9l8cxg3g9c0zcmchymnq8q0hasvj0gh9wmx15rfhq4bbf49
;; katamaran needs version 4.3
;;
https://gitlab.mpi-sws.org/iris/iris/-/commit/3d176f124f708e7325a362722c3d2b3957e3675d
;; expected hash: 1wr1jigzgl4fajl5jv4lanmb8nk4k6wdakakmxhfp5drxwhqgs0y
;;actual hash: 0n83m8hhynyk2kzzjw8jpkps8xz49gr1aarzghvp40ryaa467a6y
;; features in uncommitted patch
(define-public coq-iris
(package
(name "coq-iris")
(version "4.3.0")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://gitlab.mpi-sws.org/iris/iris.git/";)
(commit (string-append "iris-" version))))
(file-name (git-file-name name version))
(sha256
(base32
"0n83m8hhynyk2kzzjw8jpkps8xz49gr1aarzghvp40ryaa467a6y"))
(snippet
#~(begin
(use-modules (guix build utils))
(substitute* "./iris/algebra/ofe.v"
(("_%_OF.") "_%OF."))
(substitute* "./iris/bi/interface.v"
(("_%_stdpp") "_%stdpp"))
(substitute* "./iris/bi/interface.v"
(("_%_I") "_%I"))
(substitute* "./iris/bi/derived_connectives.v"
(("_%_I") "_%I"))
(substitute* "./iris/bi/derived_connectives.v"
(("_%_nat_scope") "_%nat_scope"))
(substitute* "./iris/bi/plainly.v"
(("%_type_scope") "%type_scope"))
(substitute* "./iris/bi/plainly.v"
(("_%_I") "_%I"))
(substitute* "./iris/bi/updates.v"
(("%_bi_scope") "%bi_scope"))
(substitute* "./iris/bi/updates.v"
(("%_type_scope") "%type_scope"))
(substitute* "./iris/bi/embedding.v"
(("_%_I") "_%I"))
(substitute* "./iris/bi/monpred.v"
(("_%_I") "_%I"))
(substitute* "./iris/bi/weakestpre.v"
(("_%_E") "_%E"))
(substitute* "./iris/bi/weakestpre.v"
(("_%_I") "_%I"))
(substitute* "./iris/bi/lib/counterexamples.v"
(("_%_I") "_%I"))
(substitute* "./iris/bi/lib/fractional.v"
(("_%_I") "_%I"))
(substitute* "./iris/bi/lib/fractional.v"
(("_%_Qp.") "_%Qp."))
(substitute* "./iris/bi/lib/laterable.v"
(("_%_I") "_%I"))
(substitute* "./iris/bi/lib/laterable.v"
(("P%_I") "P%I"))
(substitute* "./iris/bi/lib/laterable.v"
(("Q%_I") "Q%I"))
(substitute* "./iris/proofmode/monpred.v"
(("_%_I") "_%I"))
(substitute* "./iris/proofmode/environments.v"
(("Q%_I") "Q%I"))
(substitute* "./iris/proofmode/classes.v"
(("_%_I") "_%I"))
(substitute* "./iris/proofmode/classes.v"
(("_%_type_scope") "_%type_scope"))
(substitute* "./iris/proofmode/classes.v"
(("_%_nat_scope") "_%nat_scope"))
(substitute* "./iris/proofmode/classes.v"
(("_%_type") "_%type"))
(substitute* "./iris/proofmode/classes_make.v"
(("_%_I") "_%I"))
(substitute* "./iris/proofmode/classes_make.v"
(("_%_nat") "_%nat"))
(substitute* "./iris/proofmode/coq_tactics.v"
(("_%_I") "_%I"))
(substitute* "./iris/proofmode/notation.v"
(("_%_proof_scope") "_%proof_scope"))
(substitute* "./iris/proofmode/notation.v"
(("_%_string") "_%string"))
(substitute* "./iris/proofmode/notation.v"
(("_%_I") "_%I"))
(substitute* "./iris_deprecated/base_logic/viewshifts.v"
(("_%_I") "%I"))
;; (substitute* "./iris/tex/Makefile"
;; (("latexmk iris") "pdflatex iris"))
(delete-file "tex/Makefile")
))
))
(build-system gnu-build-system)
(arguments
(list #:parallel-build? #f ; non-deterministic failures
#:tests? #f ; 3 proof failures, appears formatting-related
#:test-target "test"
#:make-flags
#~(list (string-append "COQLIBINSTALL="
#$output
"/lib/coq/user-contrib")
;; Coq interleaves tests into the build.
;; Work around this in the check phase.
"NO_TEST=1"
;; Load mappings from _CoqProject into coqtop
;; TODO: can this be automated?
"COQTOP=coqtop -Q iris/prelude iris.prelude \
-Q iris/algebra iris.algebra \
-Q iris/si_logic iris.si_logic \
-Q iris/bi iris.bi \
-Q iris/proofmode iris.proofmode \
-Q iris/base_logic iris.base_logic \
-Q iris/program_logic iris.program_logic \
-Q iris_heap_lang iris.heap_lang \
-Q iris_unstable iris.unstable \
-Q iris_deprecated iris.deprecated")
#:phases
#~(modify-phases %standard-phases
(delete 'configure)
(add-before 'build 'change-home-dir
(lambda _
;; No such file or directory: '/homeless-shelter/....'
(setenv "HOME" "/tmp")))
;;> rqr-xwx add-build-for-documentation
;; (add-after 'build 'build-doc
;; (lambda _
;; (with-directory-excursion "tex"
;; (invoke "make" "all"))))
(replace 'check
(lambda*
(#:key tests? test-target parallel-build?
make-flags #:allow-other-keys)
(when tests?
(apply invoke "make"
"-f" "Makefile.coq.local"
"-j" (number->string
(if parallel-build?
(parallel-job-count)
1))
test-target make-flags))))
;;> rqr-xwx add-build-for-documentation
;; (add-after 'install 'install-doc
;; (lambda _
;; (install-file
;; "tex/iris.pdf"
;; (string-append #$output
;; "/share/doc/iris/iris.pdf"))))
)))
(native-inputs ;;
;;(list (texlive-updmap.cfg
(list texlive-amsfonts
texlive-amsmath
texlive-babel
texlive-biber
texlive-biblatex
texlive-csquotes
texlive-dashbox
texlive-enumitem
texlive-faktor
texlive-geometry
texlive-hyperref
texlive-ifmtarg
texlive-latexmk
texlive-marvosym
texlive-mathpartir
texlive-mathtools
texlive-microtype
texlive-pgf
texlive-scalerel
texlive-semantic
texlive-stmaryrd
texlive-tabbing
texlive-tensor
texlive-xcolor
texlive-xifthen))
(propagated-inputs
(list coq
python
coq-stdpp
;; pdflatex
rubber
texlive-scheme-basic
texlive-scripts
))
(home-page "https://iris-project.org/";)
(synopsis "Concurrent separation logic library for Coq")
(description
"This package provides a higher-order concurrent separation logic
library, implemented and verified in the Coq proof assistant.
It is used for reasoning about safety of concurrent programs,
as the logic in logical relations, and to reason about type-systems,
data-abstraction, etc.")
(license license:bsd-3)))
(define-public ocaml-rocq-core
(package
(name "rocq-core")
(version "9.1.1")
(source
(origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/rocq-prover/rocq";)
(commit (string-append "V" version))))
(file-name (git-file-name name version))
(sha256
(base32
;; (source
;; (origin
;; (method url-fetch)
;; (uri
;;
"https://github.com/rocq-prover/rocq/releases/download/V9.1.1/rocq-9.1.1.tar.gz";)
;; (sha256
;; (base32
"0ndmpyrbzl3vb5n729l1ac01gm3gaxglmi5s2j4xa0az3b76025f"))
;; "0nc726z86jzzdng2l902iyxc2af1wm006681rqf9p5lk87y07k9m"))))
(snippet
#~(begin
(use-modules (guix build utils))
;; (mkdir-p "/homeless-shelter/.cache/dune/db/temp")
(substitute* "./dev/ci/scripts/ci-waterproof.sh"
(("#!/usr/bin/env/") "#!/usr/bin/env"))
;; ))))
(substitute* "./rocq-core.opam"
(("\"@runtest\" {with-test}") ""))
))))
(build-system dune-build-system)
(propagated-inputs
(list ocaml-rocq-runtime
ocaml-findlib
ocaml-odoc
;; git
))
(home-page "https://rocq-prover.org/";)
(synopsis "The Rocq Prover with its prelude")
(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. Typical applications include the
certification of properties of programming languages (e.g. the
@code{CompCert}
compiler certification project, or the Bedrock verified low-level
programming
library), the formalization of mathematics (e.g. the full formalization
of the
Feit-Thompson theorem or homotopy type theory) and teaching. 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.")
(license license:lgpl2.1)))
(define-public ocaml-rocq-stdlib
(package
(name "ocaml-rocq-stdlib")
(version "9.0.0")
(source
(origin
(method url-fetch)
(uri
"https://github.com/coq/stdlib/releases/download/V9.0.0/stdlib-9.0.0.tar.gz";)
(sha256
(base32 "04f7xswsl4lbg9kr6zw3v8y65xaglphvl14nj3f1srgw5p2avdhs"))))
(build-system ocaml-build-system)
(propagated-inputs
(list ocaml-rocq-runtime
ocaml-rocq-core))
(home-page "https://rocq-prover.org";)
(synopsis "The Rocq Proof Assistant -- Standard Library")
(description
"Rocq is a formal proof management system. 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.
Typical applications include the certification of properties of programming
languages (e.g. the @code{CompCert} compiler certification project, or the
Bedrock verified low-level programming library), the formalization of
mathematics (e.g. the full formalization of the Feit-Thompson theorem or
homotopy type theory) and teaching. This package includes the Rocq Standard
Library, that is to say, the set of modules usually bound to the Stdlib.*
namespace.")
(license license:lgpl2.1)))
;; https://github.com/katamaran-project/opam-repository.git
;;;;;;; 1n5z52md977mrr5drig78khlsygpq00n4qfcpzix0i10al7jfn0c
; 0vbgi4a7qrhhxmgzav05l80ahwn8b9zlw1nz18zlpyabln2dsw0g
;; coq >= 8.19
;; coq-equations >= 1.3
;; coq-iris >= 4.3
;; coq-stdpp >= 1.11
;; buildFlags = [
;; "COQMAKE_ONE_TIME_FILE=${make-one-time-file}"
;; "pretty-timed"
;; ];
;; propagatedBuildInputs = [
;; coq.ocamlPackages.findlib
;; equations
;; iris
;; stdlib
;; stdpp
;; ];
;; (let ((revision "1")
;; (commit "f9495372801ce4b4dad98ad854203e694c31c1eb"))
;; (package
;; (name "ttyload")
;; (version (git-version "0.5.3" revision commit))
;; (source
;; (origin
;; (method git-fetch)
;; (uri (git-reference
;; (url "https://github.com/lindes/ttyload";)
;; (commit commit)))
;; (file-name (git-file-name name version))
;; (let ((commit "5c25216d3522d6a33e53875cd76a6d65001e4e67"))
;; (package
;; (name "mosaik")
;; (version "2.2.30")
;; (source (origin
;; ;; There are no release tarballs nor tags.
;; (method git-fetch)
;; (uri (git-reference
;; (url "https://github.com/wanpinglee/MOSAIK";)
;; (commit commit)))
;; (file-name (string-append name "-" version))
;; let ((commit "b97c293c812c7ec3cdeccd50a89769e746c01377")
;; (revision "0")
;; (base-version "0.9.6"))
;; (let ((commit "3e9d7d6e9cf8dc33eb29c497c350a1cd7df3a057")
;; (version "5.8.0.129")
;; (revision "0"))
;; (package
;; (inherit mono-5.8.0)
;; (version (git-version version revision commit))
;; (name "mono")
;; (source (origin
;; (method git-fetch)
;; (uri (git-reference
;; (url "https://gitlab.winehq.org/mono/mono.git";)
;; (commit commit)))
;; (file-name (git-file-name name version))
(define-public katamaran
(let ((commit "547725e174f0f6caf654ff2a0640d6ea330848d2")
(revision "1")) ; "0" (version (git-version "1.0" revision
commit))
(package
(name "katamaran")
(version "0.2.0")
(source
(origin
(method git-fetch)
(uri
(git-reference
(url "https://github.com/katamaran-project/katamaran/";)
(commit commit)))
(file-name (git-file-name name version))
(sha256
(base32
"0q1dqqz4vbwy94iadmqjm58k3w4kvsyfl1f4ks5g5qffxkb6r8fj"))))
;; "0vbgi4a7qrhhxmgzav05l80ahwn8b9zlw1nz18zlpyabln2dsw0g"))))
(build-system dune-build-system)
(native-inputs (list pkg-config))
(propagated-inputs
(list ocaml-findlib
coq-equations
coq-iris
;; rocq
ocaml-rocq-stdlib
coq-stdpp))
(home-page "https://katamaran-project.github.io/";)
(synopsis "Separation logic-based verification of instruction sets")
(description
"Katamaran is a verification framework for instruction set architectures
in the
Coq proof assistant. It provides the deeply-embedded language μSail, a
variant
of the [Sail](https://github.com/rems-project/sail) language, for the
specification of instructions sets and provides furthermore facilities for
the
specification of separation logic-based contracts and for
semi-automatically
verifying these contracts. The goal is to formally specify and verify with
machine-checked proofs critical security guarantees of instruction sets.")
(license license:bsd-2))))
;; katamaran
ocaml-rocq-stdlib
;; rocq-core
;; ocaml-rocq-runtime
;; functional
;; ocaml-lablgtk3-sourceview3
;; ocaml-odoc
;; ocaml-yojson
;; camlzip
;; ocaml-findlib
;; rocq
qhjiybyjshf8rskcyq3cyk5svx3qff-rocq-runtime-9.1.1.drv.gz
Description: application/gzip
