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

2018-11-08 Thread Makarius
This is the updated situation according to Isabelle/c1a27fce2076:


*** System ***

* Support for managed installations of Glasgow Haskell Compiler and
OCaml via the following command-line tools:

  isabelle ghc_setup
  isabelle ghc_stack

  isabelle ocaml_setup
  isabelle ocaml_opam

The global installation state is determined by the following settings
(and corresponding directory contents):

  ISABELLE_STACK_ROOT
  ISABELLE_STACK_RESOLVER
  ISABELLE_GHC_VERSION

  ISABELLE_OPAM_ROOT
  ISABELLE_OCAML_VERSION

After setup, the following Isabelle settings are automatically
redirected (overriding existing user settings):

 ISABELLE_GHC

 ISABELLE_OCAML
 ISABELLE_OCAMLC

The old meaning of these settings as locally installed executables may
be recovered by purging the directories ISABELLE_STACK_ROOT /
ISABELLE_OPAM_ROOT.



I have also started experimenting with the following in
$ISABELLE_HOME_USER/etc/settings:

  ISABELLE_STACK_ROOT="$HOME/.stack"
  ISABELLE_OPAM_ROOT="$HOME/.opam"

The Isabelle scripts should ensure that the specified versions are used,
independently of other versions that a user might have installed already.

In any case, both "stack" and "opam" stack-up considerable material: it
is easy to fill 5-15 GB of disk space after working some time. Only
docker requires even more space.


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-11-08 Thread Bertram Felgenhauer
Makarius wrote:
> On 08/11/2018 14:59, Bertram Felgenhauer wrote:
> >>
> >> I've misunderstood the problem. You intend to invoke old-style
> >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> >> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
> > 
> > This may be premature, but I foresee that now that `isabelle ghc`
> > and `isabelle ghci` exist, we will have scripts that use them.
> 
> There is indeed some confusion here.
> 
> My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained
> by the odd recursive setup: in the stack situation, $ISABELLE_GHC points
> to lib/Tools/ghc, and some mistake in the configuration could lead to
> infinite recursion of sub-processes (potential bombing of the OS).
> 
> It is probably better to leave the meaning of ISABELLE_GHC (and
> ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle
> ghc" tool entry points: these auxiliary scripts should go into
> $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular
> Isabelle tools.

Sounds good to me.

Cheers,

Bertram

___
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-11-08 Thread Makarius
On 08/11/2018 14:59, Bertram Felgenhauer wrote:
>>
>> I've misunderstood the problem. You intend to invoke old-style
>> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
>> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
> 
> This may be premature, but I foresee that now that `isabelle ghc`
> and `isabelle ghci` exist, we will have scripts that use them.

There is indeed some confusion here.

My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained
by the odd recursive setup: in the stack situation, $ISABELLE_GHC points
to lib/Tools/ghc, and some mistake in the configuration could lead to
infinite recursion of sub-processes (potential bombing of the OS).

It is probably better to leave the meaning of ISABELLE_GHC (and
ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle
ghc" tool entry points: these auxiliary scripts should go into
$ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular
Isabelle tools.

I have now also learned that "ghci" is just "ghc --interactive", so
there is no point to treat it too prominently.


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-11-08 Thread Bertram Felgenhauer
Makarius wrote:
> On 08/11/2018 11:30, Bertram Felgenhauer wrote:
> > Makarius wrote:
> >> Nonetheless, it is still possible to use "isabelle ghc" without stack:
> >> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
> >> Isabelle settings mechanism to override ISABELLE_GHC with the
> >> stack-based tools.
> > 
> > After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
> > a missing GHC setup, since there's no fallback on a custom
> > $ISABELLE_GHC. I've added such a fallback in the attached patch,
> > does that look reasonable?
> 
> I've misunderstood the problem. You intend to invoke old-style
> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.

This may be premature, but I foresee that now that `isabelle ghc`
and `isabelle ghci` exist, we will have scripts that use them.

> So just the usual question: What are remaining uses of this? Why not
> uninstall the "system ghc" and only use stack?

I don't think that the desire of using an existing ghc installation is
unusual. I'm not sure how common maintaining a ghc installation without
stack is these days, but ghc + cabal-install are still quite sufficient
for Haskell development. I don't care much about disk space, but I do
resent stack's propensity for downloading huge tarballs without even
prompting; my bandwidth is often limited. So I try hard to avoid that
particular tool.

> My impression is that up-to-date Haskell projects are all using stack by
> default.

My desire is to be able to override the default, not to change it.

Cheers,

Bertram
___
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-11-08 Thread Makarius
On 08/11/2018 12:16, Makarius wrote:
> On 08/11/2018 11:30, Bertram Felgenhauer wrote:
>> Makarius wrote:
>>> Nonetheless, it is still possible to use "isabelle ghc" without stack:
>>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
>>> Isabelle settings mechanism to override ISABELLE_GHC with the
>>> stack-based tools.
>>
>> After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
>> a missing GHC setup, since there's no fallback on a custom
>> $ISABELLE_GHC. I've added such a fallback in the attached patch,
>> does that look reasonable?
> 
> I've misunderstood the problem. You intend to invoke old-style
> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
> 
> So just the usual question: What are remaining uses of this? Why not
> uninstall the "system ghc" and only use stack? It should be possible to
> direct ISABELLE_STACK_ROOT to an existing stack setup, and worth sorting
> out remaining problems on that side.
> 
> My impression is that up-to-date Haskell projects are all using stack by
> default.

A remaining use of "unmanaged" ghc is actually ocaml: I would like to
keep these tools as uniform as possible, see also current a41f49148525.
Unfortunately, OPAM is not as advanced as stack yet, e.g. it does not
quite work on Windows so the Cygwin ocaml is still needed.

We could move the other way and discontinue the meaning of $ISABELLE_GHC
and $ISABELLE_OCAMLC as actual executables: the settings would merely
indicate the presence of these tools, e.g. for options [condition =
ISABELLE_GHC] in session ROOT entries.

It probably would require some changes of the Codegen setup, because
that wants to see a single environment variable instead of a
command-line fragment like "isabelle ghc" or "isabelle ocamlc".


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-11-08 Thread Makarius
On 08/11/2018 11:30, Bertram Felgenhauer wrote:
> Makarius wrote:
>> Nonetheless, it is still possible to use "isabelle ghc" without stack:
>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
>> Isabelle settings mechanism to override ISABELLE_GHC with the
>> stack-based tools.
> 
> After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
> a missing GHC setup, since there's no fallback on a custom
> $ISABELLE_GHC. I've added such a fallback in the attached patch,
> does that look reasonable?

I've misunderstood the problem. You intend to invoke old-style
$ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.

So just the usual question: What are remaining uses of this? Why not
uninstall the "system ghc" and only use stack? It should be possible to
direct ISABELLE_STACK_ROOT to an existing stack setup, and worth sorting
out remaining problems on that side.

My impression is that up-to-date Haskell projects are all using stack by
default.


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-11-08 Thread Bertram Felgenhauer
Makarius wrote:
> Nonetheless, it is still possible to use "isabelle ghc" without stack:
> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
> Isabelle settings mechanism to override ISABELLE_GHC with the
> stack-based tools.

After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
a missing GHC setup, since there's no fallback on a custom
$ISABELLE_GHC. I've added such a fallback in the attached patch,
does that look reasonable?

Cheers,

Bertram
diff -r 0a9688695a1b lib/Tools/ghc
--- a/lib/Tools/ghc Thu Nov 08 09:11:52 2018 +0100
+++ b/lib/Tools/ghc Thu Nov 08 11:25:55 2018 +0100
@@ -6,6 +6,8 @@
 
 if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then
   isabelle_stack ghc -- "$@"
+elif [ -n "$ISABELLE_GHC" ]; then
+  "$ISABELLE_GHC" "$@"
 else
   echo "Cannot execute ghc: missing Isabelle GHC setup" >&2
   exit 127
diff -r 0a9688695a1b lib/Tools/ghci
--- a/lib/Tools/ghciThu Nov 08 09:11:52 2018 +0100
+++ b/lib/Tools/ghciThu Nov 08 11:25:55 2018 +0100
@@ -6,6 +6,8 @@
 
 if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then
   isabelle_stack ghci "$@"
+elif [ -n "$ISABELLE_GHC" ]; then
+  "$ISABELLE_GHC" --interactive "$@"
 else
   echo "Cannot execute ghci: missing Isabelle GHC setup" >&2
   exit 127
___
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-11-07 Thread Makarius
On 07/11/2018 16:32, Bertram Felgenhauer wrote:
> Makarius wrote:
>> *** System ***
>>
>> * 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.
>>
>>
>> This refers to Isabelle/1722cc56d22e.
> 
> Is there a way to use a system ghc with `isabelle ghc` and
> `isabelle ghci`? I want to avoid the 145MB download and extra
> installation of ghc if possible.

The directory $ISABELLE_STACK_ROOT should be actually somewhat  bigger:
up to 5 GB for all the library modules. On Windows there is another
directory to take care of, according to "stack path programs".

I do prefer using up disk space and get a well-defined installation in
return. (I am presently working with someone building a Haskell-based
tool that is connected to Isabelle: the very first problem we had to
overcome was "cabal dependency hell". With stack it worked out nicely on
the spot, even on Windows and Mac OS X.)

Nonetheless, it is still possible to use "isabelle ghc" without stack:
you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
Isabelle settings mechanism to override ISABELLE_GHC with the
stack-based tools.


> Note in particular that setting ISABELLE_GHC now has a peculiar
> effect on `isabelle ghc`. Without the environment variable, the
> command complains:
> 
>   Cannot execute ghc: missing Isabelle GHC setup
> 
> However, if ISABELLE_GHC is set in $ISABELLE_HOME/etc/settings,
> then the same command starts downloading ghc via stack...

This should be more robust in current Isabelle/8bfa615ddde4 (the
relevant change is c911716d29bb).

You need to run "isabelle ghc_setup" once again to ensure that the extra
file "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS" is present --
otherwise it will fall back on old-style ISABELLE_GHC defaults despite
the presence of $ISABELLE_STACK_ROOT.


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-11-07 Thread Bertram Felgenhauer
Makarius wrote:
> *** System ***
> 
> * 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.
> 
> 
> This refers to Isabelle/1722cc56d22e.

Is there a way to use a system ghc with `isabelle ghc` and
`isabelle ghci`? I want to avoid the 145MB download and extra
installation of ghc if possible.

Note in particular that setting ISABELLE_GHC now has a peculiar
effect on `isabelle ghc`. Without the environment variable, the
command complains:

  Cannot execute ghc: missing Isabelle GHC setup

However, if ISABELLE_GHC is set in $ISABELLE_HOME/etc/settings,
then the same command starts downloading ghc via stack...

  > isabelle ghc
  Preparing to install GHC (tinfo6) to an isolated location.
  This will not interfere with any system-level installation.
  Preparing to download ghc-tinfo6-8.4.4 ...^C

Given the size of the download I find this unsatisfactory
(145 MB is still big for mobile plans.)

Cheers,

Bertram
___
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-22 Thread David Matthews

On 22/10/2018 14:05, Lars Hupel wrote:

The binary provided by Homebrew does not exhibit that problem. I have no
other information beyond that.


I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.

Interestingly enough, I get Poly/ML warnings of the form:

14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608)
failed (error code=3)
14:11:19 *** error: can't allocate region
14:11:19 *** set a breakpoint in malloc_error_break to debug



This is an Apple bug.  It produces this message if it can't allocate 
memory in certain situations.  That's a perfectly normal case and other 
operating systems just silently, and correctly, return zero from malloc. 
 Poly/ML deals with that.  Just ignore it.


David
___
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-22 Thread Makarius
On 22/10/2018 15:05, Lars Hupel wrote:
> 
> I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.
> 
> Interestingly enough, I get Poly/ML warnings of the form:
> 
> 14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608)
> failed (error code=3)
> 14:11:19 *** error: can't allocate region
> 14:11:19 *** set a breakpoint in malloc_error_break to debug
> 
> This happens during the build of "HOL-Decision_Procs", which succeeds
> regardless:
> 
> 14:11:19 Finished HOL-Decision_Procs (0:05:36 elapsed time, 0:10:40 cpu
> time, factor 1.91)

This is a normal feature of memory management on macOS.

After all these years, David Matthews might eventually want to look if
it is still required these days: for that he merely needs regular SSH
access to some test machine.


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-22 Thread Lars Hupel
> The binary provided by Homebrew does not exhibit that problem. I have no
> other information beyond that.

I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.

Interestingly enough, I get Poly/ML warnings of the form:

14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608)
failed (error code=3)
14:11:19 *** error: can't allocate region
14:11:19 *** set a breakpoint in malloc_error_break to debug

This happens during the build of "HOL-Decision_Procs", which succeeds
regardless:

14:11:19 Finished HOL-Decision_Procs (0:05:36 elapsed time, 0:10:40 cpu
time, factor 1.91)

The timestamp suggests that this happens close to the end of the
session; although no heap image has to be saved for that session.

I'll run some more experiments to figure out if this is spurious or not.
___
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


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 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
> * 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