[isabelle-dev] status of remote_z3

[Makarius]

On Tue, 7 Jan 2014, boehmes at in.tum.de wrote:

> It was necessary years ago when only a Windows version of Z3 was 
> available.

Now I vaguely remember the time when the only official release was for 
Windows, and Linux just an accidental snapshot for the CADE system 
competition.

Times have indeed changed a lot concerning MSR, also thanks to continous 
nagging by Mac OS X users :-)


> Unless Sledgehammer requires the remote_z3 service, any references to 
> this obsolete service can now be removed from the code. I’ll take care 
> of this.

Great.  I am looking forward to that.


This also reminds me that I wanted to turn the Z3_NON_COMMERCIAL settings 
variable into a system option (in ~~/src/HOL/Tools/etc/options).  Then the 
user can reconfigure that without rebooting (or knowing basic syntax of 
GNU bash).  But it requires some rearrangements of how Isabelle/HOL/SMT 
reads the configuration, and how the front-end allows editing it.


 	Makarius