Proposal to move CoqdocJS or a fork to coq-community

[palmskog]

Project name: CoqdocJS

Initial author(s): Tobias Tebbi (@tebbi)

Current URL: https://github.com/tebbi/coqdocjs https://github.com/palmskog/coqdocjs

Kind: collection of JavaScript and CSS code

License: BSD

Description: CoqdocJS is a collection of scripts to improve the HTML output of the coqdoc tool, adding features such as hiding/showing proof scripts on command.

Status: unknown

New maintainer: @palmskog

I have recently forked CoqdocJS and heavily modified it to fit the workflow of typical projects in coq-community, such as leveraging GitHub pages for deploying HTML. The results can be seen, e.g., for the Huffman project. However, the core JavaScript and CSS is roughly the same.

Many of these changes are not likely to be useful outside of coq-community or a similar organization. Hence, I am looking for feedback from the community as to whether to move my fork of CoqdocJS to the coq-community organization on GitHub, or determine whether we can move the original CoqdocJS repo to coq-community.

@tebbi can you comment on what your plans w.r.t. CoqdocJS are for the longer term, e.g., whether you plan to actively maintain it and if you think it may be a good idea to have the community help maintain it by moving the repo?

If it is determined that maintaining a fork is the best way to go, I would be happy to rename the fork to avoid confusion.

[tebbi]

I no longer work with Coq, so I'm the wrong person to keep maintaining CoqdocJS. Do your changes to CoqdocJS make it less useful outside of coq-community?

[tebbi]

Adding some users and contributors of CoqdocJS: @fakusb @chdoc @yforster @tchajed @Lysxia @HuStmpHrrr

[chdoc]

Hi, thanks for bringing this to my attention. I haven't had the time yet to look at the changes @palmskog made. As a user (and marginal contributor), I am very much in favor of this being actively maintained and I suppose that coq-community is a decent place for this.

However, care should be taken that CoqDocJS continues to fulfill its users needs. That is, it should be useful both for GitHub integrated projects and those that have their own websites. Also, in the long run, I don't think a single CoqDocJS tool can survive without some (easy) way to customize. For instance, there is still issue #8 which turned into a debate on how to balance the wish to ensure that inexperienced reviewers do not miss the code folding feature and maintaining a clean display for ones own use. So, implementing a few options might help to keep CoqDocJS from fragmenting to the point where technical improvements no longer reach the users (because everyone has his own fork of some state)

[palmskog]

@chdoc @tebbi the key changes I made in my fork is introducing quite strict assumptions on how the workflow is supposed to work: the non-coqdoc-generated .js, .css, .html assets live in the resources directory and are copied with the coqdoc output to the docs directory. However, the core CSS and JavaScript is essentially unchanged, and the small changes to the core could be quite easily integrated upstream. So to some extent the fork is not as easy to use for projects that want to use a non-GitHub workflow.

If we indeed decide to transfer @tebbi's repository to coq-community, the best way to maintain the workflow-opinionated parts may be in a separate branch, but I'm open to suggestions.

[chdoc]

I'm all in favor of a more strict workflow, in particular if it eases usage. I had a quick look at your fork and the workflow described there, and I have three remarks:

• I like the Makefile.coq.local approach, seems easy to use and reasonably portable
• I'm doubtful about copying the resources folder. I usually add CoqDocJS as a submodule, so that the project can easily profit from improvements to CoqDocJS.
• Proofs look broken for me.

[liyishuai]

I'd also prefer submodule to copying folder. Is there a configuration in _CoqProject to include coqdocjs/Makefile.coq.local in Makefile.coq? That'll make the workflow more automated. Otherwise, we could include it in Makefile.

[palmskog]

@liyishuai I would prefer to stay completely agnostic to git submodules, since I don't (ever want to) use them myself. The recent changes to the CoqdocJS fork should address the above concerns and reported bugs. The key for me is to keep the possibility open for simply copying over files into the repo.

@chdoc in order to ensure wide usability of CoqdocJS inside and outside Coq-community, maybe the two of us could co-maintain @tebbi's repo (assuming he agrees to transfer it to this organization)?

On the other hand, if there is no invested co-maintainer in the near future to vet master-targeted changes for wider use, I think I will carry on working in the fork, and rename it.

[chdoc]

I believe that usage/adoption of CoqDocJS will be aided by avoiding a forest of forks, and I'm willing to help maintain it, if Tobias wants to relinquish his control of the project.

As it comes to the submodule vs copying workflow, this might be as simple as making it the default copying workflow to put the CoqDocJS files into a folder named (for example) coqdocjs, i.e., adding one level of folder structure to align it with the directory normally generated by the submodule checkout.

[palmskog]

@chdoc great, I have invited @tebbi to join the coq-community organization to allow him to transfer the repo easily, should he agree with this plan. I will invite you also once the repo is transferred.

[liyishuai]

@palmskog are you planning to update your fork to make the workflow compatible with both submodule and copying? as @chdoc describes:

As it comes to the submodule vs copying workflow, this might be as simple as making it the default copying workflow to put the CoqDocJS files into a folder named (for example) coqdocjs, i.e., adding one level of folder structure to align it with the directory normally generated by the submodule checkout.

[palmskog]

@liyishuai right now I'm waiting for greenlighting from @tebbi and his potential transfer of the repo to the coq-community organization. If the transfer takes place, I would expect to first add my separate coq-community branch without explicit submodule support and then do PRs against master vetted by @chdoc.

[tebbi]

I agree with the plan going forward; I just transferred the repo.

[palmskog]

Thanks for everyone's input, let's continue any discussion as CoqdocJS issues and PRs. I've invited @chdoc to join the organization.