[isabelle-dev] Isabelle component csdp-6.x is 32-Bit [macOS]

Makarius makarius at sketis.net
Mon Dec 23 21:54:34 CET 2019


On 27/11/2019 20:00, Makarius wrote:
> On 27/11/2019 19:20, Clemens Ballarin wrote:
>> While doing 'isabelle build -a', macOS 10.14.4 (Mojave) informs me that
>> 'csdp' is a 32-bit executable that won't run on Catalina [1].  This is
>> for revision c9433e8e314e of yesterday.
>>
>> The executable is part of the Isabelle component located at
>> ~/.isabelle/contrib/csdp-6.x.  Which functionality depends on this
>> component and will fail after upgrading to Catalina?
> 
> I am generally lagging behind in checking support for Catalina for
> Isabelle and add-on tools. In the past couple of years our basis for
> macOS test hardware has dwindled. At home I merely have a somewhat
> pathetic Mac Mini to test it, but I first need to install the new OS
> version in the first place.
> 
> Concerning CSDP there is a particular problem for macOS: the official
> project downloads from https://github.com/coin-or/Csdp are only for
> Linux and Windows. The macOS executable that we ship with csdp-6.x is an
> older version.

See now the following changes:

changeset:   71339:05400628c56b
user:        wenzelm
date:        Mon Dec 23 19:07:25 2019 +0100
files:       Admin/components/components.sha1 Admin/components/main
description:
updated csdp-6.1: Linux and Windows executables are as before, but macOS has
been rebuilt for x86_64 (to accommodate Catalina);
NOTE: current version 6.2.0 caused odd problems with parallel invocations
(e.g. on Ubuntu 18.04);

changeset:   71340:6d9dd5309b85
tag:         tip
user:        wenzelm
date:        Mon Dec 23 19:27:37 2019 +0100
files:       src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
description:
proper File.platform_path for Windows;


As usual, it has required a bit more tinkering than expected. The Linux and
Windows executables are actually statically linked x86 applications; that
means they might break in a few years. The official 6.2.0 did not really work
for us for unknown reasons.


	Makarius


More information about the isabelle-dev mailing list