Re: [isabelle-dev] Maintenance work on Jenkins VM

2016-02-17 Thread Dmitriy Traytel 
Hi Lars,

even without the slow sessions, this is of great help. Thanks!

My commit yesterday (isabelle/ae44f16dcea5) broke some AFP entries (because 
without the afp_testboard, I used to follow the "break it, fix it” philosophy 
w.r.t. AFP). I will repair those today.

Dmitriy

> On 17 Feb 2016, at 00:22, Lars Hupel  wrote:
> 
> Hi Dmitriy,
> 
>> What about having an additional afp_testboard repository where one 
>> could also push -f changes. I am particularly interested in “slow” 
>> sessions there.
> 
> for now I've created a job which runs everything but the slow sessions
> (so not quite what you wanted). The repository is:
> 
>  
> 
> Same rules as for the Isabelle testboard apply.
> 
> The corresponding job is:
> 
>  
> 
> Cheers
> Lars

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

Re: [isabelle-dev] SML/NJ

2016-02-17 Thread Florian Haftmann 
> With such a painfully slow and incomplete SML/NJ test, it is time to ask
> the canonical question:
> 
>   Are there remaining uses of SML/NJ, or can it be discontinued now?

I would also prefer a second usable ML implementation as reference, but
we have to face that only maintained platforms as Poly/ML remain
suitable for our needs.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.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

[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-17 Thread Lars Hupel 
Despite increasing the ML heap size with "-H 2000", the session
"Formula_Derivatives" is failing. The build VMs have 32 GB of RAM, so
that shouldn't be a problem. Here are the relevant environment variables:

ML_PLATFORM="x86-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86-linux"
ML_SYSTEM="polyml-5.6"
ML_OPTIONS="-H 2000"

What strikes me as odd is that it's always the same session.



Formula_Derivatives FAILED
(see also
/media/data/jenkins/.isabelle/heaps/polyml-5.6_x86-linux/log/Formula_Derivatives)

  sig
val check_eqv:
   WS1S.idx ->
 WS1S.nat ->
   ((WS1S.nat, WS1S.nat) WS1S.atomic, WS1S.orderb) WS1S.aformula ->
 (Presb.presb, unit) WS1S.aformula -> bool
type 'a set
  end
### theory "WS1S_Presburger_Equivalence"
### 11.322s elapsed time, 30.652s cpu time, 4.624s GC time
### Ignoring duplicate rewrite rule:
### find0 SO ?vr (Eq_Const ?v ?va ?vb) \ False
### Ignoring duplicate rewrite rule:
### find0 SO ?vr (Less ?v ?va ?vb) \ False
### Ignoring duplicate rewrite rule:
### find0 SO ?vr (Plus_FO ?v ?va ?vb ?vc) \ False
### Ignoring duplicate rewrite rule:
### find0 SO ?vr (Eq_FO ?v ?va ?vb) \ False
val it = (): unit
ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: \

2016-02-17 Thread Makarius 

*** Isar ***

* Command '\' is an alias for 'sorry', with different
typesetting. E.g. to produce proof holes in examples and documentation.


This refers to Isabelle/5e5a881ebc12.

It means that manuals, tutorials, slides etc. may be written more easily, 
without odd conditionals in LaTeX for the 'sorry' keyword.



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