Stream: Coq devs & plugin devs

Topic: latex1 test from test-suite fails


view this post on Zulip Pierre-Marie Pédrot (Aug 23 2022 at 20:42):

Hi all, I've recently updated my texlive package on Debian unstable (to version 2022.20220722-1) and now I'm getting weird errors from test-suite/coq-makefile/latex1.v.

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2022 at 20:43):

I get a bunch of

! Argument of <C2> has an extra }.
<inserted text>
                \par
l.24 ...t.sub.testsub}{Library }{test.sub.testsub}

Runaway argument?

view this post on Zulip Pierre-Marie Pédrot (Aug 23 2022 at 20:44):

Did I break something in my installation, or is the Coq tex wrapper incompatible with the latest TexLive release?

view this post on Zulip Julien Puydt (Aug 24 2022 at 06:58):

I'll see if coq-doc compiles with a recent unstable -- I didn't check that when I did my Coq 8.16 work

view this post on Zulip Julien Puydt (Aug 24 2022 at 07:17):

The compilation of coq-doc 8.15.2 just went through. [Reminder: coq-doc is the non-free package building the Coq documentation in Debian]

view this post on Zulip Ali Caglayan (Aug 24 2022 at 11:15):

Why was it non-free again?

view this post on Zulip Théo Zimmermann (Aug 24 2022 at 11:41):

Because of the license of the refman: https://github.com/coq/coq/issues/8774

view this post on Zulip Ali Caglayan (Aug 24 2022 at 11:51):

So we are not changing the liscence since we don't fully understand the implications of doing so? Why not change the liscence and find out later what the implications are (if any)?

view this post on Zulip Théo Zimmermann (Aug 24 2022 at 11:51):

We cannot change the license because you need the permission from all the copyright owners and we don't even know who they are.

view this post on Zulip Ali Caglayan (Aug 24 2022 at 11:52):

What is stopping us though? If we change the liscence after having asked the ones we know, anybody else complaining will simply inform us who the copy right owners are.

view this post on Zulip Théo Zimmermann (Aug 24 2022 at 11:52):

Changing a license without obtaining permission from copyright owners is copyright infringement and is worse than doing nothing. Best way to make sure lots of users won't use your software anymore (and Debian won't include it).

view this post on Zulip Théo Zimmermann (Aug 24 2022 at 11:53):

Because basically, this means that you are putting users at risk by having bad licensing practices.

view this post on Zulip Ali Caglayan (Aug 24 2022 at 11:55):

But we aren't changing the liscence in "bad faith". Surely people would understand that we are simply changing the liscence to be more sane. It seems strange to me that we would be grouped as "copyright infrigners" so seriously.

view this post on Zulip Théo Zimmermann (Aug 24 2022 at 11:57):

I'm talking about law here, not about ethics.

view this post on Zulip Théo Zimmermann (Aug 24 2022 at 11:57):

On the ethics side, I'm in full agreement with you.

view this post on Zulip Ali Caglayan (Aug 24 2022 at 11:58):

Well of course, I can only give my ethical opinion since I am not a lawyer. It just seems very strange and a huge waste of (lawyer) time.

view this post on Zulip Ali Caglayan (Aug 24 2022 at 11:58):

0:-)

view this post on Zulip Théo Zimmermann (Aug 24 2022 at 11:58):

And for individual users of open source software, it may not be very important whether copyright law is well followed or deviated from, but for company users, legal trouble is something they might want to stay away from because of (hypothetical) consequences.

view this post on Zulip Théo Zimmermann (Aug 24 2022 at 12:00):

Ali Caglayan said:

Well of course, I can only give my ethical opinion since I am not a lawyer. It just seems very strange and a huge waste of (lawyer) time.

Well, I am not a lawyer either, but I have read enough to formulate an opinion on what law says in the case of copyright and its consequence on software / documentation licensing.

view this post on Zulip Théo Zimmermann (Aug 24 2022 at 12:09):

A way out in this case would be to ask the author of the OPL to publish a new version which is identical, except it allows relicensing to some CC license. A similar pattern has happened before. This is how Wikipedia was relicensed from GFDL to CC: https://wiki.creativecommons.org/wiki/Interoperability_between_Creative_Commons_licenses_and_GFDL. But Wikipedia was a sufficient important reason to justify this. I'm not sure that Coq's refman is ;-)

view this post on Zulip Paolo Giarrusso (Aug 24 2022 at 12:12):

The issue says the license authors have deprecated OPL — so they might be open to it in general?

view this post on Zulip Paolo Giarrusso (Aug 24 2022 at 12:15):

but I see your concerns.

view this post on Zulip Karl Palmskog (Aug 24 2022 at 12:28):

ah, the license text actually says "[ODL] v1.0 or later"

view this post on Zulip Karl Palmskog (Aug 24 2022 at 12:29):

so there is a glimmer of hope there

view this post on Zulip Julien Puydt (Aug 25 2022 at 07:29):

How can it be that the authors are unknown!?

If you told me "There's this author, with huge contributions, and who refuses to change", I would understand.

If you told me "There's this author, huge contributions, dead", I would tell you their family has the rights and there is hope.

But "We don't know the authors" !?

view this post on Zulip Théo Zimmermann (Aug 25 2022 at 07:53):

How can it be that the authors are unknown!?

I never said "the authors are unknown", I said "the copyright owners are unknown", which is very different.

view this post on Zulip Karl Palmskog (Aug 27 2022 at 20:17):

for some context, both US and European universities/institutes seem to have a wide variety of IP ownership practices. Sometimes, everything authored is automatically owned by the employee (or student, if the student is not an employee), but sometimes not. The problem with authors vs. owners is the latter case.


Last updated: Feb 06 2023 at 19:03 UTC