* 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
text.
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
etc.
Makariusdiff -r z3-3.2/etc/settings z3-3.2-1/etc/settings
4,6c4
< Z3_HOME="$Z3_COMPONENT/$ISABELLE_PLATFORM"
<
< # Z3_NON_COMMERCIAL="yes"
---
> Z3_HOME="$Z3_COMPONENT/$ISABELLE_PLATFORM32"
Only in z3-3.2/etc: ._settings
diff -r z3-3.2/README z3-3.2-1/README
16,19c16,17
<
< Z3_NON_COMMERCIAL="yes"
<
< 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
