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

[isabelle-dev] Maintenance work on Jenkins VM

[Lars Hupel]

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