[isabelle] Loading theories imported with Haskabelle

Hi there,

After making a few steps forward from my last email yesterday, with help of
Makarius, I got no more error messages of exception size raised. Now I'm
the 2016-1 version with Isabelle/ML 64bit version.

Now I'm bringing a new question hoping for some feedback, as what I'm doing
right now is new for me and I'm still learning.

I'm using haskabelle to translate some haskell code and what I have so far
a bunch of datatypes, written in overall 280 lines, and as an example, the
most complicated bit of formal spec, obtained through haskabelle is
like the following function definition that involves four or five other
functions, in a total of 95 lines.

function  fun1 :: "some -> inputs -> and -> outputs"
               and  fun2 :: "some -> inputs -> and -> outputs" and
               and  fun3 :: "some -> inputs -> and -> outputs" and
               and  fun4 :: "some -> inputs -> and -> outputs" and
"they call each other in some parts"
| "fun1 calls fun2"
| "fun2 calls fun3"
| "fun3 calls fun4"
| "fun4 calls fun1"

I know that as they call each other they can't be declared one after each
other. So, my question is.. Is there any way of splitting those function
definitions? Basically, this is what is taking most of the time, like
minutes with the pieces in pink/purple, and high speed fan working in my
laptop. I presume that even if I use the cloud service from college, it
still be a hard work.

I tried to shrink a bit the datatypes and reduce the amount of cases for
testing purposes, but still, it is being really hard to get feedback from

Is there something else I could do that would help me with this?

Many thanks.


Artur Oliveira Gomes
PhD Student - SCSS - Trinity College Dublin
Professor - Sistemas de InformaÃÃo - UFMS

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.