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

[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] Maintenance work on Jenkins VM

[Andreas Lochbihler]

Native_Word should work again in 203deaf5208d (see also 61aeecc4093d), both with GHC 7.8 
and GHC 7.10.


Andreas

On 01/02/16 08:32, Andreas Lochbihler wrote:

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 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]

> Native_Word should work again in 203deaf5208d (see also 61aeecc4093d),
> both with GHC 7.8 and GHC 7.10.

Build is still running, but looks like it's working again.

I'm pushing another item on my todo list: Print the relevant system
information (e.g. compiler versions) in the log.

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

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

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

[Lars Hupel]

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.

definitely possible, pending a Scala script which performs this:
.
Otherwise, we'd needlessly run HOL-Proofs in the AFP testboard.

We'd also need to find a location for the repository.

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

[Lars Hupel]

Update:

> - running makeall and AFP (without "slow" sessions) on every push to
> Isabelle
> - running slow sessions nightly
> - utilize 4 workers (8 cores, 64 GB each) from the LRZ
> - running AFP (without "slow" sessions) on every push to AFP
> - running everything on every push to testboard

All of that should be working now. See the full glory here:

  

There are four major jobs, each of which may have minor jobs:

  - isabelle-repo-checkin
- isabelle-repo-makeall
- isabelle-repo-afp
  - isabelle-repo-nightly-slow
  - testboard-checkin
- testboard-makeall
- testboard-afp
  - afp-repo-checkin
- afp-repo-afp

The first name part is the name of the "master" repository. Major jobs
containing "-checkin" get triggered on every push; those containing
"-nightly" get triggered once daily. "-slow" means building only the
sessions tagged "slow". All other jobs exclude those sessions. (In the
current setup, that means that testboard doesn't run slow sessions at all.)

Example: Someone pushes to the Isabelle repository. The
"isabelle-repo-checkin" detects this and kicks off a build with ID #5.
It then runs the minor jobs "isabelle-repo-makeall" and
"isabelle-repo-afp" in parallel, both with ID #5 as well. If either of
the minor jobs fails, the major job fails, too.

About the hardware: There are currently 4 worker machines. Each job can
take from 1-6 hours there (slowest: "isabelle-repo-nightly-slow" with
5h20m, fastest: "isabelle-repo-makeall" with 1h09m). There's currently a
problem with LRZ' VM management interface, but once that's fixed, I'll
add 4 more workers.

(NB: We don't have better hardware just yet, but I figured to better get
this running in time for post-release mode.)

Still missing in the setup:
* cross-platform/cross-parameter testing
* archival of the build logs
* time series

In any case, we can start thinking seriously about sunsetting isatest
and afptest now.

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

[Dmitriy Traytel]

Hi Lars,

great to hear!

What about having an additional afp_testboard repository where one could also 
push -f changes. I am particularly interested in “slow” sessions there.

Thanks for your work,
Dmitriy

> On 30 Jan 2016, at 12:51, Lars Hupel  wrote:
> 
> Dear list,
> 
> I'm currently performing maintenance work on the Jenkins VM. The
> following things are planned for today:
> 
> - running makeall and AFP (without "slow" sessions) on every push to
> Isabelle
> - running slow sessions nightly
> - utilize 4 workers (8 cores, 64 GB each) from the LRZ
> 
> I've already tested the above configuration locally and am currently
> applying it to the production CI server.
> 
> If that works out fine, I will additionally deploy the following jobs:
> 
> - running AFP (without "slow" sessions) on every push to AFP
> - running everything on every push to testboard
> 
> 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

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

[Lars Hupel]

> Still missing in the setup:
> * cross-platform/cross-parameter testing
> * archival of the build logs
> * time series

I forgot:

* installing compilers and setting the various
ISABELLE_GHC/ISABELLE_OCAMLC etc. for Codegenerator_Test
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev