On Sun, 8 Jan 2012, Alexander Krauss wrote:
On 01/05/2012 12:19 PM, Jasmin Christian Blanchette wrote:
We are not allowed to distribute Yices. When publishing the components,
please exclude Yices.
... and Vampire.
Could we instead provide a little script (or Isabelle tool) that turns a
tarball/zip downloaded from upstream into a packaged Isabelle component?
This would possibly lower the entry barrier for using these systems, and
should be fine with the licenses. It can also save a little packaging
work in the future.
I've occasionally spent some thoughts on Z3 as well. MSR did not mind
other distribution channels, but the user has to indicate his
non-commercial status explicit, doing some awkward editing of the
compinent settings.
This could be somehow facilitated by allowing explicit interactive setup
for components, say as Scala/JVM module that posts a dialog and asks the
user to tick a license agreement before the settings are patched
accordingly. Once that this concept is supported, one could easily include
an adhoc download as well, say for retrieving Vampire from its official
website.
Anyway, there are so many other things that could be done to simplify
deployment. I am not sure how much priority to apply to this painful
non-free stuff right now.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
