[isabelle-dev] Maintenance work on Jenkins VM

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Mon Feb 1 08:32:54 CET 2016


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:
>
>    <https://ci.isabelle.systems/jenkins/job/isabelle-repo-afp/3/console>
>
> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>


More information about the isabelle-dev mailing list