Re: [isabelle-dev] Code check failed for SML on lxbroy10

2018-02-09 Thread Makarius 
On 06/02/18 15:09, Fabian Immler wrote:
> 
> Stripping the problem down, I realized that this has nothing to do with 
> Native_Word, because the same issue arises with the following theory:
> 
> theory Test imports HOL.Code_Generator begin
> export_code Code_Generator.holds checking SML
> end
> 
> The log says:
> 
> Loading theory "Test.Test"
> /home/immler/.isabelle/contrib/jdk-8u162/x86_64-linux/jre/bin/java: symbol 
> lookup error: /usr/lib64/libhogweed.so.4: undefined symbol: __gmpn_cnd_add_n

That is a conflict of libgmp as bundled with our polyml component and
the one already installed on the system. It occurs here, because
LD_LIBRARY_PATH is augmented before starting the poly process, and then
java is started recursively for the generated code tests. With x86-linux
there is no problem, because java is an x86_64 process and ignores the
conflicting x86-linux libgmp.

Moreover, the problem appears to be specific to the Gentoo installation
of lxbroy10. I've never seen it on the many Ubuntu machines that I
routinely use for testing x86-linux and x86_64-linux.


In Isabelle/8b19a8a7f029 I have now changed the situation as follows:

  * polyml-5.7.1-1 no longer requires any local changes to
LD_LIBRARY_PATH (Linux) nor DYLD_LIBRARY_PATH (macOS). Instead the
library path is baked into the poly executable -- using funny tricks
that I did not know before, see
http://isabelle.in.tum.de/repos/isabelle/annotate/8b19a8a7f029/src/Pure/Admin/build_polyml.scala#l25
http://isabelle.in.tum.de/repos/isabelle/annotate/8b19a8a7f029/src/Pure/Admin/build_polyml.scala#l172

  * polyi is no longer needed: plain poly works as standalone executable

  * polyc should now work properly (it was never used for Isabelle)

  * libgmp is now provided for x86_64-darwin as well (before it was only
available for Linux and Windows); libgmp for x86-darwin still does not
work, because I don't know how to build it.

The explanations for libgmp on x86_64-darwin are in
polyml-5.7.1-1/README. If anybody figures out how to build the shared
library for x86-darwin, we can probably use it in the polyml component
to fill this remaining discontinuity.


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

Re: [isabelle-dev] lxisabelle/lxcisa* maintenance

2018-02-09 Thread Makarius 
On 09/02/18 18:05, Lars Hupel wrote:
> 
> on Sunday, I will have to perform necessary maintenance. The following
> services may be interrupted and/or unavailable:
> 
> - (shell access to) lxcisa0
> 
> In particular, I recommend to not start any new jobs on lxcisa0, as I
> might have to stop them. Please try to finish existing jobs by Sunday
> 10am CET. Jenkins jobs will be disabled already on Saturday evening.

Thanks for taking care of this important machine. Without it, Isabelle +
AFP maintenance would be very difficult.

Is it possible to install emacs on it?


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

[isabelle-dev] lxisabelle/lxcisa* maintenance

2018-02-09 Thread Lars Hupel 

Dear users of lxisabelle/lxcisa*,

on Sunday, I will have to perform necessary maintenance. The following 
services may be interrupted and/or unavailable:


- Jenkins
- (shell access to) lxcisa0

In particular, I recommend to not start any new jobs on lxcisa0, as I 
might have to stop them. Please try to finish existing jobs by Sunday 
10am CET. Jenkins jobs will be disabled already on Saturday evening.


Regular operation continues on Monday.

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