Source file with non-commercial license

[Chuck Lutz]

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]

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]

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]

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]

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]

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]

Hi again,

Wow, thanks very much for the quick update!

Regards,

Chuck

[Chuck Lutz]

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