Source file with non-commercial license

27 views
Skip to first unread message

Chuck Lutz

unread,
Nov 16, 2020, 7:02:36 AM11/16/20
to tlaplus
Hi folks,

I'm looking to possibly use TLA+ at work, but our legal folks have pointed out that the following file includes a license that restricts non-commercial use:

https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2tex/PosAndCol.java

Is this file vital to the use of TLA+? They want to remove it from what would be our internally-approved distribution of the .tgz / .zip from GitHub.

It seems like it would affect the pretty-printing.

Thanks in advance for any information,
Chuck Lutz

Markus Kuppe

unread,
Nov 16, 2020, 11:59:23 AM11/16/20
to tla...@googlegroups.com, Chuck Lutz
Hi Chuck,

there are many source files with an identical or similar copyright
header. You won't be able to remove all of them without breaking TLC.
However, as agreed to by the copyright holders HP/Compaq and Microsoft,
the TLA+ tools and the Toolbox are released under the (permissive) MIT
license [1]. Please open an issue [2] if your legal department still has
concerns.

Thanks,
Markus

[1] https://github.com/tlaplus/tlaplus/blob/master/README.md#license
[2] https://github.com/tlaplus/tlaplus/issues

Stephan Merz

unread,
Nov 16, 2020, 12:01:44 PM11/16/20
to tla...@googlegroups.com
I believe that the part that Chuck refers to is the copyright inherited from UBC for HeapSort, even if this algorithm is commonplace.

Stephan
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1841241c-b3f4-caa3-db17-8d1e9e3d82bf%40lemmster.de.

Markus Kuppe

unread,
Nov 16, 2020, 1:23:18 PM11/16/20
to tla...@googlegroups.com, charles...@gmail.com
On 16.11.20 09:01, Stephan Merz wrote:
> I believe that the part that Chuck refers to is the copyright inherited from UBC for HeapSort, even if this algorithm is commonplace.


Thanks, Stephan! Shouldn't be a big deal to replace this
sort-implementation with one from the JDK:
https://github.com/tlaplus/tlaplus/issues/539

M.

Chuck Lutz

unread,
Nov 17, 2020, 10:27:53 AM11/17/20
to tlaplus
Hi again Marcus and Stephan,

Yes, correct - the HeapSort was specifically the problem. 

As I was not too specific before :-), here is the main bit:

"HeapSortAlgorithm.java 1.0 95/06/23 Jason Harrison
Copyright (c) 1995 University of British Columbia"

Would omitting only this file disable TLC or anything vital? It seemed that this is perhaps part of a layout algorithm for translating to TeX, so I assumed that would be a "nice to have" vs. part of the core functionality.

Regards,
Chuck Lutz

Markus Kuppe

unread,
Nov 17, 2020, 11:14:43 AM11/17/20
to tla...@googlegroups.com
On 17.11.20 07:27, Chuck Lutz wrote:
>
> Yes, correct - the HeapSort was specifically the problem. 
>
> As I was not too specific before :-), here is the main bit:
>
> "HeapSortAlgorithm.java 1.0 95/06/23 Jason Harrison
> Copyright (c) 1995 University of British Columbia"
>
> Would omitting only this file disable TLC or anything vital? It seemed
> that this is perhaps part of a layout algorithm for translating to TeX,
> so I assumed that would be a "nice to have" vs. part of the core
> functionality.


Hi Chuck,

the implementation of HeapSort has been removed [1]. You can download
new builds of TLC and the Toolbox from [2]. Omitting the file would
indeed break the pretty-printer (TeX).

Markus

[1]
https://github.com/tlaplus/tlaplus/commit/8b52d238eb9f17df98dd795dbb589d9fba4a5822
[2] https://nightly.tlapl.us

Chuck Lutz

unread,
Nov 18, 2020, 1:25:16 AM11/18/20
to tlaplus
Hi again,

Wow, thanks very much for the quick update!

Regards,
Chuck

Chuck Lutz

unread,
Nov 20, 2020, 11:00:56 AM11/20/20
to tlaplus
Hi again Markus and Stephan,

Thanks for the link to the nightly builds. I would like to ask if you know when this change might make it into an "official" release (I put that in quotes as I am not familiar with the TLA+ release approach, rhythms, etc.)

I think we might need to look to the next release for various traceability reasons.

Thanks,
Chuck Lutz

Reply all
Reply to author
Forward
0 new messages