Re: [isabelle-dev] Automated testing questions
Hi Clemens, On 17.03.2013 20:43, Clemens Ballarin wrote: Dear Developers, What it the current best practice for testing my change to Isabelle? There used to be testboard, but I'm unsure how that evolved. Is there a similar service for testing my change to Isabelle against the AFP? I do use the testboard for bigger changesets. The description from http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01500.html (Developer-initiated tests) is AFAIK still up to date. Another alternative is to build everything on your own machine, which is feasible thanks to the wonders of PolyML 5.5 and the new build system. All you need to do is to clone the AFP repository, register it as a component (via init_component /path/to/AFP in etc/settings) and follow the instruction from http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02903.html . Also, which server should I use for pushing my changes to Isabelle so as to avoid repository trouble? lxbroy10 Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Automated testing questions
On Mon, 18 Mar 2013, Dmitriy Traytel wrote: Another alternative is to build everything on your own machine, which is feasible thanks to the wonders of PolyML 5.5 and the new build system. All you need to do is to clone the AFP repository, register it as a component (via init_component /path/to/AFP in etc/settings) and follow the instruction from http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02903.html That is a slightly dated mail of mine, it has been superseded by proper documentation in the system manual and the continously updated README_REPOSITORY file. The latter also points to isabelle-server.in.tum.de as canonical pull/push host for the conventional collection point of Isabelle changesets. If anything is missing or wrong in README_REPOSITORY, I ask once again to point it out, either on isabelle-dev or privately, and not to make unreliable/unmaintained clones of such important information. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] multiple weirdnesses
On Sat, 16 Mar 2013, Lawrence Paulson wrote: At d5c95b55f849 ~/isabelle/Repos/src/HOL: isabelle components -a ### Missing Isabelle component: /Users/lp15/.isabelle/contrib/jedit_build-20130104 Getting http://isabelle.in.tum.de/components/jedit_build-20130104.tar.gz; Unpacking /Users/lp15/.isabelle/contrib/jedit_build-20130104.tar.gz This brand-new file has a creation date of 14-June-2011 ! The jedit_build-20130104 component is from 04-Jan-2013 -- it did not change recently. This incident looks more like a drop-out of your local file-system. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Debugging low-level exceptions
On Sat, 16 Mar 2013, Florian Haftmann wrote:
Hi Alex,
What is the current (as of, say, d5c95b55f849) method for getting
exception traces? I am trying to debug a low-level exception such as
exception Match raised (line 287 of term.ML)
which happens somewhere below partial_function. Some years ago there
used to be Toplevel.debug flag, which would activate printing traces
of any top-level errors. The closest to this I found in the current
codebase is Runtime.debug : bool Unsynchronized.ref, but putting
ML {*
Runtime.debug := true;
*}
does not seem to have any effect (or I did not look in the right place).
you have to watch the »Raw output« buffer (via Plugins - Isabelle).
Toplevel.debug and Runtime.debug are the same flag, with slightly varying
purpose over the years, but now it is just for exception_trace wrapping
for Isar transactions.
The underlying PolyML.exception_trace works via low-level stdout, so the
Raw Output panel is indeed the way to see that in Isabelle/jEdit. One
also needs to guess what is the right trace, since it is not related to
formal document content --- just physical output on a side-channel.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] multiple weirdnesses
On Sat, 16 Mar 2013, Lawrence Paulson wrote: At d5c95b55f849 ~/isabelle/Repos/src/HOL: isabelle components -a ### Missing Isabelle component: /Users/lp15/.isabelle/contrib/jedit_build-20130104 Getting http://isabelle.in.tum.de/components/jedit_build-20130104.tar.gz; Unpacking /Users/lp15/.isabelle/contrib/jedit_build-20130104.tar.gz This brand-new file has a creation date of 14-June-2011 ! Back to the initial observations. Is the date 14-June-2011 the one of jedit_build-20130104.tar.gz and/or the unpacked contents? Note that Getting means perl ... jedit_build-20130104.tar.gz so the date stamp of the result is determined locally, not by the server (which looks fine anyway, according to lynx -head -dump http://isabelle.in.tum.de/components/jedit_build-20130104.tar.gz;). What is also odd, is the ### Missing Isabelle component in the first place. It means that the directory given there somehow got lost. Do you have any old or duplicate component specfications in $ISABELLE_HOME_USER/etc/settings or $ISABELLE_HOME_USER/etc/components ? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Automatic popup menus on hovers
On Sat, 9 Mar 2013, Lars Noschinski wrote: I'm currently using revision 4b5a5e26161d of Isabelle and after working with it for one day without stopping jEdit, I noticed a annoying behaviour of the popup menus which you get automatically by hovering over a command with a message: They pop up immediately, even if I don't stop over them. Afterwards, they don't vanish. So if I just want to move the cursor or click on something, these popups get in my way. If I want to do something around a failed proof step, I have to move my mouse very carefully (I got so bad, that I stopped using the mouse and went back to the keyboard). This behaviour only popped up after working with one session for a longer time and jEdit was having frequent hiccups then, so I guess this was due to memory pressure (max memory usage was near the limit of 1600m set for the JVM). I've spent some days pondering various possibilities and reading sources of Java/Swing libraries. Not everything is clear, but there are various possibilities of memory leaks and timing problems when popping up a new window for each tooltip (in the sense of regular getToolTipText of Swing components). In Isabelle/14e6d761ba1c it is now done in a completely different way. So lets see if this works better. (According to past experience odd corner cases will show up after some weeks or months using it.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] multiple weirdnesses
On Mon, 18 Mar 2013, Lawrence Paulson wrote: The June 2011 date is of the unpacked contents. The compressed archive file is dated January 2013. I've looked around on my own local file-system. The 14-Jun-2011 date stamp is there for the *toplevel* directory of various jedit_build components, but the content deeper down is newer, just as expected. There is no big mystery behind it: when updating the jedit_build stuff, I merely copy over some directory structure that I made first on 14-Jun-2011. So that is the timestamp that ends up in the tar. This should not affect the jedit build process, since the updated jars are stamped correctly. There may be other occasional hiccups, since JVM or Scala builds are not as plain and easy as Poly/ML ones. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] multiple weirdnesses
Just to clarify: these messages have appeared out of order due to mailing list moderation (because my image was too big). The only computers in question are my laptop and my main workstation, and the image in my last two messages refer to the same computer. Larry On 18 Mar 2013, at 11:46, Lawrence Paulson l...@cam.ac.uk wrote: I've checked on another computer, and I get exactly the same thing. File creation dates set in the past can cause a lot of problems, so it would be interesting to know what is going on here. Larry Screen Shot 2013-03-18 at 11.44.38.png On 18 Mar 2013, at 11:40, Makarius makar...@sketis.net wrote: On Sat, 16 Mar 2013, Lawrence Paulson wrote: At d5c95b55f849 ~/isabelle/Repos/src/HOL: isabelle components -a ### Missing Isabelle component: /Users/lp15/.isabelle/contrib/jedit_build-20130104 Getting http://isabelle.in.tum.de/components/jedit_build-20130104.tar.gz; Unpacking /Users/lp15/.isabelle/contrib/jedit_build-20130104.tar.gz This brand-new file has a creation date of 14-June-2011 ! The jedit_build-20130104 component is from 04-Jan-2013 -- it did not change recently. This incident looks more like a drop-out of your local file-system. 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] Automated testing questions
On Mon, 2013-03-18 at 12:16 +0100, Makarius wrote: If anything is missing or wrong in README_REPOSITORY, I ask once again to point it out, either on isabelle-dev or privately, and not to make unreliable/unmaintained clones of such important information. Occasionally cd isabelle hg pull -u ./bin/isabelle components -a ./bin/isabelle jedit -l HOL results in Scala build errors. If this is bound to happen from time to time, instructions on how to recover (possibly just mentioning -f) or a pointer to such instructions might be helpful. Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Automatic popup menus on hovers
On Sat, 9 Mar 2013, Lars Noschinski wrote: This behaviour only popped up after working with one session for a longer time and jEdit was having frequent hiccups then, so I guess this was due to memory pressure (max memory usage was near the limit of 1600m set for the JVM). On 03/18/2013 01:29 PM, Makarius wrote: I've spent some days pondering various possibilities and reading sources of Java/Swing libraries. Not everything is clear, but there are various possibilities of memory leaks and timing problems when popping up a new window for each tooltip (in the sense of regular getToolTipText of Swing components). Concerning actual memory leaks, I made the experience that these are rather easy to track down on the JVM: Take a heap dump and analyze it using a suitable tool such as Eclipse Memory Analyzer (http://www.eclipse.org/mat/). The tool has an automated analysis which can usually point out the main sources of memory consumption immediately. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Debugging low-level exceptions
On 03/18/2013 12:47 PM, Makarius wrote: On Sat, 16 Mar 2013, Florian Haftmann wrote: you have to watch the »Raw output« buffer (via Plugins - Isabelle). Toplevel.debug and Runtime.debug are the same flag, with slightly varying purpose over the years, but now it is just for exception_trace wrapping for Isar transactions. The underlying PolyML.exception_trace works via low-level stdout, so the Raw Output panel is indeed the way to see that in Isabelle/jEdit. One also needs to guess what is the right trace, since it is not related to formal document content --- just physical output on a side-channel. Thanks, that helped. I don't know why my first attempt didn't work (of course I tried raw output), but now I am getting the expected traces. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
