Re: [isabelle-dev] [isabelle] new quick check expriment

2012-06-25 Thread Makarius

On Mon, 18 Jun 2012, Lukas Bulwahn wrote:


On 06/17/2012 06:36 PM, Florian Haftmann wrote:
Thanks. It asks me to set  'Environment variable ISABELLE_GHC '. So I 
uncomment the line 'ISABELLE_GHC="/usr/local/ghc/$ISABELLE_PLATFORM/ghc'


Now it gives me another error message "Compilation with GHC failed". Any 
suggestion ?


PS, I work in a mac version of Isabelle 2012

Maybe we have to find a way to provide ghc as a component also…


Although Haskell is an essential part for Quickcheck in Isabelle and it 
would simplify the installation process for Quickcheck, I am not in 
favour to provide ghc contributed with the Isabelle distribution.


By default the reflex is right to avoid managing even more components -- 
such things require substantantial resources for maintenance, which needs 
to be invested continously over a long time, not just once and for all.


Specifically for GHC --- after browsing 5min through 
http://hackage.haskell.org/platform/ --- my impression is that it is 
futile anyway.  This is a highly complex system, and these guys have their 
own multiplatform packaging already, which is hard to capture as part of 
the much more modest Isabelle distribution.



Providing GHC as a component might try to help to install GHC on the 
operating system, or could try to detect the path of GHC automagically, 
but I do not have a clear vision how this should work.


BTW, this automagic detection should have been disproven sufficiently now. 
It causes more problems than any good, when the system might pick up some 
arbitrary version of some program, or a different one, or none at all. We 
have had explicit user incidents already in the past, from the last 
left-overs of this old scheme.


For the next release, the very last occurrences of the infamous 
"choosefrom" bash function will hopefully disappear: only the ML system 
and Proof General are left, and the latter can already be configured 
properly as explicit component if the versions from the Isabelle2012 
distribution are used.  See again 
http://isabelle.in.tum.de/website-Isabelle2012/dist/



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


Re: [isabelle-dev] [isabelle] new quick check expriment

2012-06-18 Thread Lukas Bulwahn

On 06/17/2012 06:36 PM, Florian Haftmann wrote:

Thanks. It asks me to set  'Environment variable ISABELLE_GHC '. So I uncomment the 
line 'ISABELLE_GHC="/usr/local/ghc/$ISABELLE_PLATFORM/ghc'

Now it gives me another error message "Compilation with GHC failed". Any 
suggestion ?

PS, I work in a mac version of Isabelle 2012

Maybe we have to find a way to provide ghc as a component also…


Although Haskell is an essential part for Quickcheck in Isabelle and it 
would simplify the installation process for Quickcheck, I am not in 
favour to provide ghc contributed with the Isabelle distribution.
So GHC must be installed by the usual means of the operating system, 
e.g., through some package manager.
Providing GHC as a component might try to help to install GHC on the 
operating system, or could try to detect the path of GHC automagically, 
but I do not have a clear vision how this should work.



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


Re: [isabelle-dev] [isabelle] new quick check expriment

2012-06-17 Thread Florian Haftmann
> Thanks. It asks me to set  'Environment variable ISABELLE_GHC '. So I 
> uncomment the line 'ISABELLE_GHC="/usr/local/ghc/$ISABELLE_PLATFORM/ghc'
> 
> Now it gives me another error message "Compilation with GHC failed". Any 
> suggestion ?
> 
> PS, I work in a mac version of Isabelle 2012

Maybe we have to find a way to provide ghc as a component also…

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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