Karl Palmskog (Jun 05 2020 at 18:45): 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.
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
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)
Jason Gross (Jun 05 2020 at 18:51):@Karl Palmskog sure! Do you want my help doing the migration, or just my approval?
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
Bas Spitters (Jun 05 2020 at 18:54):Arguably, @Emilio Jesús Gallego Arias jscoq is a pretty good alternative.
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
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?
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
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.
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 ?
Karl Palmskog (Jun 05 2020 at 18:59):https://x80.org/rhino-coq/v8.11/
Karl Palmskog (Jun 05 2020 at 19:00):still, this doesn't do exactly what Carsten's proof-reanimation does, in my view.
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.
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
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.
Emilio Jesús Gallego Arias (Jun 05 2020 at 19:32):There is also https://github.com/yforster/proviola
Emilio Jesús Gallego Arias (Jun 05 2020 at 19:33):Sorry, if you press Ctrl
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
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.
Anton Trunov (Jun 05 2020 at 19:57):@Karl Palmskog Sure, let's park it until Jason has the cycles
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.
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.
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
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
Bas Spitters (Jun 06 2020 at 07:30):Carst has left academia a long time ago ...
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)
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?
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.
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)?
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
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
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?
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
Théo Zimmermann (Jun 06 2020 at 17:15):OK, maybe not then.
Karl Palmskog (Jun 06 2020 at 17:17):https://confluence.atlassian.com/bitbucket/export-or-import-issue-data-330797432.html
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.
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
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
Théo Zimmermann (Jun 06 2020 at 20:36):BTW, there should probably be an update posted to the issue in the manifesto repository.
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: Jun 03 2023 at 17:29 UTC