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



On Tue, 1 Feb 2011, Lukas Bulwahn wrote:

On 02/01/2011 03:24 PM, René Thiemann wrote:

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.

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


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