Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle 2011 and SWI-Prolog

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: Apr 25 2024 at 08:20 UTC