Email Gateway (Aug 18 2022 at 17:14): Email Gateway (Aug 18 2022 at 17:14):From: Christian Maeder <Christian.Maeder@dfki.de>
I was also surprised by a disturbing message from an old
SWI-Prolog-5.6.? installation that caused no problem for older Isabelle
versions.
(The message and the SWI-Prolog installation is lost now. I'm under linux.)
What do I loose without SWI-Prolog?
Cheers Christian
Email Gateway (Aug 18 2022 at 17:14):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 18 2022 at 17:14):From: Lukas Bulwahn <bulwahn@in.tum.de>
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.
Lukas
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.Makarius
Last updated: Nov 21 2024 at 12:39 UTC