On Thu, 25 Sep 2014, Florian Haftmann wrote:
Ultimately there is this error:
### java.lang.NoClassDefFoundError: Generated_Code$Typerep (wrong name:
Generated_Code$typerep)
That looks like a general weakness of the code generator. I have
called the file-system
"insensible" in the log message
On Thu, 25 Sep 2014, Jasmin Christian Blanchette wrote:
Hi Florian,
Thanks for your input.
1. Increase the timeout from 3600 s to, e.g. 4800.
[...]
So, (1) is my opinion.
Unfortunately, that didn't do the trick (cf. 7f30ec82fe40,
e4d540c0dd57).
The change e4d540c0dd57 was my reaction
Florian: But you agree that it should be uniformaly "Sum" or "sum" for all
summation operators? Johannes already remarked on the discrepancy in your
proposal.
Tobias
On 25/09/2014 16:32, Florian Haftmann wrote:
a) for lists: sum_list (← listsum), prod_list (← listprod) b) for
multisets:
Hi Christian,
> theory Test
> imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"
> begin
>
> definition "foo m = do { m; return () }"
> definition "bar = foo (do { return (); return () })"
>
> export_code bar in Haskell
>
> the code for "bar" does not compile, since parenthesis are missing
> ar
>>> a) for lists: sum_list (← listsum), prod_list (← listprod)
>>> b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod)
>>> c) for finite sets: Sum (← setsum), Prod (← setprod)
>>
>> I assume a) means Sum_list and Prod_list?!
>>
>> Why Sum and not Sum_set in c)? Is the intention that the
> The situation involving ZF can go either way, as there are hardly any users.
>
> How are negative integers written in ZF now? Can one still write #-3 or is it
> $- #3?
The first one. Numerals in ZF are left as they are, *signed*.
Florian
--
PGP available:
http://home.informatik.tu
>> Ultimately there is this error:
>>
>> ### java.lang.NoClassDefFoundError: Generated_Code$Typerep (wrong name:
>> Generated_Code$typerep)
>>
>>
>> That looks like a general weakness of the code generator. I have
>> called the file-system
>> "insensible" in the log message, but such file-systems
Dear all,
while it is in principle nice that during Haskell code generation
do-blocks are mapped to Haskell do-blocks when using the heap monad of
Imperative HOL, it seems that the setup did not consider do-blocks as
arguments to functions. As a minimal example
theory Test
imports "~~/src/HO
Hi Florian,
Thanks for your input.
>> 1. Increase the timeout from 3600 s to, e.g. 4800.
[...]
> So, (1) is my opinion.
Unfortunately, that didn't do the trick (cf. 7f30ec82fe40, e4d540c0dd57).
Judging from the log file, it would appear to me that it's an instance of
multithreading divergenc
Hi Andreas,
> I would expect that if Jasmin's plugin manager is also used in the code
> generator, it would be easy to implement plugin selection for
> code_datatype, too.
interesting aspect. I will take this up after the discussion aroung the
future of interpretation.ML has been settled.
Cheer
> It doesn't seem like "subst_tac" had anything to do with it. I still have no
> idea about what made "HOL-Proofs" slower on "at-poly-e" beween September 13
> and 14. The log reveals nothing special, except a truncation at the end.
> (while processing "Predicate.thy"). My personal inclination wo
11 matches
Mail list logo
