Emilio Jesús Gallego Arias

I was expecting to get back to this next week, mainly just to set the Coq environment and port a few examples. Indeed we must use Coq's math-comp analysis library,...

> What is wrong with simply doing the translation of all the theorems by hand and crowdsourcing it (divide and conquer)? Nothing is wrong, tho it requires people to learn...

Hi @ozross , thanks a lot for quick reply! Indeed, it is possible to manually workaround this problem, however, when developing a paper, this becomes very costly as any change...

Thanks for analysis @palmskog ; we will implement implicit transitive theory deps for 0.9. I'd like to note however that implicit transitive dependencies are not inmune to breakage, they suffer...

> However, in my experience the ghost dependency "underdependency" problem is less serious than "overdepending" and requires less manual intervention. Interesting, how it is more serious / requires more intervertion,...

> In Coq-community, we have seen underdependency issues related to MathComp, e.g., a package only depending on coq-mathcomp-algebra when it should also depend on coq-mathcomp-fingroup. I'm not sure I follow,...

If you mean the other case, I'm afraid you'd have to patch the source code too, if algebra drop the dep on fingroup dune, even if it has transitive deps,...

> However, all I'd need to do is edit the coq-baz package definition to include coq-mathcomp-fingroup and it should build again. Not in the Dune model, right? You'd need to...

Yes, finally time to transfer it and complete the documentation. Should I just go ahead and do the transfer?

I get an error "You don’t have the permission to create public repositories on coq-community" There are several ways to solve this, I tried to transfer it to you @palmskog...