Email Gateway (Aug 22 2022 at 19:21): Email Gateway (Aug 22 2022 at 19:21):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I have a soft question related to the redistribution of the source code
from the library HOL. Hopefully, my understanding/interpretation of the
legalese involved is correct. However, I would like to confirm
my understanding with someone more knowledgeable.
It is my understanding that HOL is a part of Isabelle and, therefore, it is
distributed under the terms of the BSD license. Thus, if I am not mistaken,
I can amend and redistribute any code from HOL under a compatible license
(e.g. LGPL v3), provided that the file COPYRIGHT that is located in the top
directory of Isabelle is included together with the amended files from HOL.
Is it acceptable to rename the file COPYRIGHT (e.g. to COPYRIGHT-ISABELLE)?
Does it need to be located in the top directory of the project that
contains the amended file(s)? Are there any other files that I should
include? Should I provide any additional information?
As a side note, I would like to mention that my intention is merely to
include some of the source code from several files that are located in
"HOL/Types_To_Sets/Examples" (with certain amendments) in my personal
project that is licensed under LGPL v3.
Thank you
Last updated: Apr 25 2024 at 16:19 UTC