[isabelle-dev] NEWS: activation of Z3 via "z3_non_commercial" system option
makarius at sketis.net
Mon Jan 13 21:18:50 CET 2014
* Activation of Z3 now works via "z3_non_commercial" system option
(without requiring restart), instead of former settings variable
"Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu
Plugin Options / Isabelle / General.
This refers to Isabelle/0c07990363a3. For completeness, the included diff
shows the update on the Isabelle component z3-3.2-1, which is relevant for
Jasmin when he changes z3 again in the future.
The change of z3_non_commercial was already planned for Isabelle2013-2,
but did not make it into the release, because I could not make up my mind
how much hand-holding the user should get. Right now it is the minimal
possible approach to it, without any hand-holding apart from some prose
I have taken the opportunity to experiment with Pretty.para here:
traditionally we have short one-line output that is statically broken, but
here the long text might look better with dynamic word-wrapping. The
disadvantage is that such output is harder to search formally in log files
-------------- next part --------------
diff -r z3-3.2/etc/settings z3-3.2-1/etc/settings
< # Z3_NON_COMMERCIAL="yes"
Only in z3-3.2/etc: ._settings
diff -r z3-3.2/README z3-3.2-1/README
< in the environment or in "$ISABELLE_HOME_USER/etc/settings".
> the Isabelle system option "z3_non_commercial" to "yes" (e.g. via the
> Isabelle/jEdit menu Plugin Options / Isabelle / General).
Only in z3-3.2/x86-darwin: z3.dbg
More information about the isabelle-dev