Proposal to move NuprlInCoq to Coq-community

[palmskog]

Move a project to coq-community

Project name: NuprlInCoq

Initial author(s): Vincent Rahli, Abhishek Anand, and Mark Bickford

Current URL: https://github.com/vrahli/NuprlInCoq

Kind: pure Coq library and extractable program

License: GPL-3-or-later

Description: A formalization of Nuprl's Constructive Type Theory (CTT) as of 2016, including an executable proof checker in OCaml based on extracted code. There is a website listing some publications.

Status: maintained

New maintainer: Vincent Rahli (@vrahli)

[palmskog]

@vrahli expressed interest to move this project to the community, so I create this issue to keep track.

This project poses some unique challenges for CI due to its long proof checking time (hours, last time I investigated). Travis will time out for the whole project for sure. We may be able to come up with some special solution for CI via GitLab (cc: @Zimmi48), or we simply settle on checking only certain parts of the project.

In the future, this project will be a priority target for incremental checking in CI (coq/coq#9262, ejgallego/coq-lsp#327).

[Zimmi48]

@vrahli Could you confirm that https://github.com/coq-contribs/intuitionistic-nuprl is just a copy of the same project that diverged while being maintained by the Coq development team? If that's the case, I'll archive the coq-contribs copy as read-only with a link to the current repo.

BTW @vrahli, you should have received an invitation to join coq-community. After you accept the invitation, you should be able to transfer the two repositories NuprlInCoq and Velisarios. If you need help for this operation, let me (or Karl) know.

[Zimmi48]

@vrahli Do you still intend to transfer this project and Velisarios to coq-community? If yes, let me know if you need help with the transfer operation. If not, we should close this issue.

Can you also confirm that the copy in coq-contribs should be archived and redirect to your version of the project?

[vrahli]

Yes, I still want to transfer this project and Velisarios to coq-community. Yes, the copy in coq-contribs is outdated. The up to date version is this one: https://github.com/vrahli/NuprlInCoq

…

On Wed, Jun 26, 2019 at 7:55 AM Théo Zimmermann ***@***.***> wrote: @vrahli <https://github.com/vrahli> Do you still intend to transfer this project and Velisarios to coq-community? If yes, let me know if you need help with the transfer operation. If not, we should close this issue. Can you also confirm that the copy in coq-contribs should be archived and redirect to your version of the project? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#60?email_source=notifications&email_token=ABBRX3D2NGOJONZMO662CZ3P4MHF7A5CNFSM4HBJQO62YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODYSREGQ#issuecomment-505745946>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABBRX3FTPV3D3HMPW7VY6ZTP4MHF7ANCNFSM4HBJQO6Q> .

-- https://vrahli.github.io/

[Zimmi48]

@vrahli The copy at coq-contribs has been archived. You have been made a member of coq-community. Therefore, if you still intend to transfer this project, you should have everything you need to be able to proceed. If not, we should probably close this issue instead.

[spitters]

@vrahli your development is taking a long time. By moving to the community, more people can help fixing that.
https://coq-bench.github.io/clean/Linux-x86_64-4.03.0-2.0.5/released/8.6/intuitionistic-nuprl/8.6.0.html

[vrahli]

Hi, so even though this version is archived it is still compiled?

…

On Wed, Sep 30, 2020 at 4:43 PM Bas Spitters ***@***.***> wrote: @vrahli <https://github.com/vrahli> your development is taking a long time. By moving to the community, more people can help fixing that. https://coq-bench.github.io/clean/Linux-x86_64-4.03.0-2.0.5/released/8.6/intuitionistic-nuprl/8.6.0.html — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#60 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABBRX3CKV3KHOQQIR36XYZDSING3DANCNFSM4HBJQO6Q> .

-- https://vrahli.github.io/

[palmskog]

@vrahli this ancient version of the project is unfortunately the only one that Coq opam package index users will see. Our aims here here are to do frequent releases (tags) for projects to match new Coq releases and consolidate all previous tarballs floating around into a single location.