Re: [isabelle] Isabelle 2011 and SWI-Prolog

On 02/09/2011 04:39 PM, Makarius wrote:
On Wed, 9 Feb 2011, Christian Maeder wrote:

I was also surprised by a disturbing message from an old SWI-Prolog-5.6.? installation that caused no problem for older Isabelle versions.

There is a experimental evaluation mechanism to compute (symbolic) values of inductive predicates with SWI-Prolog. Some examples can be found in src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy As it is a experimental feature, it might be superseded by future developments soon.


Probably nothing. I.e. you can just deactivate Isabelle2011/src/HOL/Tools/Predicate_Compile/etc/settings by renaming the file or commenting out the "choosefrom" invocations that pick up external tools accidentally.

I've introduced "choosefrom" myself many years ago, but it has come out of fashion more recently, when explicit "components" were introduced. So it looks like it would be better to phase out this implicit collecting of settings altogether in the next release.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.