[isabelle-dev] Mail on build failures

[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 could get sent to the [isabelle-dev] or a new [isabelle-ci]
mailing list.

For afptest, the current scheme probably works well. I can try to
replicate it, but it's going to take me a while.

Opinions?

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

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

[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 over multiple machines, since 
that isn't supported by "isabelle build". This is generally helpful – 
even if we get better hardware – because distributing jobs is trivial 
with Jenkins and there's no reason we shouldn't. The shorter the build 
time, the better.


Some years ago we were in a similar situation of outdated hardware, and 
Isabelle + AFP sessions growing beyond feasibility.  So we started to 
speculate towards distributed "make".


When Isabelle "build" took over in 2012, the multicore support of Poly/ML
+ Isabelle/ML was already so advanced that the question was irrelevant.
A full test of Isabelle + AFP required less than 1h on a plain and basic
2 * 4 core machine (macbroy2).

Now we have much bigger Isabelle + AFP sessions, and still the same old 
hardware.



Clustering weak nodes always requires more administrative efforts than 
just one or two fat nodes without special tricks.




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 full hypersearch over Isabelle + AFP confirms that the documentation in 
the "system" manual is still correct:


  \<^descr>[@{setting_def ML_SYSTEM_POLYML}\\<^sup>*\] is
  \<^verbatim>\true\ for @{setting ML_SYSTEM} values derived
  from Poly/ML, as opposed to SML/NJ where it is empty. This is
  particularly useful with the build option @{system_option condition}
  (\secref{sec:system-options}) to restrict big sessions to something that
  SML/NJ can still handle.


Concerning what "SML/NJ can still handle", see also 
https://bitbucket.org/isabelle_project/isabelle-release/commits/a4e6ea45f416


That commit is only on the isabelle-release repository.  It will come back 
via merge in something like 2 weeks.



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

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

[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
> ISABELLE_GHC/ISABELLE_OCAMLC etc. for Codegenerator_Test

This is also done now. For Haskell, it immediately uncovered a problem:

  

Uint.hs:15:48:
Ambiguous occurrence `Word'
It could refer to either `Uint.Word', defined at Uint.hs:12:1
  or `Data.Word.Word',
 imported from `Prelude' at Uint.hs:3:8-11
 (and originally defined in `GHC.Types')
### theory "Impl_Uv_Set"
### 14.656s elapsed time, 16.840s cpu time, 0.572s GC time
*** Failed to load theory "GenCF" (unresolved "Impl_Uv_Set")
*** Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls
-XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir
build -e "" Generated_Code.hs
*** At command "export_code" (line 384 of
"~~/afp/thys/Collections/GenCF/Impl/Impl_Uv_Set.thy")

This is a legitimate failure, using GHC 7.10.3. The other build machines
use the (outdated) GHC 7.8.x series. Shall I downgrade GHC or would
someone (Florian, Peter?) fix the compilation problem?

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

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

[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 proposed that the last time 10 
> years ago.

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

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

[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 isn't supported by "isabelle build". This is generally helpful –
even if we get better hardware – because distributing jobs is trivial
with Jenkins and there's no reason we shouldn't. The shorter the build
time, the better.

> For regular batch tests in the style of "isatest", the main purpose is
> to accumulate accurate timing information, and preserve that in a simple
> format over a long time.  This has been forgotten in recent years, since
> measurements have become more and more messed up.  So performance-wise, we
> are flying blind, especially for AFP.

I can't yet say with confidence that we now have a setup with reliable
performance numbers. In a couple of days I will look at the numbers to
get an idea of their variance.

> A related question is what to do with SML/NJ and the ML_SYSTEM_POLYML
> variable.  For the Isabelle2016 release, I've tried to build everything
> with SML/NJ as usual, but many sessions failed, even just HOL-Library.
> 
> We could discontinue ML_SYSTEM_POLYML and merely test the "HOL" session
> for SML/NJ.
> 
> Or we could discontinue SML/NJ altogether.  I proposed that the last
> time 10 years ago.

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?

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

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

[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
../cm/util/safeio.sml:30.11
../compiler/TopLevel/interact/evalloop.sml:44.55

Settings are:

ML_SYSTEM=smlnj-110
ML_HOME="/usr/lib/smlnj/bin"


/usr/lib probably means that this is a "package" on the target system, and 
thus it is usually broken by default.


I've never used anything else than a manual build of SML/NJ from the 
official sources.  It usually works out of the box, unchanged for many 
decades.




Interestingly enough, "isabelle build" doesn't complain. The error only
becomes apparent in the log file.


Total existence failure of the outermost ML executable can lead to 
problems with the Isabelle wrapper scripts.  The same can happen for 
Poly/ML under certain circumstances.


We are normally testing Isabelle applications, not ML installations.


Nonetheless, I hope to make this more robust at some point, by replacing 
the shell scripts with Isabelle/Scala.  Not having SML/NJ anymore could 
accelerate that move.



Makarius

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

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

[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:


Standard ML of New Jersey v110.76 [built: Sun Jun 29 03:29:51 2014]
!* unable to process `' (unknown extension `')
- [autoloading]

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
 ../cm/util/safeio.sml:30.11
 ../compiler/TopLevel/interact/evalloop.sml:44.55



Settings are:

ML_SYSTEM=smlnj-110
ML_HOME="/usr/lib/smlnj/bin"
ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
"$HEAP_SUFFIX")


Interestingly enough, "isabelle build" doesn't complain. The error only
becomes apparent in the log file.

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

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

[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 make Jenkins store them into
some database, but will need to investigate further.


* installing compilers and setting the various
ISABELLE_GHC/ISABELLE_OCAMLC etc. for Codegenerator_Test


This is also done now. For Haskell, it immediately uncovered a problem:

   

Uint.hs:15:48:
 Ambiguous occurrence `Word'
 It could refer to either `Uint.Word', defined at Uint.hs:12:1
   or `Data.Word.Word',
  imported from `Prelude' at Uint.hs:3:8-11
  (and originally defined in `GHC.Types')
### theory "Impl_Uv_Set"
### 14.656s elapsed time, 16.840s cpu time, 0.572s GC time
*** Failed to load theory "GenCF" (unresolved "Impl_Uv_Set")
*** Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls
-XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir
build -e "" Generated_Code.hs
*** At command "export_code" (line 384 of
"~~/afp/thys/Collections/GenCF/Impl/Impl_Uv_Set.thy")

This is a legitimate failure, using GHC 7.10.3. The other build machines
use the (outdated) GHC 7.8.x series. Shall I downgrade GHC or would
someone (Florian, Peter?) fix the compilation problem?

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


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

[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[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
Needham_Schroeder_No_Attacker_Example
Needham_Schroeder_Guided_Attacker_Example
Needham_Schroeder_Unguided_Attacker_Example
HOL-Record_Benchmark
Record_Benchmark

Most of these appear to be benchmarks of some sort. Currently, the new
CI setup doesn't set the ISABELLE_FULL_TEST flag. I think it would be
useful to run those, but I'd like to split them up into a separate run
so that they can be executed in parallel to the regular makeall. To that
end, I would suggest grouping these sessions in 'full'. I could then run

  export ISABELLE_FULL_TEST=true
  isabelle build -v -g full

(In a similar fashion, I run 'slow' sessions separately from the others.)

If nobody complains, I'll add the group.

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

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

[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
   Find_Unused_Assms_Examples
   Needham_Schroeder_No_Attacker_Example
   Needham_Schroeder_Guided_Attacker_Example
   Needham_Schroeder_Unguided_Attacker_Example
HOL-Record_Benchmark
   Record_Benchmark

Most of these appear to be benchmarks of some sort. Currently, the new
CI setup doesn't set the ISABELLE_FULL_TEST flag. I think it would be
useful to run those, but I'd like to split them up into a separate run
so that they can be executed in parallel to the regular makeall. To that
end, I would suggest grouping these sessions in 'full'. I could then run

 export ISABELLE_FULL_TEST=true
 isabelle build -v -g full

(In a similar fashion, I run 'slow' sessions separately from the others.)


We have accumulated a fair amount of complication here. There was a time 
when it was even more complication, but we managed to recover from it by 
substantial improvements of Poly/ML (multithreading and parallel GC), 
elimination of "make", and introduction of up-to-date hardware.



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.


For regular batch tests in the style of "isatest", the main purpose is to 
accumulate accurate timing information, and preserve that in a simple 
format over a long time.  This has been forgotten in recent years, since 
measurements have become more and more messed up.  So performance-wise, we

are flying blind, especially for AFP.


A related question is what to do with SML/NJ and the ML_SYSTEM_POLYML 
variable.  For the Isabelle2016 release, I've tried to build everything 
with SML/NJ as usual, but many sessions failed, even just HOL-Library.


We could discontinue ML_SYSTEM_POLYML and merely test the "HOL" session 
for SML/NJ.


Or we could discontinue SML/NJ altogether.  I proposed that the last time 
10 years ago.



Here are also the canonical meta questions:

  * What is really required?

  * What is the simplest way to achieve that?

  * What can be discontinued?


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