search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
65 stars 20 forks source link

Add license field to opam package definition file #145

Closed ahelwer closed 1 month ago

ahelwer commented 2 months ago

Without this field, newer versions of opam will print out the following warning when running make opam-deps:

[WARNING] Failed checks on tlapm package definition from source at git+file:///mnt/data/ahelwer/src/tlaplus/proofs#main: warning 68: Missing field 'license'

This tiny change fixes that warning by adding the SPDX short form of the repo's license to the tlapm.opam file.

kape1395 commented 2 months ago

This change specified "License: 2-clause BSD", but the README.md mentions

License: 2-clause BSD, portions under LGPL2.1+LE (see file LICENSE for details)

I checked the https://github.com/tlaplus/tlapm/blob/main/LICENSE, it matches https://opensource.org/license/bsd-2-clause. No exceptions mentioning LGPL are there. Maybe README.md should be updated as well?

@muenchnerkindl, @damiendoligez, maybe you remember why LGPL is mentioned here?

muenchnerkindl commented 2 months ago

My guess would be that the `translate' utility (related to the LS4 decision procedure for propositional temporal logic) might originally have been under LGPL, but the README says that the author agreed to let us use it under BSD. @damiendoligez Do you remember?