[isabelle-dev] NEWS: support for GHC

Makarius makarius at sketis.net
Sun Oct 21 16:16:51 CEST 2018


On 21/10/2018 13:25, Lars Hupel wrote:
>> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
>> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
>> Existing settings variable ISABELLE_GHC is maintained dynamically
>> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
> 
> On an El Capitan system, this produces the following error:
> 
> $ uname -a
> Darwin macisa1.in.tum.de 15.6.0 Darwin Kernel Version 15.6.0: Mon Aug 29
> 20:21:34 PDT 2016; root:xnu-3248.60.11~1/RELEASE_X86_64 x86_64
> 
> $ ./bin/isabelle ghc_setup
> /Users/hupel/workspace/isabelle/lib/scripts/getfunctions: line 1: 31569
> Illegal instruction: 4  env STACK_ROOT="$(platform_path
> "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@"

Maybe there is something wrong with the hardware or the system installation.

It works fine on all Macs that are part of the official isabelle-dev
test infrastructure. See also Admin/PLATFORMS (Isabelle/c360f3b603f8):

  x86_64-darwin     Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
                    Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1)
                    macOS 10.12 Sierra (macbroy30 MacBookPro6,2)
                    macOS 10.13 High Sierra (!?)
                    macOS 10.14 Mojave (!?)

This also shows that 10.13 and 10.14 are presently not covered: there
has been a general decline in Mac support in recent years. Isabelle on
macOS presently hinges on a somewhat pathetic Mac Mini that I have at home.

It would be great to recover some old vigor concerning isabelle-dev
platform coverage: via regular OS installations with regular SSH access.
Maybe even with nightly build_history measurements via isabelle_cronjob
(not Jenkins).


	Makarius



More information about the isabelle-dev mailing list