search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Proposal to move NuprlInCoq to Coq-community #60

Open palmskog opened 5 years ago

palmskog commented 5 years ago

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 commented 5 years ago

@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 commented 5 years ago

@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 commented 5 years ago

@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 commented 5 years ago

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 notifications@github.com 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 https://github.com/coq-community/manifesto/issues/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 commented 5 years ago

@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 commented 4 years ago

@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 commented 4 years ago

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

On Wed, Sep 30, 2020 at 4:43 PM Bas Spitters notifications@github.com 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 https://github.com/coq-community/manifesto/issues/60#issuecomment-701474676, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABBRX3CKV3KHOQQIR36XYZDSING3DANCNFSM4HBJQO6Q .

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

palmskog commented 4 years ago

@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.