Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Lars Hupel
> On an El Capitan system, this produces the following error:

The problem can alternatively be solved by installing Homebrew's stack
version and declaring

ISABELLE_STACK="/usr/local/bin/stack"

in ~/.isabelle/etc/settings.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Lars Hupel
> * 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" "$@"

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Florian Haftmann
> * 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.

Just a side remark: I have tried »isabelle ghc_setup« and
»isabelle_ocaml_setup« and they work like a charm.

Florian



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Makarius
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Lars Hupel
> Can you actually explain the problem and its solution?

The problem appears to be that the official Stack binaries do not work
consistently on El Capitan. The machine I've tried them on is fully
updated and has no special software setup.

The binary provided by Homebrew does not exhibit that problem. I have no
other information beyond that.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Makarius
On 21/10/2018 17:34, Lars Hupel wrote:
>> On an El Capitan system, this produces the following error:
> 
> The problem can alternatively be solved by installing Homebrew's stack
> version and declaring
> 
> ISABELLE_STACK="/usr/local/bin/stack"
> 
> in ~/.isabelle/etc/settings.

Can you actually explain the problem and its solution?


Makarius



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev