[isabelle-dev] HOL/Complex fails due to Z3 requirement
makarius at sketis.net
Wed Feb 26 13:19:05 CET 2014
This refers to Isabelle/565a20b22f09:
Loading theory "Complex_Main"
*** The SMT solver Z3 is not activated. To activate it, set the Isabelle system
*** option "z3_non_commercial" to "yes" (e.g. via the Isabelle/jEdit menu Plugin
*** Options / Isabelle / General).
*** At command "by" (line 626 of "~~/src/HOL/Complex.thy")
This also explains the total existence failure of isatest today: without
main HOL, the distribution build does not work.
Z3 requirements don't work for regular library theories: Isabelle would
become a non-free non-commercial-use system. This is also why most
isatest configurations exclude Z3 according to the default settings.
More information about the isabelle-dev