Hello Ludo,
On 2026-03-30 19:41, Ludovic Courtès wrote:
Coq is already packaged so I'd expect Rocq to be "just" an upgrade
(famous last words)?
Ive probably got the rhythm to resolve it all later (Rocq should be on
this repo at some stage when I have focus).
In any case this is 8.20.1 (I certainly have no time for patches and Coq
suffices for my rig):
https://git.sr.ht/~indieterminacy/5q60nq-oq_packaging-ocaml/tree/2468f2aa9b785c067ea4e3c36a87367b650b97bc/item/jw-oq_ocaml.scm#L96
Fortunately, I did succeeed with Katamaran in any case:
https://git.sr.ht/~indieterminacy/5q60nq-oq_packaging-ocaml/tree/2468f2aa9b785c067ea4e3c36a87367b650b97bc/item/jw-oq_ocaml.scm#L1291
I still need Prooftree resolved (but am focused elsewhere):
https://git.sr.ht/~indieterminacy/5q60nq-oq_packaging-ocaml/tree/2468f2aa9b785c067ea4e3c36a87367b650b97bc/item/jw-oq_ocaml.scm#L922
Its probably the dependency, lablgtk2 confusing things:
https://git.sr.ht/~indieterminacy/5q60nq-oq_packaging-ocaml/tree/2468f2aa9b785c067ea4e3c36a87367b650b97bc/item/jw-oq_ocaml.scm#L869
Tbh, if there is any info/suggestions regarding how to form individual
modules (with manifest) that would work with Katamaran that would be
very helpful for my workflow.
Perhaps I should finally master Arun Isaac's (CWL orientated) tool,
Ravanan:
https://github.com/arunisaac/ravanan
Ludo'.
Kind regards,
Jonathan
