Proposal to move reduction-effects from coq-community to Coq main

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 reduction-effects from coq-community to Coq main #163

Open MSoegtropIMC opened 3 weeks ago

MSoegtropIMC commented 3 weeks ago

As discussed in Zulip and in the Coq call 2024-10-29, it would make sense to integrate the reduction-effects plugin into the Coq main line.

The main rational is:

there is no gallina debugger - this plugin gives t least "print" debugging
debugging gallina is an important aspect of Coq projects actually using the excellent compute capabilities of Coq
integration improves distribution, maintenance and possibly leads to a few enhancements

palmskog commented 3 weeks ago

@JasonGross @liyishuai what's your view of this proposal to move the repo code to the Coq repo, for or against?

@MSoegtropIMC I recommend you start an issue in the reduction-effects repo where you ping in and ask the copyright holders if they are willing to relicense their work from MPL-2.0 to LGPL-2.0-only (Coq's license).

JasonGross commented 3 weeks ago

I'm in favor

liyishuai commented 3 weeks ago

Affirmative.