proviola

[Zimmi48]

Move a project to coq-community

Project name: proviola

Initial author(s): Carst Tankink @Carst-Tankink

Current URL: https://bitbucket.org/Carst/proviola-source

Kind: tool

License: GPL v3

Description: A tool to be able to replay the proofs when browsing a coqdoc-generated HTML file.

Status: Not maintained.

New maintainer: looking for a volunteer

cc @JasonGross @mgrabovsky @yforster who have shown interest by having a fork on GitHub and @spitters @aa755 @siddharthist who have shown interest otherwise.

For those of you that do not already know about coq-community, have a look at the README at https://github.com/coq-community/manifesto. And sorry for the noise if you do not feel concerned (you can easily unsubscribe from this issue).

[langston-barrett]

Could this functionality be integrated into coqdoc?

[Zimmi48]

Apart from the licensing issues, this could be an alternative solution. That being said, coqdoc itself is hardly maintained these days.

[spitters]

Aside, Agda seems to have pretty good tools for documentationÆ https://agda.readthedocs.io/en/v2.5.4.1/tools/literate-programming.html

[spitters]

The SF project has some additions to the coqdoc program. Maybe those can be integrated in the main branch?

[Carst-Tankink]

About those licensing issues: I can't remember if I picked GPLv3 for a particular reason. If there is no reason for it to remain under it (and I doubt it because I'm not redistributing any GPL-licensed dependencies), I'm happy to relicense it to a compatible license.

(I do not have the time to do any active development on Proviola, but am happy to share knowledge if you find a maintainer)

[JasonGross]

I've also been doing a bit of development on proviola at https://github.com/JasonGross/proviola-source (mainly for HoTT, which continues to use it, and occasionally runs into issues)

[Zimmi48]

@JasonGross Do you want to maintain this within coq-community? A convergence between various coqdoc-related tools, and in particular js-extensions (like coqdocjs and proviola) would be great but does not have to happen first. It could be a later step if someone is up for the task.

[yforster]

Regarding this later step, I once managed to create html files with both coqdocjs and proviola for a project and tried to write down what I did: https://gist.github.com/yforster/e7d73135aea3ef5e39e1e7272e53e568

I probably won't have time to continue on this, but maybe it can help for somebody who wants to continue at some point.

[JasonGross]

@Zimmi48 I will not have much time to devote to maintaining this, but I'm willing to be a maintainer. (Ideally a co-maintainer, but I'm also willing to be sole maintainer.)

[palmskog]

@JasonGross great to hear about you assuming maintainership. If I might add a bit to this burden in the interest of the community: since there is a rich Mercurial commit history for Proviola in the BitBucket repo, could you try to import this to GitHub and add your changes on top? Note that BitBucket is killing off Mercurial support in just a few months, and will simply delete all Mercurial repositories.

For example, you could try to use the GitHub importer: https://help.github.com/en/github/importing-your-projects-to-github/about-github-importer

[palmskog]

Just in time before the disappearance of all Bitbucket Mercurial-based repositories, the Proviola code and issues have been migrated to a GitHub repository in coq-community, with @JasonGross assigned as the maintainer. Hence, I'm closing this issue.