To update:
I have managed to make some headway.
Here is is my package definition so far:
https://git.sr.ht/~indieterminacy/5q60nq-oq_packaging-ocaml/tree/fc8c91732dde9856c9624384889a66b8a5f7b2fa/item/jw-oq_ocaml.scm
I intend to package the Iris derived framework, Katamaran:
https://github.com/katamaran-project/katamaran/
https://git.sr.ht/~indieterminacy/5q60nq-oq_packaging-ocaml/tree/fc8c91732dde9856c9624384889a66b8a5f7b2fa/item/jw-oq_ocaml.scm#L1239
This is still not reconciled, with some of the points to be resolved
documented here:
https://git.sr.ht/~indieterminacy/2q50rqr-oq_kanbans-katamaran/commit/cb10ddc481279737bb665c3ed9e860c69493c614
I have managed to package the supporting inputs, which includes a modern
Coq version (I did have success with Rocq but its not included in that
package atm) and a package definition for Iris (I realise there are
duplicate definitions in this version writing this, I should swipe the
first definition - I hope my concerns are well described in any case):
https://git.sr.ht/~indieterminacy/5q60nq-oq_packaging-ocaml/tree/fc8c91732dde9856c9624384889a66b8a5f7b2fa/item/jw-oq_ocaml.scm#L1011
To supplement, I have updated the definition for ProofGeneral (which
equally was lacklustre regarding updates).
I have been experiencing difficulties getting Prooftree (a supplement to
ProofGeneral):
https://git.sr.ht/~indieterminacy/5q60nq-oq_packaging-ocaml/tree/fc8c91732dde9856c9624384889a66b8a5f7b2fa/item/jw-oq_ocaml.scm#L922
I suspect there is a flaw with my packaging of one of the main
dependencies, lablgtk2:
https://git.sr.ht/~indieterminacy/5q60nq-oq_packaging-ocaml/tree/fc8c91732dde9856c9624384889a66b8a5f7b2fa/item/jw-oq_ocaml.scm#L869
There is a version 3 that works - I tried upgrading lablgtk2 to 3 and
then upgrading Prooftree to version 3.
Id benefit from some help to wrap this up for some activity.
Anybody able to help resolve this?
Kind regards,
Jonathan
On 2026-03-20 18:45, indieterminacy wrote:
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 install
Error: 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
