Re: [isabelle-dev] NEWS: process management (summary and update)
On 11.03.2016 18:37, Makarius wrote: > * The executable "isabelle_process" has been discontinued. Tools and > prover front-ends should use ML_Process or Isabelle_Process in > Isabelle/Scala. INCOMPATIBILITY. > > * New command-line tool "isabelle process" supports ML evaluation of > literal expressions (option -e) or files (option -f) in the context of a > given heap image. Errors lead to premature exit of the ML process with > return code 1. To whomever is now maintaining Haskabelle (Ondřej?): This change breaks Haskabelle as it calls isabelle_process to build its adaptation table (in lib/mk_adapt). -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] the function "real"
On 12.11.2015 13:58, Lars Noschinski wrote: > On 11.11.2015 22:09, Johannes Hölzl wrote: >> It looks like the setup for blast changed, in the following entries is a >> non-terminating blast call. They do not seam to be related to the change >> at all: >> >> Graph_Theory > > I replaced this 'by safe meson+' now. I am a bit surprised that this > proof broke, it is just basic set theory and first order logic. Ok, bisected to the change which broke this proof: it is 933eb9e6a1cc by Larry. The good news is the current head unbroke the proof agian. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] the function "real"
On 11.11.2015 22:09, Johannes Hölzl wrote: > It looks like the setup for blast changed, in the following entries is a > non-terminating blast call. They do not seam to be related to the change > at all: > > Graph_Theory I replaced this 'by safe meson+' now. I am a bit surprised that this proof broke, it is just basic set theory and first order logic. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] local ghc and happy installations in Munich
Hi, historically, I am still responsible for our local ghc-6.12.1, ghc-7.0.3, and happy-1.16 installations. As far as I can tell, these are not used anymore -- if anybody disagrees, please speak up. Otherwise, I will delete them next week. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
On 10.09.2015 12:19, Dmitriy Traytel wrote: > Hi Florian, > > while I very much welcome the simplified printing rules and your effort > of unifying case_prod/split, I am not sure if adding a third alternative > name is the way to go. The situation reminds me of the one depicted in [1]. > > Clearly, case_prod is the "right" name from the perspective of the > (co)datatype package. I also prefer a name following the usual case_ convention over a special case for type prod. >> b) partially applied with explicit double lambda abstraction in >> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; >> >> c) partially applied with eta-contracted body term "uncurry f": >> no special syntax, plain "uncurry" combinator. This does not seem to work right now; case b) is printed like c) if the body is eta-contractable (but not eta-contracted). >> This schema emerged after some experimentation and seems to be a >> convenient compromise. The longer perspective is to overcome the >> case_prod/split schism eventually and consolidate theorem names accordingly. What is the problem with converging to the default names created by the new datatype package? -- Laras ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] simps_of_case and function types
Hi everyone, Lars Hupel privately reported a situation where simps_of_case does not work as expected (refering to 2015 and to 87f0f707a5f8). I have not solved the issue yet (and will probably not find time the next two months), so I document my findings here. fun nosplit where nosplit x f = (case x of [] ⇒ f | _ # xs ⇒ nosplit xs f) fun nosplit' where nosplit' x (f :: 'a ⇒ 'b) = (case x of [] ⇒ f | _ # xs ⇒ nosplit xs f) simps_of_case foo: nosplit.simps (* produces 2 theorems, as expected *) simps_of_case foo: nosplit'.simps (* produces only one theorem! *) The reason is that simps_of_case tries to apply the split rule for lists, but without the elaborate steps done by the splitter. Instead, it simply relies on Higher-Order-Unification, which falls short on these examples. Unfortunately, simps_of_case cannot use the Splitter, as splitter applies the split-rule in the wrong direction. So simps_of_case either needs to reimplement the Splitter's logic for instantiating the split rule or the Splitter needs to be refactored generate the instantiated equation. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: 'subgoal' command
On 03.07.2015 04:02, Daniel Matichuk wrote: Additionally, fresh names are chosen for any free variables that appear in the subgoal e.g. lemma ⋀x y. A x y subgoal for A Results in x being named Aa. In this case I would expect either an error (Free name clash) or for the new fixed term to shadow the free A. The second choice is a bit strange, however, because you end up with two different coloured As in the goal. I would expect unspecified variables to get internal names, i.e. names ending with _; similar to variables not specified in a case command. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle services not available this weekend (2015-07-03 to 2015-07-06)
Hi everyone, due to maintenance of the power grid at TU Munich, a number of Isabelle related services will not be available this weekend (starting Friday, July 3th, 9:00 CEST to Monday, July 6th, somewhere in the afternoon CEST), in particular - the isabelle-dev mailing list, - the development repositories, - and the Munich mirror of the website[1]. The isabelle-users mailing list is hosted in Cambridge and thus not affected. -- Lars [1] The mirrors at Cambridge and Sydney are not affected: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html http://mirror.cse.unsw.edu.au/pub/isabelle/index.html ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
On 24.06.2015 16:29, Larry Paulson wrote: This may be the problem. I don’t remember exactly what I was trying to do, only that it was very difficult. Of course nobody uses show_types any more. At least this was the problem for me. A notorious instance of the same problem are the functions in HOL-Word, e.g. ucast :: 'a word = 'b word and uint :: 'a word = int. Getting at the types of things like uint (ucast 4) in some big term happens often when verifying C programs and is pretty annoying. Such things need a disambiguating output syntax (at least as long as hovering in the output buffer doesn't show the types, maybe even then). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New proof method rewrite
On 14.04.2015 15:59, Lars Noschinski wrote: Currently, I'm still contemplating whether it is feasible to add a proper ML interface in the short remaining time, but this probably needs to wait for the next release, too. Turns out, a proper ML interface is not too hard, see now ef4fe30e9ef1. Writing the patterns down, however, is a quite annoying task. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New proof method rewrite
On 09.04.2015 21:08, Makarius wrote: On Thu, 9 Apr 2015, Lars Noschinski wrote: On 18.03.2015 15:16, Lars Noschinski wrote: commit 4ed50ebf5d36 adds a new proof method rewrite. This is the pattern-based replacement for subst Christoph Traut and I presented at the last Isabelle Workshop [1]. For now, it lifes in ~~/src/HOL/Library/Rewrite and is still missing a proper documentation (but there are examples in ~~/src/HOL/ex/Rewrite_Examples). I've used it now a bit to add annotations in program verification and (contrary to my former intuition) found the order of the patterns to be the wrong way around. If someone has used the rewrite method and has some opinions on that, I would be glad to hear these. I haven't used it yet, although I looked a bit through the sources, just as a matter of pre-release routine. I also added a symbol assignment for \hole in the IsabelleText font and isabellesym.sty -- it is the result of spending 30min looking carefully through DejaVuSansMono and http://mirrors.ctan.org/info/symbols/comprehensive/symbols-a4.pdf -- see now b911c8ba0b69. LaTeX packages should not be overly exotic as rendering of Isabelle symbols -- hopefully wasysym.sty was a decent choice here. Nice, this deals with the conflict I encountered a few days ago with the use of the \box symbol in AutoCorres. Back to the actual topic of this thread: If you want to change the syntax for the release, there are a very few days left until the first release candidate is published, while the repository still remains in pre-forked state, probably until the end of next week. Technically, to have Parse.xthms1 before quasi-keywords like at, you need some Scan.unless trickery, but it should be doable. Method.sections also manages that with add, del etc. I was not clear above. I don't want to change the general syntax of position to rules, but was contemplating whether the position should read inside-out or outside-in. As I noted in my other mail, this will have to wait for the next round. Here is also a command line to explore possibilities of true keywords, instead of quasi-keywords: $ isabelle build -n -a -d '$AFP' -k at -k asm -k concl Note that outer syntax is now local to each theory, so as long as it is just a separate theory somewhere, one can be liberal. Anything for main HOL needs more care, of course. (For Eisbach we also have some open problems with keyword clashes still left to address, concl is one of them.) The goal is definitely to have the tool end up in Main, so I will not get too fancy with the syntax. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle/jEdit hangs on exit
Hi everyone, I sometimes managed to hang Isabelle/jEdit by: * changing multiple files * selecting quit * in the dialog asking me whether I want to save all files, clicking on Select All then Save Selected The editor hang for a few minutes, till I killed it with SIGKILL (SIGTERM didn't suffice). Most recently, this happened with 19e5f5ac7b59. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New proof method rewrite
On 18.03.2015 15:16, Lars Noschinski wrote: commit 4ed50ebf5d36 adds a new proof method rewrite. This is the pattern-based replacement for subst Christoph Traut and I presented at the last Isabelle Workshop [1]. For now, it lifes in ~~/src/HOL/Library/Rewrite and is still missing a proper documentation (but there are examples in ~~/src/HOL/ex/Rewrite_Examples). I've used it now a bit to add annotations in program verification and (contrary to my former intuition) found the order of the patterns to be the wrong way around. If someone has used the rewrite method and has some opinions on that, I would be glad to hear these. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Mira still alive?
On 02.04.2015 00:31, Makarius wrote: On http://isabelle.in.tum.de/reports/Isabelle there is very little to see. This is occasionally important to investigate timing problems, or to see how Isabelle vs. AFP works out. The testbench suites were running, but none of the other tests. One instance was even hanging since a last september. As I usually don't need these services, I only notice hiccups when somebody tells me about it. Unfortunately, mira is not very reliable. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Mira/AFP broken?
On 20.03.2015 00:03, Makarius wrote: There are very few AFP tests on http://isabelle.in.tum.de/reports/Isabelle in recent weeks/months. Is there anybody who understands how that works, to look what is the situation? It seems that the mira AFP test locked up during mirroring the repositories about a month ago. I restarted it. 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
[isabelle-dev] New proof method rewrite
Hi, commit 4ed50ebf5d36 adds a new proof method rewrite. This is the pattern-based replacement for subst Christoph Traut and I presented at the last Isabelle Workshop [1]. For now, it lifes in ~~/src/HOL/Library/Rewrite and is still missing a proper documentation (but there are examples in ~~/src/HOL/ex/Rewrite_Examples). The plan is to eventually move it into the main HOL image (although technically it should work with any logic with a simplifier setup). [1] https://www21.in.tum.de/~noschinl/Pattern-2014/ ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Improved Graphview
On 21.01.2015 11:58, Lars Noschinski wrote: While the UI was clearly subobtimal, I found it very useful to be able to show only a part of the total graph (via Show - only children or so). Similarly, I liked the ability to highlight the children/parents of certain nodes. I'll describe the use-case: I have a hierarchy of 19 locales, with 1 root and 8 leaves, describing some complex case distinction. After finishing the proof I got the certain feeling that this hierarchy is too complex or not enough partial results are shared. So, I'm only interested in this part of the whole locale hierarchy -- I don't want to see any other nodes Furthermore, I have a property P and in my hierarchy there locales corresponding to P and not P. I wanted to ensure that each of my leaf locales inherited from one of these locales (the structure was very much a DAG, not really tree-like, so it was not obvious to see). -- I colored the descendants of the P and not-P locales (bonus points for different colors). I then proceeded to print the resulting graph and adding further annotations with a pen ;) I just tried it again with fde2659085e1. Without the ability to filter out irrelevant nodes, the task described here feels rather daunting ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Improved Graphview
On 18.01.2015 23:14, Makarius wrote: On Sat, 17 Jan 2015, Makarius wrote: Attentive readers of incoming changesets might have noticed the recent improvements of the Graphview component, which was a not-quite-working student project from some years ago. As of Isabelle/32b162d1d9b5 it is already quite usable, although a few details of the old graph browser are still missing. More details are present in Isabelle/5d08b2332b76, notably some kind of tree view on the content, with possibilities to select a subset of nodes, or jump to a particular node via double-click. I am leaving a brief time-window open to point out remaining uses of the old browser, but the plan is to dismantle it rather soon. I haven't used the locale dependency graph much, just a bit in 533f6cfc04c0 (with the new Graphview component). While the UI was clearly subobtimal, I found it very useful to be able to show only a part of the total graph (via Show - only children or so). Similarly, I liked the ability to highlight the children/parents of certain nodes. I'll describe the use-case: I have a hierarchy of 19 locales, with 1 root and 8 leaves, describing some complex case distinction. After finishing the proof I got the certain feeling that this hierarchy is too complex or not enough partial results are shared. So, I'm only interested in this part of the whole locale hierarchy -- I don't want to see any other nodes Furthermore, I have a property P and in my hierarchy there locales corresponding to P and not P. I wanted to ensure that each of my leaf locales inherited from one of these locales (the structure was very much a DAG, not really tree-like, so it was not obvious to see). -- I colored the descendants of the P and not-P locales (bonus points for different colors). I then proceeded to print the resulting graph and adding further annotations with a pen ;) -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Folding in Isabelle/jEdit
Hi, I've played around a bit with the folding in Isabelle/jEdit (as of 533f6cfc04c0). As far as I can see, one can fold - the lemma statement, without the proof - the lemma statement, including the proof However, my lemma statements usually consists of multiple lines (due to being in structured syntax), so the most useful option for me would be: - fold the proof, keeping the lemma statement unfolded Is such a fold available? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Shortcuts for \^sub and \^sup?
Hi, in Isabelle 2014, on can enter \^sub and \^sup via C+e DOWN and C+e UP, respectively. In 91649ea1b32c, these shortcuts don't work anymore (at least for me). Is there any other shortcut for these? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL broken?
On 11.11.2014 18:10, Dmitriy Traytel wrote: http://isabelle.in.tum.de/reports/Isabelle/report/60d6105dac94411c8f55ea7626a15c71 anybody taking care of this? Mea culpa. Apparently I pushed something less then I posted to the testboard. Taking care of this. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL broken?
On 11.11.2014 19:37, Lars Noschinski wrote: On 11.11.2014 18:10, Dmitriy Traytel wrote: http://isabelle.in.tum.de/reports/Isabelle/report/60d6105dac94411c8f55ea7626a15c71 anybody taking care of this? Mea culpa. Apparently I pushed something less then I posted to the testboard. Taking care of this. Should be fixed now. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Stripped testboard repository
Hi everyone, someone accidentally pushed a big bunch of unrelated changes to the testboard repository, effectively hiding a lof of history. I clone a new repository, based on the latest tip -- if you miss any commits, you might need to push them again (the test results are still there, but not shown when not in the repository). A backup of the old repository exists. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] porting code to isabelle2014 and getting unfinished linear change errors
On 25.08.2014 09:04, Michael Norrish wrote: I'm based off RC0 (at 9e0c62d of the *git* mirror at github.com/seL4/isabelle; this is tagged Isabelle2014-RC0 and certainly seems to be the same as 251ef0202e71 in the Mercurial world). I am running code that seemed to be legitimate in 2013-2, but which is now giving me errors such as *** exception Fail raised (line 169 of sign.ML): Unfinished linear change of theory content *** At command end (line 142 of ~/ver2014/l4v/tools/c-parser/testfiles/fncall.thy) This is related to never leaving the local theories properly. If I remember correctly, you use Proof_Context.theory_of in places where it really should have been Named_Theory.exit(_global). One annoying thing about this is that it is happening at theory end rather than directly after or during the execution of my code. What would be the easiest way to debug this problem? Or is there an obvious fix I can apply? The way I debugged this was commenting out large parts of the code until the error disappeared. David Greenaway already has some patches I used to get autocorres (including the c-parser) running on 2014 -- I'll send them to you privately. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Haskabelle test
Hi, Is there anyone who knows how the Haskabelle test is setup and can change it so it runs not only if the Haskabelle repository changes, but also if the Isabelle repository changed? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Methods that fail with stack-overflow
On 03.07.2014 13:57, Peter Lammich wrote: Hi, I recently ran into a method that produced a stack-overflow. The good thing is: In the current jedit version, it is properly highlighted and you immediately see that there is some error. (This was not always the case in the past) The bad thing: The only way how to get a clue what is going wrong is to open the raw output panel. This writes stack-overflow then, without any location or trace. How to enable tracing for those exceptions, in particular as Toplevel.debug seems to have gone away? There is ML_trace (and a similar option); i.e. declare [[ML_trace]]. Have a look at print_options. I don't know whether this helps in your concrete situation. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit FAILED
On 28.06.2014 17:24, Makarius wrote: On Sat, 28 Jun 2014, Makarius wrote: On Sat, 28 Jun 2014, Florian Haftmann wrote: suggests that something is bad with $JEDIT_HOME in the mira build environment. JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings of that component within Isabelle. So it should normally be there, although I don't understand the mira setup. Another guess: Isabelle/jEdit is really missing, because of a lacking isabelle jedit -b that is done in regular makedist (e.g. in isatest). mira just executes isabelle build -s -v with job specific options (can be seen in Admin/mira.py). If isabelle jedit -b is a necessary step to setup a fresh Isabelle installation, I can add that to the setup script. BTW: Admin/mira.py is the Isabelle specific part of the mira setup. Unfortunately, the version of the script used is not the one for the version which is tested, but the one which is current on mira startup. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
On 27.06.2014 23:47, Makarius wrote: Just a side remark: in the repository version we are talking about, and thus the coming release, ML in auxiliary files works smoothly and often better than the ML blocks, because the file gets its own ML mode. For ML files, I occasionally had the problem that hovering would not work. It usually recovered after some time. I haven't been able to pin it down to a certain situation yet. The file in question has around 400-500 lines. I /think/, this refers to d3d91422f4 (haven't worked enough with later revisions yet). It might be coincidence, but I haven't encountered this behaviour with ML blocks yet. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
On 27.06.2014 07:52, John Wickerson wrote: Moreover, I would like an incremental search, but there is probably a jEdit pluging somewhere? (Probably with the same problems of entering non-ASCII characters) There is already an incremental search, but by default it has no keyboard shortcut. Myself, I have re-bound Ctrl-F to Incremental Search Bar, and am quite happy with that. (This is in jEdit's Global Options, then Shortcuts.) I'm pretty sure this is bound to Alt-, by default. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the Isabelle2014 release
On 11.06.2014 06:56, Thomas Sewell wrote: OK, I've finished the needed adjustments the AFP proofs which were affected by the hypsubst change. The result is fairly encouraging: the AFP is *huge* and the diffstat of the required changes is: 63 files changed, 134 insertions(+), 81 deletions(-) Not an especially high percentage of changes in the end. Nice! I don't think there's a testboard equivalent for a simultaneous Isabelle/AFP change, That is correct. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the Isabelle2014 release
On 05.06.2014 05:44, Thomas Sewell wrote: In particular, I want to avoid ever changing the setting globally. I've had some bad experiences in the past with theories with differing global configurations, which means that the location of a tactic and the include graphs of theories start having subtle effects on the way the tactics run. It's a mess. A little less invasive would be enabling the compatibility mode for a whole theory using context notes [[...]] begin ... end. signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard problem
On 04.06.2014 13:37, Johannes Hölzl wrote: We remove ~isatest/.isabelle/heaps/.../HOL-Proofs on lxbroy10 and now it works... I don't know why mira is accessing this file, it actually sets up the settings file to _not_ look into the users heaps-directory. But it looks like there is a problem with this setup. After looking a bit closer: Mira changes ISABELLE_HOME_USER (by appending it to $ISABELLE_HOME/etc/settings). Of course, this is too late to affect ISABELLE_PATH, which still refers to $USER_HOME/.isabelle/heaps. So, we set $USER_HOME instead before starting Isabelle (see bcc6dc6c1d1c8a6). @Makarius: Does this use fit the intention of USER_HOME? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Improved management of dockable windows
On 12.05.2014 14:26, Makarius wrote: * Improved management of dockable windows: clarified keyboard focus and window placement wrt. main editor view; optional menu item to Detach a copy where this makes sense. I've started using the Detach functionality quite a bit during the last week. A few comments on that: * At least for the output window, I'd like to see a more direct to to detach a window than the context menu. * The fact that a detached window stays on top of the jEdit window is often quite nice. * On GNOME 3.8, the detached (and floating instance) windows do not have the usual close button, nor can they be maximized (resizing is possible, though) (this refers to b7999893ffcce). This is annoying, as I sometimes use the whole second screen to look at long goals (which are sometimes awkwardly wrapped). (I guess this is a side-effect of making the windows JDialogs). * Sometimes, I use a detached window to see the proof state at a certain position in my theory, regardless on where my cursor is. If I successfully changed (i.e. not in between) some lemmas before, I want to see the updated proof state at the same position as before (for example by clicking some update button). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: improved syntactic and semantic completion mechanism
On 31.03.2014 22:04, Makarius wrote: - Syntax completion of the editor and semantic completion of the prover are merged. Since the latter requires a full round-trip of document update to arrive, the default for option jedit_completion_delay has been changed to 0.5s to improve the user experience. I haven't been able to get used to this (having to wait for a symbol completion disturbs my typing flow), so I switched back to 0s. Enabling immediate completion did not make this more palatable for me, for two reasons: For example, ! is not immediately completed (due to !!). Moreover, typos sometimes caused erroneous completions. I usually feel that I mistyped and hit backspace immediately - if the word was completed in between, I should have hit Ctrl-Z instead. The other thing I noticed during the last days was the following: When I modify a term, I usually place the term at the position where I want to insert something (which is often directly before a variable or constant), start typing and only add the necessary space as the last character I type. This means that I don't have symbol completion available (because the completion mechanism believes me to be in the middle of a word). I usually notice this when I want to enter a symbol, so I type SPACE LEFT and add another character of the symbol to trigger the completion popup. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: improved syntactic and semantic completion mechanism
On 31.03.2014 22:04, Makarius wrote: These cumulative NEWS refer to Isabelle/075397022503. This also marks the point where my continously shrinking and growing TODO list has reached a stable state concerning completion and the main activity on this part is finished for now. I have recently written some proof with some german plain text. This triggered a lot of completion popups, suggesting to correct german to english words (which is to be expected). Unfortunately, the completion popup does not disappear when I continue typing the next word. Then, at the end of the line, i press RETURN TAB (to get to the correct indentation level again) which then completes the word -- this seems to be timing related, as a single RETURN pause closes the completion popup. For me, the expected behaviour would have been to close the completion as soon as a word-separating character (in this case, a space) has been entered. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] neg_numeral fallout
(moving this to the -dev list):
On 15.05.2014 18:59, Florian Haftmann wrote:
Hi Lars,
when you abolished neg_numeral, the lemmas in word_no_log_defs got
slightly weaker (as they do not work for -1 anymore). I noticed that
when converting WordLemmaBucket from autocorres-095-beta3 to the
development version (in neg_mask_mono_le).
I don't know what is the best way to fix this. word_bitwise_1_simps has
special cases for 1, if we do this for -1 too, we get 4 times as many
lemmas.
this is indeed the recommendation from NEWS.
I tried to make this transition whenever encountering numeral lemmas,
but the word library is too convoluted to do proper analysis and the
experimental tests exhibited no problem there.
I thought about it a bit more and arrived at the following change. Any
thoughts?
--- a/src/HOL/Word/Word.thy
+++ b/src/HOL/Word/Word.thy
@@ -2283,6 +2283,18 @@ lemma word_bitwise_1_simps [simp]:
- numeral a XOR 1 = word_of_int (- numeral a XOR 1)
by (transfer, simp)+
+text {* Special cases for when one of the arguments equals -1. *}
+
+lemma word_bitwise_m1_simps [simp]:
+ NOT (-1::'a::len0 word) = 0
+ (-1::'a::len0 word) AND x = x
+ x AND (-1::'a::len0 word) = x
+ (-1::'a::len0 word) OR x = -1
+ x OR (-1::'a::len0 word) = -1
+ (-1::'a::len0 word) XOR x = NOT x
+ x XOR (-1::'a::len0 word) = NOT x
+ by (transfer, simp)+
+
lemma uint_or: uint (x OR y) = (uint x) OR (uint y)
by (transfer, simp add: bin_trunc_ao)
-- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] neg_numeral fallout
On 16.05.2014 12:30, Gerwin Klein wrote: Looks ok, but what about all the other operators? (shift, rotate, etc) As far as I can see, shift and rotate don't have their own lemmas for evaluating numerals, so the demise of neg_numerals shouldn't have introduced a regression there. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] neg_numeral fallout
On 16.05.2014 12:53, Lars Noschinski wrote: On 16.05.2014 12:30, Gerwin Klein wrote: Looks ok, but what about all the other operators? (shift, rotate, etc) As far as I can see, shift and rotate don't have their own lemmas for evaluating numerals, so the demise of neg_numerals shouldn't have introduced a regression there. See now 376604d56b5 -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Errors in right bar shadowed by warnings
Hi, while porting some larger theory (~5800 lines) to the repository version (23a9cb098ccb), I noticed that sometimes the red error bars in the right status bar are shadowed by warnings; that is, I see in the theory panel that there are errors in this theory, but I have to carefully scroll through the theory file until I find the location. I haven't cooked up a small example, but this can be seen in WordLemmaBucket.thy in 6789d4b8379e in macbroy26:/home/noschinl/repos/vcg-labeling.git A video (slightly bad quality, the state of options to do simple video cropping in Linux seems kind of ... bad): http://www21.in.tum.de/~noschinl/isabelle-shadowed-errors.m4v -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: improved syntactic and semantic completion mechanism
On 31.03.2014 22:04, Makarius wrote: I played a bit around with your new completion setup. - Support for semantic completion based on failed name space lookup. The error produced by the prover contains information about alternative names that are accessible in a particular position. This may be used with explicit completion (C+b) or implicit completion after some delay. Where C+b is bound to Complete Isabelle text, I assume (following the repository versions, it was still Complete Word for me). - Semantic completions may get extended by appending a suffix of underscores to an already recognized name, e.g. foo_ to complete foo or foobar if these are known in the context. The special identifier __ serves as a wild-card in this respect: it completes to the full collection of names from the name space (truncated according to the system option completion_limit I would expect an _explicit_ completion after foo to offer both foo and foobar. After all, I am apparently not satisfied with the current completion. I also noticed that __ is marked as completable, but you need to request explicit completion -- is this intended? - Syntax completion of the editor and semantic completion of the prover are merged. Since the latter requires a full round-trip of document update to arrive, the default for option jedit_completion_delay has been changed to 0.5s to improve the user experience. With immediate completion, this seems somewhat usable for me (but I still need test it more -- for most of my current work I am bound to the release version). Without immediate completion, I always have to insert artificial pauses for symbol completion, which is very annoying. What are the drawbacks of a 0s delay? The one I could observe is that I need to requeste fact completion explicitly, which is okay-ish for me -- I often need to think about the right facts anyway. An alternative would be an incremental filling of the completion popup. I think Eclipse does that. Personally, I like C+SPACE better than C+b as an explicit completion key binding. I encountered some behaviour which I found confusing (5b171d4e1d6e): - theory Scratch imports Main begin notepad begin from - If I now enter an s after the from, a popup listing possible facts appears (which is expected). Close this popup (for example, by pressing Esc). Now press C+b to open it again. The first suggestions is now sledgehammer (keyword), which was absent before. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Support for Navigator plugin
On 07.04.2014 15:16, Makarius wrote: Note that keyboard shortcuts similar to major web browsers refers to A-LEFT and A-RIGHT on Windows and Linux. On Mac OS X, that would be Control-LEFT and Control-RIGHT, but it is neither a standard browser key sequence, nor does it usually work at all, due to some conflicts with other Apple desktop navigation functionality that I don't really understand. A-LEFT and A-RIGHT overwrite the standard indentation bindings. I use CS-LEFT/RIGHT for this reason. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Support for Navigator plugin
On 07.04.2014 15:40, Makarius wrote: I do check for jEdit keymap conflicts routinely, since this is not ESCAPE-META-ALT-CONTROL-SHIFT with an infinite space of possibilities. There is indeed an overlap with actions called shift-left (Sift Indent Left) and shift-right (Shift Indent Right), but as far as I can tell they are the same as S-TAB and TAB (which I am routinely using for that). S-TAB yes, TAB only works at the beginning of the line. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: ML antiquotation @{print}
So what should I use before antiquotations are available? Should I still avoid
PolyML.makestring?
Makarius makar...@sketis.net schrieb:
* ML antiquotation @{print} inlines a function to print an arbitrary
ML value, which is occasionally useful for diagnostic or demonstration
purposes.
This refers to Isabelle/386e4cb7ad68, which also points to the place where
the older antiquotation @{make_string} is documented.
Despite these official Isabelle/ML tools for debugging and diagnostics, I
sometimes see low-level ML traditionalists who are stuck with PolyML.print
or PolyML.makestring -- but there are no reasons for that, apart from old
habits. David Matthews has provided better entry points for that several
years ago, and the above antiquotations make use of them.
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] Annotations in Theories panel not visible
On 01.04.2014 07:54, Lars Noschinski wrote: I've tried on Linux with Swing LF Nimbus, GTK+, Metal, and it all works for me. Do you have any special GUI or font properties? If the problem still persists can you make a screenshot? I made a short video: http://www21.in.tum.de/~noschinl/jedit-annotations.webm. I tested the Metal and Nimbus LF; the font is IsabelleText. This is on a system running Debian stable with Gnome 3.4.2. I couldn't reproduce the behaviour on another machine with Debian testing and Gnome 3.8.4. Looking closer yet again, the annotations don't vanish, but the bars get too wide. If you look at the video above, the Theories panel is redrawn two times before the actual process of proving starts. Each time, the width of the bars increases. After the third iteration, it is wider than the panel. But there is no optical indication for this (e.g., a scrollbar), so it looks like part of the annotations vanish when processing procedes into the hidden part of the panel. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle support for Standard ML
On 31.03.2014 16:04, Makarius wrote: What we have here is the Isabelle Prover IDE technology used for something that is not Isabelle, namely official Standard ML. It is just a coincidence that it runs within the same Poly/ML runtime system -- there is no direct connection to the Isabelle/ML world. This means regular SML projects can be edited with it, assuming that the build process is not too exotic --- just the typical list of use statements (without nesting) that need to be replaced by 'SML_file' here. I tried to load Pure.ML with SML_File, but this probably qualifies as a too exotic build process ;) -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Annotations in Theories panel not visible
On 31.03.2014 22:43, Makarius wrote: On Tue, 18 Mar 2014, Lars Noschinski wrote: I just noticed (in f0d2609c4cdc) that not all warnings and errors are visible in the Theories panel. If I run isabelle jedit -l Pure src/Pure/Main.thy and watch the Theories panel, I see that there are some warning e.g. in Orderings. However, as soon as Orderings is finished, the annotations for Orderings disappear (in the Theories panel). This happens with some, but not all theories (e.g., Code_Generator or Ctr_Sugar keep their annotations). This happens not only for warnings, but also for errors. Thanks for keeping an eye on such important details. Did you see this again in the meantime? I could not reproduce it in the version f0d2609c4cdc nor in 97d6a786e0f9 from today. Reproducable with 97d6a786e0f9. Theory Orderings has very few warnings compared to Code_Generator or Ctr_Sugar, so there could be a problem with the GUI geometry calculations. These are just small rectangles painted in a certain spot -- when the theory is finished the odd messages move to the right and might just get out of view. Looking at the problem more closely, it seems that the final rectangles (after the theory has finished) are about half or maybe a third the size of the rectangles during processes (and vanish, if they are small enough). I've tried on Linux with Swing LF Nimbus, GTK+, Metal, and it all works for me. Do you have any special GUI or font properties? If the problem still persists can you make a screenshot? I made a short video: http://www21.in.tum.de/~noschinl/jedit-annotations.webm. I tested the Metal and Nimbus LF; the font is IsabelleText. This is on a system running Debian stable with Gnome 3.4.2. I couldn't reproduce the behaviour on another machine with Debian testing and Gnome 3.8.4. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_makeall not finishing on testboard
Hi Brian, On 20.03.2014 15:24, Brian Huffman wrote: I've noticed that recent changesets (up to 00112abe9b25) on testboard have completed Pure and HOL tests, but the HOL_makeall results never show up. (The most recent HOL_makeall report is 3253aaf73a01, dated March 18.) Does anyone know why this is? Is one of the HOL theories going into an infinite loop? (I currently have insufficient computing resources to test everything myself.) No; it is just that the relevant Mira instance crashed. I've restarted it now. Best regards, Lars signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Annotations in Theories panel not visible
Hi, I just noticed (in f0d2609c4cdc) that not all warnings and errors are visible in the Theories panel. If I run isabelle jedit -l Pure src/Pure/Main.thy and watch the Theories panel, I see that there are some warning e.g. in Orderings. However, as soon as Orderings is finished, the annotations for Orderings disappear (in the Theories panel). This happens with some, but not all theories (e.g., Code_Generator or Ctr_Sugar keep their annotations). This happens not only for warnings, but also for errors. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Abbreviation for \leftarrow
On 05.03.2014 16:25, Makarius wrote: Did you try any of the catch-all abbreviations, like . for left arrows, or . for right arrows, or for double arrows? No; I only discovered them today. As \leftarrow is the only left arrow I use, this will probably work. Still, having symmetric abbreviations would be nice. Ambiguous completions are never immediate, though. I never used immediate completion. I need to try again it with the semantic completion. It is also possible to add more abbreviations in $ISABELLE_HOME_USER/etc/settings, although I consider that as something for expert users only. I like to keep my settings as close to the default as possible. It is annoying enough to keep my jEdit configuration in sync between different Isabelle releases. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: improved support for Isabelle/ML
On 18.02.2014 17:36, Dmitriy Traytel wrote: However, once I had to restart Isabelle as JEdit became quite irresponsive (using almost 4GB of memory, forced GC didn't help). Maybe I just hat too many ML files open (I usually don't close them once opened) or my ML files are just too big: e.g. ~~/src/HOL/Tools/BNF/bnf_gfp.ML, although on a fresh start after opening just this ML file the system is responsive (with some understandable delay in displaying the markup, but instantly processing edits). Maybe slightly lighter type annotations (at every constant/variable rather than at every subterm) would dodge such problems? While I haven't tried the support for ML-files yet, seeing the types for arbitrary subexpressions is my most beloved feature of the ML-markup. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Stymied by cryptic failure in Product_type.thy
On 17.02.2014 19:55, Josh Tilles wrote: I'm experimenting with separating the intuitionistic parts of HOL from the classical parts. (If anyone is interested, I'd be happy to describe my goals and/or motivations in more detail; for now I'll stick to just the problem description) Renaming HOL.thy to IHOL.thy did not cause any problems. I.e., `./bin/isabelle build HOL` still succeeded after commit 122bc618d6 https://github.com/MerelyAPseudonym/isabelle/tree/122bc618d65927d16877b1107e91224ba3bfbaf8. I then started extracting everything in (I)HOL.thy that depended on the axiom `True_or_False` to a file named CHOL.thy. Many of the ensuing failures I was able to handle, but I don't know what to make of this one from Product_type.thy: ``` free_constructors case_prod for Pair fst snd proof - fix P :: bool and p :: 'a × 'b show (?x1 x2. p = Pair x1 x2 ? P) ? P by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def) next fix a c :: 'a and b d :: 'b have Pair_Rep a b = Pair_Rep c d ? a = c ? b = d by (auto simp add: Pair_Rep_def fun_eq_iff) moreover have Pair_Rep a b ? prod and Pair_Rep c d ? prod by (auto simp add: prod_def) ultimately show Pair a b = Pair c d ? a = c ? b = d by (simp add: Pair_def Abs_prod_inject) qed ``` jEdit underlines qed in red, claiming that: ``` Tactic failed The error(s) above occurred for the goal statement: P (local.prod.case_prod f prod) = (?x1 x2. prod = Pair x1 x2 ? P (f x1 x2)) ``` The position of the error message is a bit misleading. It is not the qed which fails. Instead, after finishing the proof, the free_constructors command tries to prove something on its own -- and fails. Probably, its internal tactics depend on the choice axiom. BTW: Whoever wrote this proof: The first case would be better stated as assume ?x1 x2. p = Pair x1 x2 ? P then show P because meta-implication in show-statements may lead to counter-intuitive behaviour. Best regards, Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New (Co)datatypes: Status Plan 2
On 20.11.2013 17:17, Makarius wrote: Looking at http://isabelle.in.tum.de/reports/Isabelle/ is odd: spinning wheel for 4bc48d713602 (time comment 8 hours ago). So maybe mira is down or non-terminating. In the last days, the CouchDB seems to be down more often than not. Maybe next week I'll have time to look into that; for now I just restarted mira. -- Lars signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Coinductive FAILED
On 06.11.2013 23:12, Jasmin Christian Blanchette wrote: BTW is there any particular reason why testboard and tests are kind of dead these days? The reason is that none of the Mira daemons is running and for some reason I didn't get any notification about that. -- Lars signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Coinductive FAILED
On 07.11.2013 09:50, Lars Noschinski wrote: On 06.11.2013 23:12, Jasmin Christian Blanchette wrote: BTW is there any particular reason why testboard and tests are kind of dead these days? The reason is that none of the Mira daemons is running and for some reason I didn't get any notification about that. (I restarted them just now) signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard
On 02.10.2013 01:09, Alexander Krauss wrote: On 09/27/2013 11:49 AM, Lars Noschinski wrote: It might be a good idea to implement a strategy which tests the existing heads in reverse chronological order (commits pushed last get tested first), but I am not sure whether this information is available in Mercurial (we have the commit date, but this is not necessarily related to the push-date). Such a strategy is easy to implement for a single repository. But for multiple repositories (Isabelle+AFP) there is no useful notion of heads (The obvious lifting to products does work theoretically, but not practically, since there are just too many of them...) Hm, you are right. Another option would be to record the tip-tuples in a push-hook and work on these, if there is no tip to be processed. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle jedit -l HOL fails
Try running jedit -bf, if that does not help, manually remove the build artifacts (I.e. the jar files). Sometimes rebuilding of the Java components doors not work reliably. Clemens Ballarin balla...@in.tum.de schrieb: After updating the repository today (and a seemingly good run of 'isabelle components -a') 'isabelle jedit -l HOL' gives me 2013-10-01 20:42:22.345 java[35294:903] *** NSInvocation: warning: object 0x10ad24390 of class 'ThreadUtilities' does not implement methodSignatureForSelector: -- trouble ahead 2013-10-01 20:42:22.348 java[35294:903] *** NSInvocation: warning: object 0x10ad24390 of class 'ThreadUtilities' does not implement doesNotRecognizeSelector: -- abort /Users/ballarin/isabelle/repo/lib/Tools/java: line 1: 35294 Trace/BPT trap $ISABELLE_JDK_HOME/bin/$PRG $@ I'm still on MacOSX 10.6.8 Snow Leopard. Any ideas? Clemens ___ 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] Testboard
On 27.09.2013 09:16, Peter Lammich wrote: I pushed on testboard 19 hours ago, and my push (36cf426cb1c6) currently only shown as 1/3 processed. Now, testboard seems to have stopped processing it ... however, many later pushs have already run through completely. What's the strategy to get your push on testboard processed within reasonable time? Basically Mira is just watching the repository. If a test run finishes, it looks at the repository, takes the tip and tests it (if it was not already tested). In particular, this means that later pushes can take the focus away from your pushes. It might be a good idea to implement a strategy which tests the existing heads in reverse chronological order (commits pushed last get tested first), but I am not sure whether this information is available in Mercurial (we have the commit date, but this is not necessarily related to the push-date). -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_25-Sep-2013 integration test
On 26.09.2013 10:01, Peter Lammich wrote: I cannot unpack the tar-file. My Linux (Ubuntu 12.04.2 LTS) gives me a bunch of error messages: tar: Ignoring unknown extended header keyword `SCHILY.ino' tar: Ignoring unknown extended header keyword `SCHILY.nlink' tar: Ignoring unknown extended header keyword `SCHILY.dev' ... This seems to happen when using GNU tar to unpack files created by the OS X-version of tar and is not an error. This irritating warning can be avoided by using GNU tar to build the tar files (obviously), or reportedly by playing around with the --format option of tar. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] trace_unify_fail
Hi, I just spent some time discovering where trace_unify_fail went (there now exists an attribute unify_trace_failure). As the introduction of this flag had a NEWS entry, wouldn't this change also merit a NEWS entry (in particular, as it is not documented in the reference manual)? Even if it is crude to use (due to it being a global-only option), it is an important debugging tool, in particular with large goals as you get in program verification. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Dockable window Find
On 09.08.2013 21:05, Makarius wrote: *** Prover IDE -- Isabelle/Scala/jEdit *** * Dockable window Find provides query operations for formal entities (GUI front-end to 'find_theorems' command). Speaking of a1a78a271682, the UI elements for the Search criteria don't work well for me: If the dock is not wide enough, the elements overflow into the next row, but the space reserved for the UI elements does not increase. Hence, they are hidden by the output frame. (on Debian with standard GNOME 3 installation). Best regards, Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL iff notation
On 03.09.2013 16:21, Makarius wrote: On Tue, 3 Sep 2013, Lawrence Paulson wrote: For sure. I think it confuses beginners at first, because == is only allowed in real definitions rather than derived ones. Real definitions are actually just for foundational purposes: users never see them -- neither end-users nor users in the sense of other tools built on top of the system infrastructure (notably Local_Theory.define). As long as def and defines require ==, I don't see much reason in abandoning == for definition in my own usage. (Actually, I would even prefer to use == even for fun and primrec, as it has a better priority for these purposes.) -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] lemma addition
On 01.08.2013 17:19, Makarius wrote: Both of which are discharged by blast. If we look at the theorems blast uses to prove ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B (how this can be done is described in Section 3.7 of the Isabelle Cookbook), we see that Relation.converse_iff plays a role, which was declared with the iff attribute. I did not understand this mysterious reference. Which version of the Cookbook, which page exactly? It is less mysterious than other references on this list... Section 3.7, p. 66ff in [1] gives recipes how proof terms can be inspected. It is what worked best for me for getting ideas of blast proofs. ` Using only canonical information reveals these possibilities that might be little known: * print_options: blast_trace, blast_stats, but this looks a bit chatty and of limited practical use They seem to be mostly useful for debugging blast itself. [1] http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/file/95d6853dec4a/progtutorial.pdf -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] lemma addition
On 25.07.2013 04:16, Christian Sternagel wrote: While the following lemma is proved automatically lemma converse_subset: A¯ ⊆ B¯ ⟷ A ⊆ B by auto I'm not sure exactly how, since simp_trace shows no application of simplification rules and neither of the rules suggested by different ATPs through sledgehammer are -- as far as I can tell -- automatic rules in the sense of [intro], [elim], [dest]. auto's call to safe splits it to goal (2 subgoals): 1. ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B 2. ⋀a b. A ⊆ B ⟹ (b, a) ∈ A ⟹ (b, a) ∈ B Both of which are discharged by blast. If we look at the theorems blast uses to prove ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B (how this can be done is described in Section 3.7 of the Isabelle Cookbook), we see that Relation.converse_iff plays a role, which was declared with the iff attribute. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proper AFP history on the web
On 10.07.2013 17:29, Makarius wrote: Is there a proper way to access AFP history on the web What about the clone at TUM, i.e. http://isabelle.in.tum.de/repos/AFP/? This should be updated regularly by Mira. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Subscripts within identifiers
On 02.07.2013 13:15, Makarius wrote: After 10 years we actually have a chance to stop such jokes about identifiers starting or ending with control symbols, or control symbols getting out of sync, and especially the confusion about which of the two subscript controls is what. Nice! What do you mean by getting out of sync in contrast to starting/ending with control symbols? * There is just one \^sub and \^sup control symbol to that effect; \^isub and \^isup remain within the infinite collection of Isabelle symbols without any special meaning. I.e., in the notation below they are not are LETTERs anymore and the then-current IDEs will stop rendering them as sub-/superscripts? * Superscript is for explicit notation, e.g. x\^sup2 for some operator _\^sup2 applied to term x. Graph_Theory/Digraph from the AFP defines a constant reachable with syntax (_ \rightarrow\^isup*\index _ [100,100] 40) (this should probably by infix instead). Is this going to stay valid (with \^isup replaced by \^sup)? It does not quite fit the scheme you described above. * Subscript may get used within identifiers, e.g. x\^sub2 for a variable of that name. This proposal excludes superscripts from occurring in identifiers. Does this mean that there was no legitimate use of \isup at all? Instead of making \^sub a letter as was done in Isabelle2003, the syntax is changed like this: LETTER = A .. Z a .. Z \alpha ... \A ... \a ... etc. DIGIT = 0 .. 9 LETDIG = LETTER | DIGIT | _ | ' SUBSCRIPT = \^sub IDENTIFIER = LETTER ( SUBSCRIPT? LETDIG )* [ I always assumed the _ was also excluded from occurring at the end of a (parsed) identifier? ] Best regards, Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Subscripts within identifiers
On 02.07.2013 18:00, Makarius wrote: * There is just one \^sub and \^sup control symbol to that effect; \^isub and \^isup remain within the infinite collection of Isabelle symbols without any special meaning. I.e., in the notation below they are not are LETTERs anymore and the then-current IDEs will stop rendering them as sub-/superscripts? I do not understand the LETTER aspect in this question. The front-ends interpret certain control symbols independently of these token syntax considerations: \^sub1 is rendered accordingly, wherever it occurs. I meant to refer to \^isub and \^isup only in my question above. As far as I inderstood your post, only LETTERs, DIGITs, _ and a restricted usage of \^sub may occur in identifiers. So the LETTER aspect of my question boils down to whether these symbols are still going to be allowed in identifiers. (_ \rightarrow\^isup*\index _ [100,100] 40) [...] The above looks fine to me. It would merely come out as \rightarrow\^sup*\index. The \index part then uses \^bsub..\^esub as usual. (Many years ago there would have been a conflict with \^subDIGIT for the index slot, but that has disappeared some years ago.) Ok, then my theories shouldn't have any problems with the proposed changes. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Formatting AFP Devel-Entries
Hi, the table for the devel-entries is not formatted correctly, e.g. in http://afp.sourceforge.net/devel-entries/Graph_Theory.shtml The status field shows Status: [-STATUS-] and has no background, in contrast to the rest of the table. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Formatting AFP Devel-Entries
On 17.06.2013 19:31, Gerwin Klein wrote: Hi Lars, thanks for spotting that. I know what's going wrong (I'm parsing isabelle build output wrong), and I have a more fundamental fix for it almost ready to go, but it's on my computer at home which I can't access while travelling. I'll be back end of June and will push it then. Thanks for looking into that. A more severe problem is that the URLs in the BibTeX data are wrong (both for devel and release), they are missing the .shtml suffix. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Strange interaction of locales and constant definitions
On 22.05.2013 22:16, Clemens Ballarin wrote: This is a fairly complex interaction of structure declarations, the overloaded constant pow aka (^) and parsing of a locale expression. It would be interesting to see whether this problem is already present in early 2009 or was introduced later. HOL-Algebra has not changed much since 2009. I tested the releases and it seems that this problem was introduced between 2009-2 and 2011. It works in 2009, 2009-1 and 2009-2. It does not work in 2011, 2012, 2013 and the current repository version. I didn't test 2011-1. BTW: Do you agree with me that M shouldn't be declared as structure? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Global build failures of the AFP in the testboard
On 17.05.2013 17:24, Makarius wrote: On Thu, 16 May 2013, Lars Noschinski wrote: - ML_PLATFORM=x86-linux ML_HOME=/home/polyml/polyml-svn/x86-linux ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - and I would simplify this to: - ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - [...] Alternatively, you could just make a general default of --gcthreads 4 for all machines as decent approximation. This is what I did now, see revision 9ce4a76615bb9. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On 21.05.2013 13:59, Makarius wrote: I do this usually by searching backwards for context (which means I might miss contexts opened by locale) or manually search through the sidekick. To check whether I am in a local context at all, I usually insert an additional end command and look for an error. BTW, there is also the old-fashioned TTY command print_context to ask the prover. It is more relevant in non-trivial contexts like 'interpretation'. On the other hand, all these things should be more immediate in the Prover IDE, as generated templates or similar. I did not know about print_context, which solves my immediate use case. This command is not documented in the reference manual (at least not in the index), though. Also, it only seems to work half-way for unnamed contexts: - If I open an unnamed context with some fixes, assumes in the theory context, print_context ignores this, i.e. in theory Foo imports Main begin context fixes P assumes P begin print_context outputs only theory Foo. - This is different inside a named context: theory Foo imports Main begin locale A begin context fixes P assumes P begin yields theory Foo locale A = fixes P :: bool assumes P as output of print_context. Although this might also be considered slightly irritating, as those elements are not part of the locale, so something like theory Foo locale A context fixes P :: bool assumes P would be better. How is interpretation related to print_context? It seems that neither interpret nor interpretation extends the context as displayed by print_context? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On 23.04.2013 19:37, Florian Haftmann wrote:
See now http://isabelle.in.tum.de/repos/isabelle/rev/e4b5bebe5235.
This does not seem to work for me in 06db08182c4b:
-
theory Interpretation imports Main begin
locale A begin
definition f :: bool where f ≡ True
end
context begin
interpretation I: A by unfold_locales
thm I.f_def (* Unknown fact I.f_def *)
end
interpretation I: A by unfold_locales
thm I.f_def (* Works *)
-
It seems that the interpretation inside the context block has no effect
at all?
When following the suggestions of the ML code
http://isabelle.in.tum.de/repos/isabelle/file/9e4220605179/src/Pure/Isar/expression.ML#l42
I am personally still in favor of only three Isar keywords, corresponding to
permanent_interpretation
ephemeral_interpretation
interpret
with the perspective to generalize permanent_interpretation from named
targets to arbitrary targets by means of a dedicated local theory
operation, like Local_Theory.subscription in the previous series of
patches. But for the moment I will leave this aside anyway.
I don't know whether this is what you are talking about, but there is
one functionality I would like to have for my Graph theory:
I have a locale (or rather, a locale hierarchy) describing a single
graph. I chose this formalization as I usually talk about a single
graph. However, if I want to talk about multiple graphs (for example
because I want to prove properties of union) it would be nice to
switch to a mode of working as in HOL-Algebra (i.e. have an explicit
domain and all lemmas only hold for elements of the domain).
It seems with your suggestion above, I could do something like
--
locale graphs =
defines GG = {G. graph G}
begin
context
fixes G assumes G : GG
begin
permanent_interpretation graph G sorry
end
--
to get all the lemmas of graph in graph, with the additional assumption
G : GG. Of course, one would need to transfer the automation manually,
as in particular elim and dest are not stable under such a transformation.
-- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The-operator
On 22.05.2013 17:14, Roger H. wrote:
how can i prove the following:
( THE A. {a. f a = {c1, c2, c3}} = {a. f a = A} ) = {c1, c2, c3} ?
This is a topic for the isabelle-users mailing list; this mailing list
is for topics specific to the developer version of Isabelle.
But the answer is: You don't; nitpick will give you a counter-example.
-- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On 21.05.2013 12:46, Makarius wrote: An old idea on my list is to add some support to the Prover IDE to rework theories with many consecutive (in a) to use just one context a begin ... end around it -- this is also more efficient. Apart from that I have occasionally considered to provide explicit fold support for such contexts in the editor -- the canonical layout does not have any indentation here. I don't know whether context blocks are an important unit for folding, but something I have missed recently is a quick way to find out in what context I am at a certain point in my theory. I do this usually by searching backwards for context (which means I might miss contexts opened by locale) or manually search through the sidekick. To check whether I am in a local context at all, I usually insert an additional end command and look for an error. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Global build failures of the AFP in the testboard
On 16.05.2013 00:43, Gerwin Klein wrote: On 16.05.2013, at 1:25 AM, Lars Noschinskinosch...@in.tum.de wrote: @Alex, Gerwin: Is there any reason remaining why the AFP should not use the default PolyML version? I remember Alex and I dropped a similar override from the Isabelle tests. Not that I am aware of. The main reason there was an explicit version mention there was to keep track of what exactly was running and where it came from. We have a record of that now with the component system, so that can be dropped. Ok. Currently the options are - ML_PLATFORM=x86-linux ML_HOME=/home/polyml/polyml-svn/x86-linux ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - and I would simplify this to: - ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - Since AFP tests run both on lxbroy10 (for the testboard) and lxbroy8 (for main); should I add a special case for lxbroy10 with --gcthreads 8? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Global build failures of the AFP in the testboard
On 15.05.2013 15:55, Makarius wrote: On Thu, 25 Apr 2013, Dmitriy Traytel wrote: http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694 Side-remark about mira configuration: the log says ML_HOME=/home/polyml/polyml-svn/x86-linux but that SVN version is often fluctuating, depending on current experiments with the SVN, and usually lagging behind. The latest official release version is here: /home/polyml/polyml-5.5.0 or even just what Admin/components/main specifies. For best performance on hardware with many cores, ML options like this usually help: ML_OPTIONS=-H 1000 --gcthreads 4 or ML_OPTIONS=-H 1000 --gcthreads 8 Where are these mira/testboard options anyway? Normally the entry points for anything like that is Admin/ within the Isabelle repository, such as Admin/isatest/. The basic configuration of the Mira system is at ~isatest/testbench/mira/settings/settings.py (for testboard), resp. ~isatest/testbench-main/mira/settings/settings.py (for reports) and includes the configurations from the repositories (e.g. Isabelle:Admin/mira.py or AFP:admin/mira.py). The latter overrides the ML settings. @Alex, Gerwin: Is there any reason remaining why the AFP should not use the default PolyML version? I remember Alex and I dropped a similar override from the Isabelle tests. Caveat: The settings (both global and repository-specific) are only loaded once when the mira daemon is started. If they change it is necessary to restart the daemon. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Webview for AFP repository?
On 21.04.2013 02:13, Florian Haftmann wrote: Hi all, what appears to me as the official webview for the AFP repository (http://hg.code.sf.net/p/afp/code) appears very poor in style, due to a missing stylesheet (hg.code.sf.net/p/afp/code/static/style-paper.css), I guess. There is also http://sourceforge.net/p/afp/code/ci/tip/tree/. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Highlighting of locale variables
Hi, I wonder whether it would be a good idea to distinguish the syntax highlighting for free variables and free variables fixed by a locale (locale variables). It seems that this information is already available to the IDE (these variables are marked as fixed when hovering). Rationale: In the locale context, these locale variables are morally constants. Somebody suggested to highlight locale variables like constants, but personally I'd prefer a highlighting similar to variables obtained or fixed in a proof (maybe a non-bold orange?). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Highlighting of locale variables
On 12.04.2013 15:24, Makarius wrote: On Fri, 12 Apr 2013, Lars Noschinski wrote: Rationale: In the locale context, these locale variables are morally constants. Somebody suggested to highlight locale variables like constants, but personally I'd prefer a highlighting similar to variables obtained or fixed in a proof (maybe a non-bold orange?). [...] Can you point to situations where this is still treated differently? Such incidents are mostly coming from the depths of time, as Larry usually calls this. I was referring to variable fixed by a locale. In the example below, F is always rendered like a free variable (i.e. blue); although it's scope is not the lemma, but the locale. --- locale dummy = fixes F :: 'a begin lemma P F oops --- There are certain intermediate states, like undeclared frees that are implicitly fixed by the system infrastructure via auto fix, but that is slightly different. An oddity related to this is the let command. In the example below, a is rendered as an undeclared free. This feels wrong as writing such a statement seems perfectly fine, because constants and variables on the left hand side are generalized anyway. --- notepad begin let ?X a = 1 + a end --- -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Revision of Big Operators on sets
On 23.03.2013 20:58, Florian Haftmann wrote:
* Revised devices for recursive definitions over finite sets:
- Only one fundamental fold combinator on finite set remains:
Finite_Set.fold :: ('a = 'b = 'b) = 'b = 'a set = 'b
This is now identity on infinite sets.
- Locales (»mini packages«) for fundamental definitions with
Finite_Set.fold: folding, folding_idem.
Before this revision there we had the lemma Min.in_idem. What replaces
this lemma?
My first try was making min an instance of folding_idem, but apparently
the F in folding_idem is separate from the one in Min_def. So, what is
the intended way to recover this lemma?
interpret Min: folding_idem min :: ('a :: {bot,linorder} ⇒ 'a ⇒
'a) bot
by unfold_locales (simp_all add: fun_eq_iff min_max.inf.left_commute)
-- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
On 11.03.2013 17:51, Makarius wrote: This looks just like making the meaning of indentation a bit more formal. Lets say as a mode of checking in the Prover IDE: fail if something is wrong in that respect, or paint things in funny colors. We shortly thought about this earlier and it has the appeal of formalizing an already established convention, which is definitely useful. However, there are two things which make me slightly uncomfortable with this solution: - when I'm exploring a proof which I expect to collapse into a one-line by-statement I usually don't (and don't want to) bother with indentation (this is obviously less of issue when using funny colors). - Isabelle does not have significant whitespace anywhere else (I'm aware of). It does not even consider linebreaks to be relevant. So my initial feeling about this suggestion is neat hack. Markup.proof_state is there for a long time already, to turn it into some use. Does this mean this could be implemented exclusively on the jEdit side, without touching the prover? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
There is definitely an use case for such an operation. When doing program verification, I often have long sequences of apply commands. These are either applications of the VCG or (mostly) oneliners to solve the verification conditions. To keep the proof as robust as possible, I use the classical method of indentation (=number of goals) and try to use only fastforce. But there are cases where I need to use auto[] or simp and in this cases it would be neat if I easily could indicate that a step has to solve a subgoal. Makarius makar...@sketis.net schrieb: On Fri, 8 Mar 2013, Joachim Breitner wrote: Sometimes, when I’m writing apply-script style proofs, I have wanted a way to modify a proof method foo to “Try foo on the first goal. If it solves the goal, good, if it does not solve it, fail”. Such non-trivial control structures are usually done via tactics and tacticals. There is a whole zoo of tacticals, and no point to hardwire them in the Isar method combinator syntax. The implementation manual in Isabelle2013 contains an up-to-date chapter 4 on tactical reasoning, which was derived from the classic Isabelle manuals from many years ago. There is also some explanation what it means formally to be a tactic and a proof method. The method_setup command can then be used to provide concrete Isar syntax to suitable methods in the usual manner. The Isar proof method language was designed a certain way, to arrive at stilized specifications of some operational aspects in the proof text. It has excluded any kind of programming or sophisticated control structures on purpose. In 1998 it was not clear yet if that would work out, since the big applications of that time (e.g. HOL-Bali) were done differently. In retrospect the Isar method language was more succesful in this respect than I had anticipated. We see big applications today without lots of specialized goal-state manipulation. In general the problem of what is a good proof interaction language is a very delicate one. To make serious progress, one would have to revisit what you see as Ltac and SSReflect in Coq today, and revisit it on the background of profound understanding how Isar works. Then maybe also combine it with IDE-style templating and outlines produced by the prover. 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
[isabelle-dev] jEdit: Automatic popup menus on hovers
Hi, 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). -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem with simproc enat_eq_cancel
On 01.03.2013 15:10, Andreas Lochbihler wrote: By the way, why does the failure in the simproc yield a proof error at all? Usually, simp does not raise Proof failed if it gets stuck somewhere. I guess this means that the simproc raises Proof failed which merely propagates through the simplifier. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
On 29.01.2013 17:46, Lars Noschinski wrote: On 28.11.2012 10:11, Lars Noschinski wrote: Hi everyone, mira still crashes from time to time. I got a new one today. lxbroy10 testboard `mira daemon 'bisect(Isabelle_makeall)'` was hanging for more then 10 days in Mirroring master repositories. Seems to be buried deep inside mercurial code. Happened again today (killed it after 6 hours) -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
On 28.11.2012 10:11, Lars Noschinski wrote: Hi everyone, mira still crashes from time to time. I got a new one today. lxbroy10 testboard `mira daemon 'bisect(Isabelle_makeall)'` was hanging for more then 10 days in Mirroring master repositories. Seems to be buried deep inside mercurial code. [2013-01-19 07:04:51,215] INFO mira.workbench No cases selected in this iteration. Sleeping... [2013-01-19 07:05:51,315] INFO mira.workbench Mirroring master repositories... [2013-01-29 17:39:51,426] INFO mira.daemon Encountered SIGTERM signal; terminating. Traceback (most recent call last): File /home/isatest/testbench/mira/bin/mira, line 17, in module bootstrap.cli(app_location, sys.argv[1:]) File /home/isatest/testbench/mira/mira/bootstrap.py, line 57, in cli raise SystemExit(tool(env, *args)) File /home/isatest/testbench/mira/mira/tools.py, line 118, in daemon return env.daemonize(instance_name, lambda: loop(env, scheduler_expr)) File /home/isatest/testbench/mira/mira/environment.py, line 200, in daemonize notification = partial(notify, 'mira system error')) File /home/isatest/testbench/mira/util/daemonize.py, line 80, in daemonize result = f() File /home/isatest/testbench/mira/mira/environment.py, line 172, in daemon_activity f() File /home/isatest/testbench/mira/mira/tools.py, line 118, in lambda return env.daemonize(instance_name, lambda: loop(env, scheduler_expr)) File /home/isatest/testbench/mira/mira/tools.py, line 107, in loop env.workbench.loop(mira.schedule.parse_scheduler_expr(env, scheduler_expr)) File /home/isatest/testbench/mira/mira/workbench.py, line 132, in loop repositories.mirror_all(self.env) File /home/isatest/testbench/mira/mira/repositories.py, line 53, in mirror_all repos.mirror(env) File /home/isatest/testbench/mira/mira/repository.py, line 137, in mirror mercurial.commands.pull(repository.ui, repository) File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/commands.py, line 2308, in pull other = hg.repository(cmdutil.remoteui(repo, opts), source) File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/hg.py, line 63, in repository repo = _lookup(path).instance(ui, path, create) File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/httprepo.py, line 263, in instance inst.between([(nullid, nullid)]) File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/httprepo.py, line 184, in between d = self.do_read(between, pairs=n) File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/httprepo.py, line 128, in do_read fp = self.do_cmd(cmd, **args) File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/httprepo.py, line 80, in do_cmd resp = self.urlopener.open(urllib2.Request(cu, data, headers)) File /usr/lib64/python2.7/urllib2.py, line 400, in open response = self._open(req, data) File /usr/lib64/python2.7/urllib2.py, line 418, in _open '_open', req) File /usr/lib64/python2.7/urllib2.py, line 378, in _call_chain result = func(*args) File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/url.py, line 415, in http_open return self.do_open(httpconnection, req) File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/keepalive.py, line 250, in do_open r = h.getresponse() File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/url.py, line 282, in getresponse return keepalive.HTTPConnection.getresponse(self) File /usr/local/ldist/DIR/mercurial-1.4.3/lib64/python2.7/site-packages/mercurial/keepalive.py, line 562, in safegetresponse return cls.getresponse(self) File /usr/lib64/python2.7/httplib.py, line 1030, in getresponse response.begin() File /usr/lib64/python2.7/httplib.py, line 407, in begin version, status, reason = self._read_status() File /usr/lib64/python2.7/httplib.py, line 365, in _read_status line = self.fp.readline() File /usr/lib64/python2.7/socket.py, line 430, in readline data = recv(1) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Pushing to testboard fails
Hi, I just tried pushing some commit to the testboard (via ssh://nosch...@lxbroy10.informatik.tu-muenchen.de//home/isabelle-repository/repos/testboard ) and it failed with: hg push -f testboard pushing to ssh://nosch...@lxbroy10.informatik.tu-muenchen.de//home/isabelle-repository/repos/testboard searching for changes remote: abort: could not lock repository /home/isabelle-repository/repos/testboard: Permission denied abort: unexpected response: empty string Is this still the right URL? Or is something broken on the server side? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Repository and Wiki [was: push request (Sublist.thy)]
On 17.12.2012 12:13, Makarius wrote: We merely need to learn where to draw the line. For example, the isatest settings have greatly benefitted from being exposed in Admin/isatest/settings under official version control. Before it was always a guess in the dark what isatest was using in a failed test in the first place. AFAIK this is still a problem with mira. Unless something changed recently, mira uses the version of isabelle/Admin/mira.py present when the mira daemon was started, which is not a very well-defined notion. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
On 28.11.2012 10:11, Lars Noschinski wrote: Hi everyone, mira still crashes from time to time. Sometimes, it is not a programming error, but some external error condition which could maybe be handled more gracefully: Next error condition: Isabelle fails to produce any heap image. I have no idea what failed there (the commit on which it failed seems to be working and the crash ), but it should not crash mira (see attached logs). Strictly speaking, this is a problem of the supplied AFP/admin/mira.py and Isabelle/Admin/mira.py scripts. I am not sure what the correct fix is -- catch any exception (except RTS stuff) in there, on the account that user configuration should not be able to bring down the daemon or just fix these functions locally to report that there is no data to report. I am leaning to the latter, at the moment. What kind of data my these functions return? -- Lars [2012-12-14 08:35:22,443] INFO mira.workbench Scheduling... [2012-12-14 08:35:22,500] INFO mira.workbench Running AFP(0799339fea0f3cdf961a3c6f1bf3b48a68fec48b:Isabelle,f583cbc458949a6de760655bf14fbc7bb94cecab:AFP)... [2012-12-14 08:35:22,625] INFO mira.workbench Updating workbench... [2012-12-14 08:35:31,310] INFO mira.workbench Executing... [2012-12-14 08:36:22,867] CRITICAL mira *** [2012-12-14 08:36:22,867] CRITICAL mira mira system error [2012-12-14 08:36:22,867] CRITICAL mira *** [2012-12-14 08:36:22,867] CRITICAL mira Traceback (most recent call last): File /home/isatest/testbench/mira/util/daemonize.py, line 80, in daemonize result = f() File /home/isatest/testbench/mira/mira/environment.py, line 174, in daemon_activity f() File /home/isatest/testbench/mira/mira/tools.py, line 117, in lambda return env.daemonize(instance_name, lambda: loop(env, scheduler_expr)) File /home/isatest/testbench/mira/mira/tools.py, line 106, in loop env.workbench.loop(mira.schedule.parse_scheduler_expr(env, scheduler_expr)) File /home/isatest/testbench/mira/mira/workbench.py, line 141, in loop report = self.run(case) File /home/isatest/testbench/mira/mira/workbench.py, line 96, in run return tuple(self.run_stepwise(case))[-1] File /home/isatest/testbench/mira/mira/workbench.py, line 69, in run_stepwise self.env.get_configuration(case.conf).impl(self.env, case, locs, dep_paths, playground) File string, line 31, in AFP File string, line 134, in isabelle_build File string, line 96, in extract_report_data File string, line 90, in extract_image_size OSError: [Errno 2] No such file or directory: '/tmp/mira/workbench/61855-140069064406784/Isabelle/heaps/polyml-5.5.0_x86-linux' [2012-12-14 08:36:22,867] CRITICAL mira *** [2012-12-03 23:00:29,505] INFO mira.workbench Scheduling... [2012-12-03 23:00:29,659] INFO mira.workbench Running Isabelle_makeall(e83037efa69482ccf8ade001628366d5dd8c47bd:Isabelle)... [2012-12-03 23:00:29,726] INFO mira.workbench Updating workbench... [2012-12-03 23:00:34,564] INFO mira.workbench Executing... [2012-12-03 23:01:39,472] CRITICAL mira ** [2012-12-03 23:01:39,473] CRITICAL mira mira system error [2012-12-03 23:01:39,473] CRITICAL mira ** [2012-12-03 23:01:39,473] CRITICAL mira Traceback (most recent call last): File /home/isatest/testbench/mira/util/daemonize.py, line 80, in daemonize result = f() File /home/isatest/testbench/mira/mira/environment.py, line 174, in daemon_activity f() File /home/isatest/testbench/mira/mira/tools.py, line 117, in lambda return env.daemonize(instance_name, lambda: loop(env, scheduler_expr)) File /home/isatest/testbench/mira/mira/tools.py, line 106, in loop env.workbench.loop(mira.schedule.parse_scheduler_expr(env, scheduler_expr)) File /home/isatest/testbench/mira/mira/workbench.py, line 141, in loop report = self.run(case) File /home/isatest/testbench/mira/mira/workbench.py, line 96, in run return tuple(self.run_stepwise(case))[-1] File /home/isatest/testbench/mira/mira/workbench.py, line 69, in run_stepwise self.env.get_configuration(case.conf).impl(self.env, case, locs, dep_paths, playground) File string, line 175, in Isabelle_makeall File string, line 134, in isabelle_build File string, line 96, in extract_report_data File string, line 90, in extract_image_size OSError: [Errno 2] No such file or directory: '/tmp/mira/workbench/59205-140114537547520/Isabelle/heaps
Re: [isabelle-dev] Reasons mira crashes
On 14.12.2012 09:40, Lars Noschinski wrote: On 28.11.2012 10:11, Lars Noschinski wrote: Hi everyone, mira still crashes from time to time. Sometimes, it is not a programming error, but some external error condition which could maybe be handled more gracefully: Next error condition: Isabelle fails to produce any heap image. I have no idea what failed there (the commit on which it failed seems to be working and the crash ), First I thought, the reason it failed was that it was still using an old version of Mira (16f40e322e50) from 9 months ago, still unaware of the changes related to the components. But even after updating the mira repository and restarting, it still fails. but it should not crash mira (see attached logs). This still stands. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Must the AFP be used as a component? (was: Reasons mira crashes)
On 14.12.2012 10:12, Lars Noschinski wrote: On 14.12.2012 09:40, Lars Noschinski wrote: On 28.11.2012 10:11, Lars Noschinski wrote: Hi everyone, mira still crashes from time to time. Sometimes, it is not a programming error, but some external error condition which could maybe be handled more gracefully: Next error condition: Isabelle fails to produce any heap image. I have no idea what failed there (the commit on which it failed seems to be working and the crash ), First I thought, the reason it failed was that it was still using an old version of Mira (16f40e322e50) from 9 months ago, still unaware of the changes related to the components. But even after updating the mira repository and restarting, it still fails. Found the reason of the failure now. Mira executes /bin/isabelle build -s -v -j 6 -d $PATH_TO_AFP/thys/ -g AFP which then terminates with Session Open_Induction (AFP) Undefined environment variable: AFP Finished at Fri Dec 14 10:41:25 CET 2012 0:00:17 elapsed time, 0:00:21 cpu time, factor 1.23 before anything was built (hence no data to collect for Mira, hence the crash). The reason is that Open_Induction/ROOT (and also Open_Induction/Open_Induction.thy) relies on $AFP being set, which is only the case if AFP is registered as a component (which is not the case for Mira). @Gerwin: Since you made the ROOT file, what was the intention of using $AFP instead of ../ used in all other theories? Also, I wonder why this did not occur before ... OT: I just saw this: What is the reason for mira writing init_components $COMPONENT/contrib $ISABELLE_HOME/Admin/components/main instead of init_components $ISABELLE_HOME/contrib $ISABELLE_HOME/Admin/components/main to the settings file? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] push request (Sublist.thy)
On 14.12.2012 14:23, Johannes Hölzl wrote: Why is there again this diverging clone of important administrative information? So the community wiki is not about Isabelle community at all, but to make administration harder by putting unreliable information snippets on a virtual whiteboard. I feel better having a Whiteboard where people actually feel encouraged to add information, then when this information is just not recorded anywhere because it would be too much hassle. Also, as far as discoverability of documentation goes, sticking it in Admin/ between a number scripts which are mostly relevant to the Release Maintainer ranks pretty low. I would like to add that there is also the config_tum repository, which Florian created when he wanted administrative information neither in the Wiki nor in the public Isabelle repository. I probably would have looked there (as it contains some mira administration info), but never in the Isabelle repository. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] getting development version to work
On 11.12.2012 17:57, Aaron Gray wrote: Lars, On 11 December 2012 08:49, Lars Noschinski nosch...@in.tum.de mailto:nosch...@in.tum.de wrote: On 10.12.2012 19:54, Aaron Gray wrote: I cannot get the 'isabelle components -a' to work on Fedora 17, it just returns doing nothing at all with no message. I will be looking into this when I get some more time, hints on how to debug this would be well appreciated. Did you read README_REPOSITORY and added the init_components lines given there to your ~/.isabelle/etc/settings files? What does 'isabelle components -l' say? Its missing all the 'contrib' directory entries as compared to Ubuntu's. Are those entries missing entirely or are they in the 'Missing components' category? The former one definitely suggests that you did not add the init_components lines to your settings file (are you sure its in the right location?). If its the latter and 'isabelle components -a' does not do anything, this suggests some problem with the components tool (or its dependencies). -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] getting development version to work
On 10.12.2012 19:54, Aaron Gray wrote: I cannot get the 'isabelle components -a' to work on Fedora 17, it just returns doing nothing at all with no message. I will be looking into this when I get some more time, hints on how to debug this would be well appreciated. Did you read README_REPOSITORY and added the init_components lines given there to your ~/.isabelle/etc/settings files? What does 'isabelle components -l' say? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Editing large sessions with Isabelle/jEdit
On 06.12.2012 14:20, Makarius wrote: On Thu, 6 Dec 2012, Lars Noschinski wrote: Does this also influence memory usage? Probably not. In general one also needs to distinguish ML and JVM resources. David Matthews made Poly/ML 5.5.0 ultra-smart in memory management, and the JVM still cannot quite compete. [...] So this seems to mean JVM memory ... Yes, I was talking about JVM memory (which is shown in the lower right corner of jEdit). With sort-of, I mean that the word stopped for a few seconds (apparently for garbage collection). Memory usage then dropped to around 750 of 1000MiB, but filled up very quickly again, even if I was just browsing around, not making any changes (This was with my graph library, which hasn't a current, publicly available copy at the moment. But it is definitely small compared to e.g. Probability). Did you try to monitor the JVM process already? I usually use jconsole or jvisualvm. None of them is really good, so I switch back and forth and make guesses. I'll keep this in mind for the next time it happens. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
Did you try starting jEdit with -f to force a fresh build? Jasmin Blanchette jasmin.blanche...@gmail.com schrieb: Am 03.12.2012 um 23:08 schrieb Lawrence Paulson: Missing components maybe? I did isabelle components -a earlier today. In fact, the issue is likely to be related to the big upgrade that resulted from my invocation of this very command yesterday night. Jasmin ___ 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] Reasons mira crashes
On 29.11.2012 11:28, Makarius wrote: On Thu, 29 Nov 2012, Lars Noschinski wrote: We could make up a rule always go through host X (X being one of the macbroys/lxbroys) and hope it is the simultaneous access from multiple hosts and not the fact that it is laying on a NFS which makes it unreliable. I've been thinking of this occasionally, but it does not work either, because the gateway systems that are reachable for ssh from outside are fluctuating a lot. It used to be just atbroy100 as canonical example some years ago, then one had to shuffle macbroy20..29 to get some machine that happens to be available, now one occasioanlly needs to take the lxlabbroy into account. I edit my .hg/hgrc a lot these days. I now wanted to suggest isabelle.in.tum.de as an obvious choice for a gateway host, but it is not reachable via SSH from the outside =) So if there is an easy solution to more robust access of some file system served at TUM, I am for it. Anything beyond that should be a move away from home-made servers to some professional hosting platform like Bitbucket (not Sourceforge, not Google code). Note that we have already several home-made services running that are only half-maintained, and we cannot afford this for the main collection point of Isabelle changesets. I will ask the MTAs about that. Since some time they also provide hosting of mercurial repositories. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [OT] Reasons mira crashes
On 29.11.2012 11:49, Makarius wrote: For future changes it might be worth to keep in mind that the Mercurial project considers the python interface as internal: http://mercurial.selenic.com/wiki/MercurialApi Right. This classification has somehow changed over the years. Back in 2008, use of the API was encouraged more. Switching to a CLI interface requires a bit of work, though. Just to recall the original motivations for using Mercurial instead of Git (which was not as aggressible marketed in 2008 as now so there was a genuine choice to be made): (1) Mercurial emphasizes a nice semantic model of monotonic history and immutable changes (in coincidence with the Isabelle/ML approach and the then emerging PIDE document model). This is true for the UI, for the underlying model Git is the pure one: If you do e.g. a rebase, mercurial makes a non-monotonic change to its storage, while Git preserves the old history, and only changes the branch pointer. The slight tendency away from Python APIs is another thing. Since Isabelle/Scala is the official system programming language for quite some time already, I've occasionally checked the situation for JVM-based access to Mercurial operations. Projects like http://hg4j.com/ are not very far yet. JGit is said to be stable and full-featured. [But of course, changing our choice is not an option at this point.] -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [OT] Reasons mira crashes
On 29.11.2012 12:13, Makarius wrote: Does JGit work smoothly on Windows, for example? In Isabelle/Scala I play more and more funny tricks to get rid of the received Unix model of executing some process to do small auxiliary things. I would expect so: JGit is a pure Java implementation, not using C Git. You don't change such fundamental platforms without getting a real benefit from it. Of course. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
On 28.11.2012 22:18, Makarius wrote: We have the shared disk configuration, with Advantages: can use existing setup, Disadvantages: generally restricted to intranets, not generally recommended due to general issues with network filesystem reliability. I think what people are actually using now for the most part (as almost everyone uses a laptop not permanently connected to the intranet) is the ssh configuration (which of course reduces to the shared disk configuration, as everyone uses a different machine to ssh to. So we still carry a lot of CVS baggage stemming from 1993, not just in the low-level technological sense. Nothing new, all known already. I usually ignore it to avoid the trouble of thinking about more fundamental changes. We could make up a rule always go through host X (X being one of the macbroys/lxbroys) and hope it is the simultaneous access from multiple hosts and not the fact that it is laying on a NFS which makes it unreliable. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
