[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