[isabelle-dev] Standard component setup (Re: NEWS)

[Makarius]

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