Zulip Chat Archive

Stream: mathlib4

Topic: how should I merge old & new copyright headers?

Bulhwi Cha (Apr 23 2023 at 06:38):

I'm porting data.string.defs, which has two different copyright headers.

data.string.defs:

Copyright (c) 2019 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Keeley Hoek, Floris van Doorn

Data.String.Defs:

Copyright (c) 2021 Chris Bailey. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Bailey

@Chris Bailey, is it okay for me to change the copyright header as follows?

Copyright (c) 2019 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Keeley Hoek, Floris van Doorn, Chris Bailey

Bulhwi Cha (Apr 23 2023 at 07:28):

GitHub PR: !4#3601

Scott Morrison (Apr 23 2023 at 09:43):

LGTM.

Chris Bailey (Apr 23 2023 at 15:46):

Bulhwi Cha said:

I'm porting data.string.defs, which has two different copyright headers.

data.string.defs:

Copyright (c) 2019 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Keeley Hoek, Floris van Doorn

Data.String.Defs:

Copyright (c) 2021 Chris Bailey. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Bailey

Chris Bailey, is it okay for me to change the copyright header as follows?

Copyright (c) 2019 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Keeley Hoek, Floris van Doorn, Chris Bailey

Yes, I'm fine with any changes to the copyright header that you feel are warranted. Thanks.

Eric Wieser (Apr 23 2023 at 17:21):

I'm porting data.string.defs, which has two different copyright headers.

Is any of Data.String.Defs worth keeping? Usually the approach when porting is to discard the previous ad-hoc port and replace it with the mathport output; unless the adhoc version contains content that wasn't in mathlib3

Scott Morrison (Apr 23 2023 at 21:26):

Some functions, e.g. stripPrefix etc were added for metaprogramming.

Bulhwi Cha (Apr 24 2023 at 02:10):

New PR: !4#3612

Last updated: Dec 20 2023 at 11:08 UTC