As far as I understand, the reason that GHC does not construct such proofs is
that it can't express them in its internal proof language (System FC).
Iavor is quite right
It seems to me that it should be fairly straight-forward to extend FC to
support this sort of proof, but I have not been
On Tue, Jan 1, 2013 at 3:41 PM, Brandon Allbery allber...@gmail.com wrote:
On Tue, Jan 1, 2013 at 9:13 AM, Bernhard Urban lew...@gmail.com wrote:
The main issue: The GHC runtime relies on glibc
I have to assume this is not meant literally, because ghc works on OS X and
*BSD.
Right. I was
On Wed, Jan 02, 2013 at 05:21:43PM +, Simon Peyton-Jones wrote:
Serge
That's odd. I've tried with both 7.6 and HEAD, and both fail on T_cubeext
thus:
T_cubeext.hs:102:10:
Overlapping instances for LinSolvRing (UPol k)
arising from a use of `upEucRing'
Matching
| The solution is to add (EuclideanRing k) to the type sig of cubicExt.
| Then it compiles all the way up to the top.
|
| But the DoCon declares
|class (EuclideanRing a, FactorizationRing a) = Field a
|
| (EuclideanRing is a superclass for Field),
| and the test
I agree with Iavor that it is fairly straight-forward to extend FC to
support FD-style type improvement. In fact, I've formalized such a proof
language in a PPDP'06 paper:
Extracting programs from type class proofs
(type improvement comes only at the end)
Similar to FC, coercions (proof terms)
On Wed, Jan 02, 2013 at 08:23:37PM +, Simon Peyton-Jones wrote:
| The solution is to add (EuclideanRing k) to the type sig of cubicExt.
| Then it compiles all the way up to the top.
|
| But the DoCon declares
|class (EuclideanRing a, FactorizationRing a) = Field a
I made a second mistake. I meant (LinSolvRing (UPol k)). Apologies.
| I don't know why 7.4 accepts it, but I'm not inclined to investigate...
| looks like a bug in 7.4.
|
| ghc-7.4.1 may use a special trick, but is correct.
I don't understand your explanation. What is wrong with this
I'm trying to build ghc-7.4.1 using ghc-7.4.1 on my raspberry pi (armv6l)
and I get the following error:
inplace/bin/ghc-stage1 -H32m -O-package-name ghc-prim-0.2.0.0
-hide-all-packages -i -ilibraries/ghc-prim/. -ilibraries/ghc-prim/dist-install/build
My random guess is that /tmp is mounted using tmpfs (aka a RAM drive)
and it got full. Try remounting /tmp to use the sdcard instead ?
On Wed, Jan 2, 2013 at 7:32 PM, rocon...@theorem.ca wrote:
I'm trying to build ghc-7.4.1 using ghc-7.4.1 on my raspberry pi (armv6l)
and I get the following
Thanks for your help, but unfortunately this isn't the issue
Filesystem Size Used Avail Use% Mounted on
/dev/sda2 924G 584G 294G 67% /tmp
So there is pleanty of room on temp.
BTW, I also tried building it twice and I got the same error at the same
place.
On Wed, 2 Jan 2013,
Some further information it seems that llc is segfaulting:
pi@raspberrypi /tmp/ghc-7.4.1 $ llc -O3 -relocation-model=static /tmp/ghc7189_0/ghc7189_0.bc -o /tmp/ghc7189_0/ghc7189_0.lm_s
Stack dump:
0. Program arguments: llc -O3 -relocation-model=static /tmp/ghc7189_0/ghc7189_0.bc -o
11 matches
Mail list logo
