Re: [isabelle-dev] Unable to push to Isabelle reop
Macbroy20 works for me. Thanks, Florian and Alex. Clemens Quoting Alexander Krauss kra...@in.tum.de: Quoting Clemens Ballarin balla...@in.tum.de: [...] pushing to ssh://balla...@macbroy2.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle searching for changes remote: Not trusting file /mnt/nfsbroy/home/isabelle-repository/repos/isabelle/.hg/hgrc from untrusted user wenzelm, group isabelle remote: abort: could not lock repository /home/isabelle-repository/repos/isabelle: Permission denied abort: unexpected response: empty string I wonder whether this is related to the recently 'broken' repository, or are my permissions degrading? This may be a side effect of Makarius' re-cloning. Maybe try another host as gateway? macbroy2 has a somewhat non-standard setup. Do you get the same result when using, e.g. macbroy20? Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Unable to push to Isabelle reop
On Thu, 16 Aug 2012, Alexander Krauss wrote: Quoting Clemens Ballarin balla...@in.tum.de: [...] pushing to ssh://balla...@macbroy2.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle searching for changes remote: Not trusting file /mnt/nfsbroy/home/isabelle-repository/repos/isabelle/.hg/hgrc from untrusted user wenzelm, group isabelle remote: abort: could not lock repository /home/isabelle-repository/repos/isabelle: Permission denied abort: unexpected response: empty string I wonder whether this is related to the recently 'broken' repository, or are my permissions degrading? This may be a side effect of Makarius' re-cloning. Maybe try another host as gateway? macbroy2 has a somewhat non-standard setup. Do you get the same result when using, e.g. macbroy20? macbroy2 might even be one of the sources for the decay, it has a very odd NFS configuration due to Apple. Franz Huber has recently recommended the following machines for external logins: lxlabbroy1..15 macbroy20..29 Although he cannot guarantee continous availability of these relatively old and fragile systems. I usually have my own indirection via .ssh/config or local /etc/hosts to make an alias that can be easily switched on demand, without editing too many hgrc files. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] download-components
On Wed, 15 Aug 2012, Tjark Weber wrote: On Wed, 2012-08-15 at 13:22 +0200, Makarius wrote: I will have to take a look at the component business again soon, to simplify it further and remove features and clones of other Isabelle scripts. Great. I've now turned download_components into an isabelle (Admin) tool (cf. 01d1734f779d), as you suggested. Feel free to make further refinements. So I have to follow one more change to get the work done eventually. This is not very productive. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] http://isabelle.in.tum.de/testboard/
produces class 'mpatch.mpatchError'Python 2.7.3: /usr/bin/python2.7 Thu Aug 16 17:59:20 2012 A problem occurred in a Python script. Here is the sequence of function calls leading up to the error, in the order they occurred. ... Both with firefox and safari. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Java 7 update 6
That is indeed good news. Would it be appropriate to advise users to upgrade, is there are no immediate need? Larry On 16 Aug 2012, at 16:39, Makarius wrote: Oracle has released the important Java 7u6 yesterday, see also http://www.oracle.com/us/corporate/press/1735645 It means much more uniformity of the 3 plaform families: Linux, Mac OS X, Windows. For example, Mac OS X users now get the IsabelleTextBold font by default without modifying the local system. It also means that Chinese glyphs are *unavailable* in a uniform manner, because Apple's unofficial glyph substitution for the JVM is no longer used. I generally expect thing to become better, since problems show up more uniformly and can be addressed more easily. Isabelle/b19ba23e70c5 already uses jdk-7u6 together with jedit_build-20120813. This is a mandatory update of components, although just plain Isabelle/Scala (e.g. isabelle build) still happens to work with JDK 1.6 if that happens to be used by a side-entry. Makarius ___ 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] Java 7 update 6
On Thu, 16 Aug 2012, Lawrence Paulson wrote: That is indeed good news. Would it be appropriate to advise users to upgrade, is there are no immediate need? They can't. It requires a number of subtle changes in other components. In the past few weeks I've worked towards that on the isabelle repository, such that today the change looked mostly trivial. We have more and more the situation of no serviceable parts inside Isabelle, which means that the fully integrated system has become so complex that users cannot do much maintenance themselves. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] http://isabelle.in.tum.de/testboard/
On Thu, 16 Aug 2012, Tobias Nipkow wrote:
produces
class 'mpatch.mpatchError' Python 2.7.3: /usr/bin/python2.7
Thu Aug 16 17:59:20 2012
A problem occurred in a Python script. Here is the sequence of function calls
leading up to the error, in the order they occurred.
...
The end of Python vomiting has this:
class 'mpatch.mpatchError': patch cannot be decoded
args = ('patch cannot be decoded',)
message = 'patch cannot be decoded'
This is the same dropout that we've had on
http://isabelle.in.tum.de/repos/isabelle last week.
It could be an NFS corruption of the repository, or just the server
feeling too hot. I've no real idea.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Java 7 update 6
On Thu, 16 Aug 2012, Makarius wrote: On Thu, 16 Aug 2012, Lawrence Paulson wrote: That is indeed good news. Would it be appropriate to advise users to upgrade, is there are no immediate need? They can't. It requires a number of subtle changes in other components. In the past few weeks I've worked towards that on the isabelle repository, such that today the change looked mostly trivial. One more thing: A latest version always involves some follow-up work to iron out new issues -- days, weeks, months. We shall see. For example: TAB completion in jEdit/Sidekick used to work by pure accident on Linux so far, but not on Windows or Mac OS X. Now everybody is equal again. If any of the early adopters and testers on this list can tell me how to deal with it, I will be very grateful. (The jEdit guys might have found a solution on their 5.0pre1 development branch in the meantime, while we are on 4.5.2 official/stable.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] http://isabelle.in.tum.de/testboard/
On Thu, 16 Aug 2012, Alexander Krauss wrote: It could be an NFS corruption of the repository, or just the server feeling too hot. I've no real idea. This seems to be happening regularly now, which is really very annoying. The testboard is not the main repository; so far the problem did not occur again on the latter. I am still hoping that the main repository is clean. * Strip the broken revisions (after making a backup): cp -a . /some/backup/location hg strip -n REV (Note: This seems to fail with the newest version installed at some machines: here, strip also produces an exception. However, hg 2.1.1 installed at lxbroy10 works). The release notes for Mercurial 2.1.2 say that option -n (no backup) is now ignored, and it seems to have been discontinued later. What is its purpose here anyway? Generally, it is important to understand that hg strip is a non-monotonic single-user maintenance operation on the physical repository. It is a matter of last resort, in a situation where a single person is sent into the reactor to make some repairs after a meltdown, while everybody else is standing outside watching. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
