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:

   <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-...@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

Reply via email to