It should now work again in 034a4d15b52e. Sorry for the trouble.
Andreas
PS: The error message is not so obscure if you look at the types. The left hand side talks
about hyper-naturals, the right hand side about nat.
On 12/03/15 13:56, Andreas Lochbihler wrote:
Hi Makarius,
You are right, t
Hi Makarius,
You are right, that's my fault. I'll look into it.
Andreas
On 12/03/15 12:48, Makarius wrote:
On Thu, 12 Mar 2015, Account Isatest wrote:
Unfinished session(s): HOL-NSA-Examples
Presumably this is caused by
changeset: 59676:4762c690a75c
parent: 59654:e327a9ae2d61
user:
On Thu, 12 Mar 2015, Account Isatest wrote:
Unfinished session(s): HOL-NSA-Examples
Presumably this is caused by
changeset: 59676:4762c690a75c
parent: 59654:e327a9ae2d61
user:Andreas Lochbihler
date:Tue Mar 10 16:35:14 2015 +0100
files: src/HOL/NSA/StarDef.thy
des
>> Test for platform mac-poly-M2 failed. Log file attached.
>> [...]
>> Unfinished session(s): Codegen, Codegen_Basics
>> Finished at Sat Jan 17 04:34:07 CET 2015
>> 2:52:32 elapsed time, 5:48:49 cpu time, factor 2.02
>
> I have repaired this already in Isabelle/4a0b34ef0563.
>
> The Codegen setu
On Sat, 17 Jan 2015, Account Isatest wrote:
Test for platform mac-poly-M2 failed. Log file attached.
[...]
Unfinished session(s): Codegen, Codegen_Basics
Finished at Sat Jan 17 04:34:07 CET 2015
2:52:32 elapsed time, 5:48:49 cpu time, factor 2.02
I have repaired this already in Isabelle/4a0b34
On Tue, 3 Apr 2012, Florian Haftmann wrote:
Am 02.04.2012 13:36, schrieb Florian Haftmann:
/mnt/home/isatest/isadist/Isabelle_02-Apr-2012/lib/scripts/run-polyml:
line 77: 27590 Killed "$POLY" -q $ML_OPTIONS
*** Code check failed for SML: "$ISABELLE_PROCESS" -r -q -u Pure
*** At command "expor
Am 02.04.2012 13:36, schrieb Florian Haftmann:
>>> /mnt/home/isatest/isadist/Isabelle_02-Apr-2012/lib/scripts/run-polyml:
>> line 77: 27590 Killed "$POLY" -q $ML_OPTIONS
>>> *** Code check failed for SML: "$ISABELLE_PROCESS" -r -q -u Pure
>>> *** At command "export_code" (line 17 of
>>> "~~/src/HOL
/mnt/home/isatest/isadist/Isabelle_02-Apr-2012/lib/scripts/run-polyml:
line 77: 27590 Killed "$POLY" -q $ML_OPTIONS
*** Code check failed for SML: "$ISABELLE_PROCESS" -r -q -u Pure
*** At command "export_code" (line 17 of
"~~/src/HOL/Codegenerator_Test/Generate.thy")
Does anybody understand th
On Mon, 2 Apr 2012, isat...@macbroy28.informatik.tu-muenchen.de wrote:
macbroy28
Isabelle version: 4c7548e7df86
Started at Mon Apr 2 00:24:47 CEST 2012 (polyml-5.3.0_x86-linux on ...
HOL-Library-Codegenerator_Test FAILED
ROOT.scala:7920: warning: match is not exhaustive!
missing combination
The failure is intended to be fixed with changeset 66ba67adafab and was
related to changes in 3f1d1ce024cb.
Lukas
On 10/20/2011 12:19 PM, Makarius wrote:
On Thu, 20 Oct 2011, Account Isatest wrote:
Test for platform at-poly-test failed. Log file attached.
[...]
3:02:39 elapsed time, 3:1
On Thu, 20 Oct 2011, Account Isatest wrote:
Test for platform at-poly-test failed. Log file attached.
[...]
3:02:39 elapsed time, 3:11:31 cpu time, factor 1.04
Logics HOL FAILED!
--- test FAILED --- Thu Oct 20 03:25:34 CEST 2011 --- macbroy21
Again the same failure. Here are t
11 matches
Mail list logo
