search

coq-community / reduction-effects

A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
Mozilla Public License 2.0
6 stars 6 forks source link

Move to coq main line / relicensing #24

Open MSoegtropIMC opened 4 weeks ago

MSoegtropIMC commented 4 weeks ago

As discussed in https://github.com/coq-community/manifesto/issues/163 (see there for further references) it would make sense to integrate this plugin into the main line. This has been discussed in the recent Coq call 2024-10-29 and the Coq developer team is positive about this.

A not necessarily required but convenient step would be to relicense this to the license of Coq (LGPL-2.1 only). It likely makes sense to dual license it.

What do the contributors think of both, the move and the relicensing?

@liyishuai @JasonGross @SkySkimmer @herbelin @Zimmi48 @gares

Please state your agreement to the move and the relicensing here (preferably state your opinion on both variants, a dual license and a single new license).

JasonGross commented 4 weeks ago

I'm in favor of the move. I never understood why this was a separate repo in the first place.

I have no opinion on relicensing vs dual licensing, and am happy to do whatever is most convenient

MSoegtropIMC commented 4 weeks ago

A note on the license: as discussed in Zulip the preferred option is to archive the repo here using the current license and use the new license only for the copy living in the Coq repo then.

liyishuai commented 4 weeks ago

A note on the license: as discussed in Zulip the preferred option is to archive the repo here using the current license and use the new license only for the copy living in the Coq repo then.

I second this archiving and relicensing plan.

SkySkimmer commented 4 weeks ago

all ok

gares commented 4 weeks ago

I'm in favor of the move to the coq repo. I'm in favor of relicensing the code under the same license of Coq (LGPL 2.1 only).

herbelin commented 4 weeks ago

All ok, I'm following the (meta)move for a move. I a priori favor a relicensing the code under the same license of Coq.