[isabelle-dev] Mail on build failures

2016-01-31 Thread Lars Hupel
Dear Isabelle and AFP developers, currently, isatest and afptest send build failure notifications to specific people specified in a global list (isatest) or per entry (afptest). How should this work in the future? For isatest, I don't think this global list makes much sense. Rather failures

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Makarius
On Sun, 31 Jan 2016, Lars Hupel wrote: The "ISABELLE_FULL_TEST" variable and "slow" group are somehow adhoc measures to get meaningful interactive tests, without wasting too much time. It probably makes sense to imitate that for "testboard" setups. The idea is to distribute the build load

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

2016-01-31 Thread Lars Hupel
> * archival of the build logs As a temporary solution, I have now configured Jenkins to retain all build logs. I've found some pointers how to make Jenkins store them into some database, but will need to investigate further. > * installing compilers and setting the various >

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Lawrence Paulson
Maybe it’s time. They’ve not made it better, and it seems pretty hopeless now. Larry > On 31 Jan 2016, at 13:41, Makarius wrote: > > We could discontinue ML_SYSTEM_POLYML and merely test the "HOL" session for > SML/NJ. > > Or we could discontinue SML/NJ altogether. I

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Lars Hupel
> The "ISABELLE_FULL_TEST" variable and "slow" group are somehow adhoc > measures to get meaningful interactive tests, without wasting too much > time. It probably makes sense to imitate that for "testboard" setups. The idea is to distribute the build load over multiple machines, since that

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Makarius
On Sun, 31 Jan 2016, Lars Hupel wrote: unexpected exception (bug?) in SML/NJ: Io [Io: openIn failed on "/build/smlnj-tOOpSy/smlnj-110.76/sml.boot.x86-unix/smlnj/basis/.cm/x86-unix/basis.cm", No such file or directory] raised at: Basis/Implementation/IO/bin-io-fn.sml:617.25-617.71

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Lars Hupel
> Building with SML/NJ configuration is trivial. It would be "just another > job" in Jenkins. I'd just need to know about what to build precisely. > Can you explain to me what the ML_SYSTEM_POLYML variable means? I was speaking too early. Here's what I get when trying to build Pure with SML/NJ:

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

2016-01-31 Thread Andreas Lochbihler
Hi Lars, The theory Uint comes from Native_Word. I'll have a look and see whether this can be fixed. Andreas On 31/01/16 22:21, Lars Hupel wrote: * archival of the build logs As a temporary solution, I have now configured Jenkins to retain all build logs. I've found some pointers how to

[isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Lars Hupel
As of 527488dc8b90, there are five sessions which contain theories that are only processed under ISABELLE_FULL_TEST=true: HOL-ex Sudoku HOL-Datatype_Examples Brackin IsaFoR Misc_N2M HOL-Word-SMT_Examples SMT_Tests HOL-Quickcheck_Benchmark Find_Unused_Assms_Examples

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Makarius
On Sun, 31 Jan 2016, Lars Hupel wrote: As of 527488dc8b90, there are five sessions which contain theories that are only processed under ISABELLE_FULL_TEST=true: HOL-ex Sudoku HOL-Datatype_Examples Brackin IsaFoR Misc_N2M HOL-Word-SMT_Examples SMT_Tests HOL-Quickcheck_Benchmark