Stream: coq-community devs & users

Topic: Migrating Proviola to GitHub


view this post on Zulip Karl Palmskog (Jun 05 2020 at 18:45):

@Jason Gross I'm worried about the Proviola repository on Bitbucket, which is set to disappear in about a month (July 1). You've expressed interest in maintaining this on GitHub. Maybe we could just transfer the repo to GitHub in the coq-community organization as-is very soon and park it there for the time being? Then, if you have enough time later on, we could set up formal maintainership, etc.

view this post on Zulip Karl Palmskog (Jun 05 2020 at 18:47):

I think the circumstances here warrant deviating from our usual process slightly, in particular since this is a valuable tool in use by the community that to my knowledge has no equivalent

view this post on Zulip Karl Palmskog (Jun 05 2020 at 18:49):

ping also @Anton Trunov and @Théo Zimmermann if this OK with you (just parking the repo in the org until a maintainer assumes control)

view this post on Zulip Jason Gross (Jun 05 2020 at 18:51):

@Karl Palmskog sure! Do you want my help doing the migration, or just my approval?

view this post on Zulip Karl Palmskog (Jun 05 2020 at 18:53):

@Jason Gross well, I can do the migration, I just wanted to know if you were still interested in being the maintainer, then we could set up metadata and so on directly if you don't mind

view this post on Zulip Bas Spitters (Jun 05 2020 at 18:54):

Arguably, @Emilio Jesús Gallego Arias jscoq is a pretty good alternative.

view this post on Zulip Jason Gross (Jun 05 2020 at 18:54):

Yeah, sure. I don't have many cycles to spare for maintaining it right now, but I'm down to be maintainer for now

view this post on Zulip Jason Gross (Jun 05 2020 at 18:54):

@Bas Spitters do you want to see if we can get the HoTT documentation building with jscoq rather than (or in addition to) proviola?

view this post on Zulip Karl Palmskog (Jun 05 2020 at 18:54):

@Bas Spitters I don't think jscoq supports the particular proof-state hovering stuff easily right now, although it could for sure in the future

view this post on Zulip Karl Palmskog (Jun 05 2020 at 18:56):

Jason Gross said:

Yeah, sure. I don't have many cycles to spare for maintaining it right now, but I'm down to be maintainer for now

OK, sounds good. I will look into the transfer in a few hours, and will write up on the GitHub issue if it works out.

view this post on Zulip Bas Spitters (Jun 05 2020 at 18:58):

This one is a few versions behind. https://x80.org/rhino-hott/
Not sure how hard it is to update it @Emilio Jesús Gallego Arias ?

view this post on Zulip Karl Palmskog (Jun 05 2020 at 18:59):

https://x80.org/rhino-coq/v8.11/

view this post on Zulip Karl Palmskog (Jun 05 2020 at 19:00):

still, this doesn't do exactly what Carsten's proof-reanimation does, in my view.

view this post on Zulip Bas Spitters (Jun 05 2020 at 19:25):

A main design goal by Carsten was to make it easy for people to obtain a "movie" of what a proof looks like without installing anything.
jscoq has some of the same goals.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2020 at 19:31):

Should be easy to port, we have been working on a package system but better support for HoTT is doable easily

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2020 at 19:32):

Regarding goals jsCoq does indeed show goals on hover if you press Alt, would be pretty easy to tweak it.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2020 at 19:32):

There is also https://github.com/yforster/proviola

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2020 at 19:33):

Sorry, if you press Ctrl

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2020 at 19:34):

as of today jsCoq does indeed need to run the code to show the goals, but would be easy to have it save a file with pre-computed goals if needed

view this post on Zulip Karl Palmskog (Jun 05 2020 at 19:35):

I've seen that proviola repo before, doesn't contain the full history, which was the goal here. Hopefully we can merge changes into the full repo.

view this post on Zulip Anton Trunov (Jun 05 2020 at 19:57):

@Karl Palmskog Sure, let's park it until Jason has the cycles

view this post on Zulip Théo Zimmermann (Jun 05 2020 at 20:22):

Even if it is to deprecate it eventually in favor of something newer and better, or to merge it with some other project, I still think that moving to coq-community would be a good step forward.

view this post on Zulip Karl Palmskog (Jun 05 2020 at 20:23):

I started the migration via GitHub's importer, we'll see how it goes, can apparently be quite slow. I will also try to assign all commits to Carst's GitHub account.

view this post on Zulip Karl Palmskog (Jun 05 2020 at 20:29):

ah, this might take extra work, there are issues that could be valuable to retain: https://bitbucket.org/Carst/proviola-source/issues - I think I will try this: https://github.com/jeffwidman/bitbucket-issue-migration

view this post on Zulip Karl Palmskog (Jun 05 2020 at 23:58):

the repo is up: https://github.com/coq-community/proviola/ --- but the bad news is that we have to get in touch with Carst to get our hands on the issues in JSON form that can be imported to GitHub

view this post on Zulip Bas Spitters (Jun 06 2020 at 07:30):

Carst has left academia a long time ago ...

view this post on Zulip Karl Palmskog (Jun 06 2020 at 10:20):

I know, but he is apparently using GitHub from time to time, so he might still have access to his BitBucket account (which is needed to download the issues)

view this post on Zulip Karl Palmskog (Jun 06 2020 at 14:21):

@Jason Gross I put you as admin of the repo and added basic metadata/README. Carst said he was open to relicensing from GPL3 to something else. In the interest of wider use in the community, maybe we should ask him if the MIT license would work? Or what do you think?

view this post on Zulip Théo Zimmermann (Jun 06 2020 at 16:59):

@Karl Palmskog Since this is a tool and not a library, strong copyleft is not an issue, so I don't think relicensing would bring anything.

view this post on Zulip Théo Zimmermann (Jun 06 2020 at 17:01):

Regarding the issues to import, does having access to the JSON data change anything about the information that can be retrieved? Otherwise, we might do without. Does your issue importer tool use the GitHub issue import API (the same that was used for Coq and OCaml)?

view this post on Zulip Karl Palmskog (Jun 06 2020 at 17:09):

all issue importer tools need the JSON data from BitBucket, which is only accessible to the BB repo owner. In my view, we either obtain these JSONs or let the issue data disappear completely, since it's too much work to scrape via HTML

view this post on Zulip Karl Palmskog (Jun 06 2020 at 17:10):

to my knowledge, the importer tool I linked uses GitHub's APIs as targets for the processed JSON data from BitBucket

view this post on Zulip Théo Zimmermann (Jun 06 2020 at 17:13):

There are several possible GitHub API so that doesn't really answer my question. And doesn't Bitbucket have an API that could be used as an alternative?

view this post on Zulip Karl Palmskog (Jun 06 2020 at 17:14):

feel free to investigate, but BitBucket support pages all say the only way to export issue data is via repository "Settings", only accessible to the owner

view this post on Zulip Théo Zimmermann (Jun 06 2020 at 17:15):

OK, maybe not then.

view this post on Zulip Karl Palmskog (Jun 06 2020 at 17:17):

https://confluence.atlassian.com/bitbucket/export-or-import-issue-data-330797432.html

view this post on Zulip Karl Palmskog (Jun 06 2020 at 17:47):

in the end, I did find one tool that didn't require export via admin access. The results are a bit mixed (user mapping didn't fully work out), but at least we have the data now.

view this post on Zulip Karl Palmskog (Jun 06 2020 at 17:49):

I'll leave the decision about whether to pursue relicensing or not to Jason, but personally I think GPL3 is a fairly antisocial/forceful license in a community which at least statistically favors permissive open source licenses

view this post on Zulip Théo Zimmermann (Jun 06 2020 at 20:36):

There's no proper way to map issue and comment authors so what you got was the best that an import issue tool could do

view this post on Zulip Théo Zimmermann (Jun 06 2020 at 20:36):

BTW, there should probably be an update posted to the issue in the manifesto repository.

view this post on Zulip Jason Gross (Jun 06 2020 at 20:58):

Karl Palmskog said:

Jason Gross I put you as admin of the repo and added basic metadata/README. Carst said he was open to relicensing from GPL3 to something else. In the interest of wider use in the community, maybe we should ask him if the MIT license would work? Or what do you think?

Sure, MIT License sounds good. Or whatever. Also happy to follow your lead on this.


Last updated: Feb 05 2023 at 15:03 UTC