Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle and SWI-Prolog under MacOS

Email Gateway (Aug 18 2022 at 17:02):

From: Lukas Bulwahn <bulwahn@in.tum.de>
On 02/01/2011 03:24 PM, René Thiemann wrote:

Dear all,

after updating to Isabelle 2011, I get the following message when
calling "isabelle version"

expr: syntax error
Isabelle2011: January 2011

However, I figured out that only if the executable

/opt/local/bin/swipl (SWI-Prolog via MacPorts)

is present, then the "expr: syntax error" is displayed.
To put it differently, after "mv /opt/local/bin/swipl /opt/local/bin/swi"
the call "isabelle version" just displays

Isabelle2011: January 2011

as desired. Any ideas?

An experimental feature of the Isabelle system is trying to detect if
the swi-prolog exists and if existent, tries to determine its version
via the non-standard and non-portable bash/linux command expr.

I will improve this bash script in the development version.

The error message "expr: syntax error" can be ignored, and should not
cause the main system to fail.

Lukas

Best,
René

PS: The same error occurs on two different Intel-Macs both running
Leopord (10.5)
PPS: If one removes the original swipl and replaces it by some script
like "echo $* >/tmp/args"
then the "expr: syntax error" remains, and detects that swipl is
called with arguments "--version"

Email Gateway (Aug 18 2022 at 17:03):

From: Makarius <makarius@sketis.net>
This is a known feature, it was there from the very beginning of the
swi_prolog setup, and is also documented, see
http://isabelle.in.tum.de/repos/isabelle/annotate/9e576ec5c0dc/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version

Makarius

Email Gateway (Aug 18 2022 at 17:15):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,

after updating to Isabelle 2011, I get the following message when
calling "isabelle version"

expr: syntax error
Isabelle2011: January 2011

However, I figured out that only if the executable

/opt/local/bin/swipl (SWI-Prolog via MacPorts)

is present, then the "expr: syntax error" is displayed.
To put it differently, after "mv /opt/local/bin/swipl /opt/local/bin/
swi"
the call "isabelle version" just displays

Isabelle2011: January 2011

as desired. Any ideas?

Best,
René

PS: The same error occurs on two different Intel-Macs both running
Leopord (10.5)
PPS: If one removes the original swipl and replaces it by some script
like "echo $* >/tmp/args"
then the "expr: syntax error" remains, and detects that swipl is
called with arguments "--version"

Last updated: Apr 25 2024 at 04:18 UTC