search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.42k stars 339 forks source link

Backward generation of binary releases #5202

Open ajrouvoet opened 3 years ago

ajrouvoet commented 3 years ago

@L-TChen pointed out that the nightly release comes with binaries for multiple platforms. In teaching Agda I've seen many students struggle to get Agda on Windows. A zip with executables would save them many hours and frustration to get started (with PLFA).

Is it possible to still release in backwards fashion the binaries for the different platforms for e.g. 2.6.1.1?

L-TChen commented 3 years ago

I don't think there will be any technical problems with this. As I mentioned on Zulip, one needs to check if conditions listed in the license of every package Agda uses are met before releasing an official binary. Perhaps this is not an issue, but I hope someone can clarify this.

As for Windows, I don't know how to build a .msi but just ordinary executable files. Will it be enough?

nad commented 3 years ago

As I mentioned on Zulip, one needs to check if conditions listed in the license of every package Agda uses are met before releasing an official binary.

The cabal-plan tool can help with that, but this tool only handles Cabal packages (and the rts package seems to be excluded from the generated listing). I'm not sure exactly which other libraries Agda depends on, but the list includes zlib and ICU.

andreasabel commented 3 years ago

The cabal-plan tool can help with that, but this tool only handles Cabal packages (and the rts package seems to be excluded from the generated listing).

See #5134 for more context on this.

L-TChen commented 3 years ago

The following is the list of all licenses used by dependencies reported by cabal-plan:

The clause from BSD-2/3 in which we are interested is the following part

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: ...

  1. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. ...

MIT license is similar

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

so is ISC

Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above copyright notice and this permission notice appears in all copies.

In short, for the binary redistribution, we just need to provide the copyright notice of every (direct or indirect) dependency used by Agda. So, the question is how. Is it sufficient to list all the dependencies used by Agda with the link to their Hackage page in the documentation?

ajrouvoet commented 3 years ago

Thank you for looking into this! Do you mean the online docs or something like a man page or --help? I think the notices should be accessible from the distributed package, so the online docs won't do afaict.

L-TChen commented 3 years ago

Aha, you're right. It should be the documentation bundled with the distribution according to the clause.

I am now baffled after checking how other software is doing it. For example, pandoc does not mention dependencies at all, and the macOS binary provided on the official website shows its own GNU license only. Is it enough to just include the license report as part of the distribution?

ajrouvoet commented 3 years ago

I am now baffled after checking how other software is doing it.

Just like protecting your software against malicious updates of dependencies, licensing of dependencies is also largely ignored in much software development...

Does the report include the copyright notices? The literal text should be in there.

L-TChen commented 3 years ago

Here is the report generated by cabal-plan. It lists Haskell dependencies (but external libraries) and licenses with a link to the license declaration on Hackage. Perhaps a little script is needed to download all copyright notices following the link and put all of them as part of distribution?

nad commented 3 years ago

Note that, as I wrote above, cabal-plan does not list all relevant dependencies.

L-TChen commented 3 years ago

Is it enough to check if the description file .cabal contains a nonempty field extra-libraries?

nad commented 3 years ago

Perhaps it is possible to "smuggle in" a dependency using Setup.hs.

andreasabel commented 3 years ago

@L-TChen

  1. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

I took that seriously in BNFC/bnfc#308. BNFC has an option --license which prints the license text, see https://github.com/BNFC/bnfc/blob/master/source/src/BNFC/License.hs. https://github.com/BNFC/bnfc/blob/3bb050a426c6fbdc9d89b4c8217a648701681b6e/source/main/Main.hs#L60

While implementing this, I wondered why cabal does not have a standard solution for this, like it has for the version number (module Paths_XXX (version)). I opened a ticket at https://github.com/haskell/cabal/issues/7173

But I also wonder how "reproduce" is to be implemented, officially.

L-TChen commented 3 years ago

Right, it makes sense to solve this issue upstream. I will see if I can make a PR to improve the situation.