Re: [isabelle-dev] cvc4

> On 5 Aug 2017, at 09:16, Lawrence Paulson wrote: > > A new version has appeared and now sledgehammer always complains about > “abnormal termination”. Could you send me the following details? 1. Platform (e.g. macOS 10.12.2) 2. The output of "isabelle getenv CVC4_SOLVER" 3.

Re: [isabelle-dev] Towards the release

Hi Makarius, > The Windows platform is a bit strange, but there are usually many ways > to get things through eventually. Simon has found a way to avoid "ocamlbuild". It looks like we'll be able to have the three binaries in place before the branch. Nonetheless, Nunchaku will remain labeled as

Re: [isabelle-dev] Towards the release

Hi Makarius, > Are there any non-trivial chunks still in the commit/push pipeline that > need special considerations? I was hoping to push Nunchaku into Isabelle (source code + binary component) before the release, but we have some issues with ocamlbuild on Windows. Would it make sense to push

Re: [isabelle-dev] not-exists problem

> On 13.09.2016, at 23:33, Lawrence Paulson wrote: > > I’m not sure that this suggestion addresses my original problem: that the use > of the negated quantifier (by an output translation, i.e., not by request) > produced a confusing output. This output already contains only a

Re: [isabelle-dev] Status of HOL/Library/Old_SMT.thy

> On 01.09.2016, at 22:04, Makarius wrote: > > What is the status of HOL/Library/Old_SMT.thy? It might be worthwhile to ask on isabelle-users@ to be sure. I seem to remember that Filip Maric (cc:d) showed some interest in it at some point. Jasmin

Re: [isabelle-dev] Multiset insert

Hi Bertram, > Will the introduction of add# mean that the induction principle for > multisets will be changed as well? If so, do you have a migration path > for proofs based on the current induction principle? (Currently there > are two cases, {#} and M + {#x#}; note that the singleton multiset >

Re: [isabelle-dev] Multiset insert

> I would also like to point out that for some reason, intersection and union > are #∪ and #∩, whereas all other multiset operations seem to have the # at > the end (e.g. ⊆#). Unless there is some deeper reason for this, I suggest we > change it. Good point. Indeed, I first wrote ∪# in

Re: [isabelle-dev] Multiset insert

> On 28.07.2016, at 10:33, Peter Lammich wrote: > >>> How about >>> >>> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where >>> "add# x M = {#x#} + M" > > This, however, may produce confusion with multiset union, which is an > instance of the plus type

Re: [isabelle-dev] Multiset insert

Tobias wrote: > How about > > definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where > "add# x M = {#x#} + M" Lovely! Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Multiset insert

Tobias wrote: > Did we ever discuss the naming issue? "insert_mset" would be the canonical > name, but it would make larger expressions hard to read. I'm not so sure "insert_mset" would be the right name. Its set-based terminology might suggest a definition like insert_mset x M = {#x#} #∪

Re: [isabelle-dev] Acces to internal interfaces ...

Dear Burkhart, > in Isabelle 2016, certain traditional interfaces to data-type packages > do no longer exist, for example Datatype.get_info thy typename or > its homologue on records. This function yielded for a given typename > the list of constructors together with their types, and other

Re: [isabelle-dev] Isabelle repository broken

On 24.05.2016, at 17:12, Makarius wrote: > > The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or > 6a17bcddd6c2 (eberlm). > > The failure is as follows: > ### theory "Generate_Binary_Nat" > ### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time > ***

Re: [isabelle-dev] NEWS: Highlighting of entity def/ref positions

Hi Dmitriy, Makarius, Dmitriy wrote: > At first I was a bit surprised to see the first occurrence of list, Nil, and > Cons in blue in the following datatype definitions. > > datatype 'a list = Nil | Cons 'a "'a list” > > But I guess, it makes sense to indicate that this is a new thing being

Re: [isabelle-dev] PIDE reports on mixfix annotations (notably for datatype)

Hi Makarius, You wrote: > Mixfix annotations have gained a more formal status recently, with PIDE > markup reports that lead to some highlighting and tooltips in the IDE. > [...] > BNF datatypes are a notable exception. E.g. this example produces duplicate > "bad" markup about Unicode in

Re: [isabelle-dev] PIDE reports on mixfix annotations (notably for datatype)

Hi Makarius,You wrote:Mixfix annotations have gained a more formal status recently, with PIDE markup reports that lead to some highlighting and tooltips in the IDE.[...]BNF datatypes are a notable exception. E.g. this example produces duplicate "bad" markup about Unicode in mixfix notation:

Re: [isabelle-dev] src/Doc/Corec fails

> The problem is a missing macro \textsubscript Thanks for the heads-up. I added the "subscript" package, which is supposed to help (d0fc75798baf); then I reverted that and gave up the idea of having bold subscripts (19387866eace), since there was another issue with \textsubscript (spurious

Re: [isabelle-dev] Explicit representation of multisets

> but this leads to the rather lengthy "insert_mset x M" as opposed to the > current "{#x#} + M". This would come up in all inductive proofs. If we want > to mimic sets, it actually seems unavoidable... With completion, it might actually be easier to type "insert_mset x M" than "{#x#} + M".

Re: [isabelle-dev] Jenkins maintenance window

Hi Lars, > However, turns out that the actual problem was that somebody pushed > something completely unrelated (maybe a different repository?) into > testboard. This also generated a gargantuan changelog in Jenkins. I > don't blame that person, it could happen to anyone. But we need to fix >

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

> What is special about Sudoku? You're right, probably nothing. >> SMT_Tests (requires Z3) > ... > In 2013 we did not have Z3 as default component, usable for everybody. Now > the condition on it is always true -- z3 is always enabled. We could indeed enable it by default. >> Slow: >> Brackin

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

> On 18.11.2015, at 16:26, Lawrence Paulson wrote: > > These suggestions are worth a discussion. Should we go ahead? Would anybody > like to apply this patch and test that everything still works? I could do it, if nobody has objections. Jasmin

Re: [isabelle-dev] HOL-Proofs broken?

Hi Makarius, > My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out of > resources and fail. I've made approx. 3 runs in the vicinity -- it always > takes very long. > > Is that another failure to do a full "isabelle build -a" before pushing > anything? I did "isabelle

Re: [isabelle-dev] HOL-Proofs broken?

> On 06.10.2015, at 22:37, Makarius wrote: > >> On Tue, 6 Oct 2015, Dmitriy Traytel wrote: >> >> So the main candidates for bad changesets are: ebf296fe88d7, 2ebdd603cd71. > > More results on macbroy2: > > 5b5656a63bd6 > Finished HOL-Proofs (0:18:14 elapsed time, 0:49:28

Re: [isabelle-dev] Multiset missing Nitpick_Model.unrep in 2007ea8615a2

Thanks, sorry (24b5e7579fdd). Jasmin > On 06.10.2015, at 11:42, Dmitriy Traytel wrote: > > The title says it all. > > Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Exposing some functions of the API

Hi Florian, Frédéric, Sorry for not answering this earlier. Somehow, I failed to notice that two of the three functions are my responsibility. >> During some programming tasks, I had to use the following functions: >> >> BNF_FP_Def_Sugar.co_datatype_cmd > > note that these *_cmd functions are

Re: [isabelle-dev] Sledgehammer error involving Vampire

I suspect they have updated Vampire and the new version’s proof format has changed a bit. I have it on my TODO list. Jasmin On 18.07.2015, at 23:37, Jason Dagit dag...@gmail.com wrote: On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson l...@cam.ac.uk mailto:l...@cam.ac.uk wrote: I’ve seen

Re: [isabelle-dev] Deprecating legacy ASCII symbols?

Makarius wrote: * Convenience: users somethings find it too combersome to type proper Isabelle symbols. I never do that myself, but take the time to type things nicely. It is actually not much time for me, since I implemented the input methods myself and know how they work.

Re: [isabelle-dev] Deprecating legacy ASCII symbols?

Concerning :: versus \Colon I am in favour to get rid of \Colon altogether: there is visually no difference in final LaTeX documents, and in the editor it introduces a bit too much complication to my taste. As far as I am concerned: By all means, kill it! At some point in 2014, I realized

Re: [isabelle-dev] Infix syntax for division?

Hi Florian, a) The radical solution: there is only »_ / _« for both field division and euclidean division. How natural is notation like »a / b * b + a mod b = a« then? b) The conservative solution: partial division has »_ div _«, an (the more special) field division »_ / _«. This seems more

Re: [isabelle-dev] docs for new datatype package

Hi Gerwin, From your first email: I’m still seeing a different order of premises in the rules themselves, though. Maybe that only occurs for more than 2 constructors, or it has to do with the fact that my case is not just mutual through one set of datatypes, but also involves a third

Re: [isabelle-dev] docs for new datatype package

Does it really fully unregister? Not fully: (I believe) it unregisters only the non-nested occurrences, e.g. “a” and “b” in my previous example (several emails ago). For “a list” and “b list”, there is some hope, since the old package used to do it right (keeping them apart from the fully

Re: [isabelle-dev] docs for new datatype package

Hi Gerwin, The rule set I’d need is “typ_desc_typ_struct.inducts”, which datatype_compat doesn’t generate. It does generate the four constituent rules that I can put in a set myself, but the order of premises in these rules is different to the old datatype package, which means my goal

Re: [isabelle-dev] docs for new datatype package

The rule set I’d need is “typ_desc_typ_struct.inducts”, which datatype_compat doesn’t generate. The rule you’re looking for is called “compat_a_b_a_list_b_list.induct” (no s). Actually, it’s the other way around. With the old package, the “inducts” rule is just a collection of four

Re: [isabelle-dev] docs for new datatype package

Hi Gerwin, Thanks for that pointer. FOL-Fitting looks reasonably well behaved with its 2-way nesting. This file has 4-way nesting and something seems to have changed in the order of the subgoals that the induction leaves, which makes the unstructured apply scripts a pain to update. Is

Re: [isabelle-dev] NEWS: Z3 open source

What is still not clear to me is how provers are determined. The Sledgehammer panel uses the system option sledgehammer_provers, after many failed attempts in the past to cope with the ML heuristics. In Isabelle/323feed18a92 I've tried to update this wrt. recent changes. Is it true

Re: [isabelle-dev] docs for new datatype package

Hi Gerwin, On 19.04.2015, at 20:25, Gerwin Klein gerwin.kl...@nicta.com.au wrote: Thanks for updating. Currently trying to pull through proofs in https://github.com/seL4/l4v/blob/master/tools/c-parser/umm_heap/CTypes.thy They are unfortunately pretty horrid to start with (violating

Re: [isabelle-dev] docs for new datatype package

Hi Gerwin, On 19.04.2015, at 16:45, Gerwin Klein gerwin.kl...@nicta.com.au wrote: The datatype manual says in e8472fc02fe5: The datatype_compat command is needed to register new-style datatypes for use with fun and function (Section 2.2.2) Is this still correct? Indeed, this is a

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

Hi Andreas, In Isabelle2014, processing this datatype declaration takes about one minute. So what has happened in between? (The Isabelle2014 timing panel is also way off with 8 seconds.) Thanks for your report. What happened in between is that we generate more theorems. I suspect one or a

Re: [isabelle-dev] NEWS: Z3 open source

Can you explain the status of Old_SMT? Is there anything that isatest still needs to run here? “old_smt” is there just in case. I was thinking of killing it right after the Isabelle2015 release. It’s not even tested by any regression test. People like Filip Maric, who use Z3 heavily (cf.

Re: [isabelle-dev] Someone messed up HOL_library/Multiset_Order

On 26.03.2015, at 14:00, Peter Lammich lamm...@in.tum.de wrote: Isabelle version: devel -- hg id 034b13f4efae Someone pushed a fix a few hours ago already (75433c3ee203). Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de

[isabelle-dev] Reprocessing in Isabelle/jEdit

Hi all, When editing inside Isabelle/jEdit (f19f4afa49e2), it used to be so that everything above was left alone. Now, if I edit a lemma in the middle of the window, everything above it that is visible gets reprocessed. So if I write something like thm list.exhaust it can take a couple of

Re: [isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading

Hi Chris, Just a reminder that this old thread is not yet resolved and currently I'm essentially stuck. I hope somebody who has a clue will answer your email. Independent of my being stuck, could one of the devs apply at least the first of the following attached patches (and the second

Re: [isabelle-dev] Notes on datatype_new list

Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de: The definition of list should look like before. I don't see how this is an option. This would result in the following duplicate constants: map_list vs. map set_list vs. set rel_list vs. forall_list2 un_Cons1 vs. hd

Re: [isabelle-dev] Notes on datatype_new list

Am 26.05.2014 um 12:25 schrieb Makarius makar...@sketis.net: On Sun, 25 May 2014, Jasmin Christian Blanchette wrote: The = as the name for Nil's discriminator deserves an explanation. [...] So I introduced this weird = syntax, which suggests that equality is used for discriminating. I am

Re: [isabelle-dev] Notes on datatype_new list

Am 26.05.2014 um 12:05 schrieb Makarius makar...@sketis.net: The observed here problem is different: the type constructor list somehow ends up in the name space with a concealed flag. There might be one or more Binding.conceal too many in the BNF sources. Ah, now I get it. Of course this

Re: [isabelle-dev] Notes on datatype_new list

Am 26.05.2014 um 15:24 schrieb Makarius makar...@sketis.net: I think you could afford an actual keyword for the dead modifier and use it without colon, like lazy in HOLCF/domain. That would substract dead from the normal identifier space, but merely means its very few occurrences on

Re: [isabelle-dev] Remaining uses of Proof General?

Am 25.05.2014 um 14:59 schrieb Makarius makar...@sketis.net: On Sun, 25 May 2014, Jasmin Christian Blanchette wrote: In the course of a day, I typically find myself pulling from the Isabelle repository several times. I am encouraged in this by my use of Mercurial queues. So it's not

Re: [isabelle-dev] bnf_decl axiomatization

Am 13.05.2014 um 15:35 schrieb Makarius makar...@sketis.net: On Tue, 13 May 2014, Dmitriy Traytel wrote: Let me explain Jasmin's ;): bnf_axiomatization was the name, I intended for the command first, before I was persuaded by my colleagues to correlate the name with typedecl rather than

Re: [isabelle-dev] AFP hg down?

For the record: The AFP was apparently never down. It's just my ISP at home that doesn't seem to like sourceforge.net these days. Even basic things like ping don't work from home -- but they do work when I'm logged on a TU server. Strange... Jasmin Am 23.04.2014 um 07:35 schrieb Tobias Nipkow

Re: [isabelle-dev] Issues with interpretations

Hi Andreas, 4. If anybody has any ideas on how to address Scenario 3, please let me know! I don't think that scenario 3 is the one to address. IMO the hooks should behave as if they were executed in the name space of the datatype declaration, so size is doing something sensible already.

Re: [isabelle-dev] smt2

Hi Larry, Am 15.03.2014 um 16:27 schrieb Lawrence Paulson l...@cam.ac.uk: But working very well, in my experience. I'm glad to hear that. :) Now, will smt2 calls be suitable for the Library and AFP? No, because they suffer from the exact same issues as smt calls. We could of course rethink

Re: [isabelle-dev] smt2

Hi Makarius, While experimenting with the increasingly useful Isabelle/ML IDE, I've found various spots that are awaiting further cleanup, renovation or demolition. Just some arbitrary examples: * HOL/SAT.thy with some related ML modules. I've brushed this up recently, e.g. to get

Re: [isabelle-dev] smt2

Hi Andreas, Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler andreas.lochbih...@inf.ethz.ch: On 14/03/14 14:18, Jasmin Blanchette wrote: Another candidate is Quickcheck_Narrowing.thy. Nothing in HOL seems to depend on it, and (please correct me if I'm mistaken) hardly anybody go

Re: [isabelle-dev] smt2

Hi Andreas, How big an issue is it to you if we move narrowing to Library? [...] If you do so, please make sure that the connection to the datatype packages is kept, i.e., narrowing generators are generated for all datatypes (even those that are defined while narrowing was not in scope).

Re: [isabelle-dev] HOL-IMP very slow

Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk: I’m not sure what the question is any more. If it is about the choice of names in Skolemization, that has been entirely redone in the past few years. I imagine it is now something like this: Subgoal.FOCUS (fn

Re: [isabelle-dev] [isabelle] primcorec complains about invalid map function

Hi Andreas, I read the comment to your changeset 3def821deb70, which says that Nat.pred may show up in theorems generated by primcorec. This is fine, because the destructor view for codatatypes goes well with discriminators and selectors for datatypes. As I do not know where discriminators

Re: [isabelle-dev] HOL-IMP very slow

Am 12.02.2014 um 20:40 schrieb Makarius makar...@sketis.net: Mainly the proof reconstruction on the Isabelle side, especially the question of type variables. I can't help much there. Perhaps Larry knows more. All I can recall is that Metis sometimes suggests type instantiations (since types

Re: [isabelle-dev] NEWS: New (co)datatype package is now in Main

Am 22.01.2014 um 21:18 schrieb Makarius makar...@sketis.net: On Tue, 21 Jan 2014, Jasmin Christian Blanchette wrote: This brings the new (co)datatype package where we want it to be for the next release. Great. This is a big step forward. Thank you for your kind words. I would like to

Re: [isabelle-dev] NEWS: New (co)datatype package is now in Main

Hi Larry, Am 23.01.2014 um 14:38 schrieb Lawrence Paulson l...@cam.ac.uk: Great news! I hope to see a brief announcement paper illustrating some of the new things that can be done. Or did you publish that last year? I believe you are on the committee of a conference where such a paper has

Re: [isabelle-dev] AFP failures

Am 26.11.2013 um 13:01 schrieb Dmitriy Traytel tray...@in.tum.de: Zorn is supposed to move to Main together with the new (co)datatype package. I guess it was removed from Library only by mistake. Yes, it should definitely be in Library for now. My change 483131676087 took it out by mistake.

Re: [isabelle-dev] New (Co)datatypes: Status Plan 2

Hi Makarius, Am 20.11.2013 um 14:12 schrieb Makarius makar...@sketis.net: Dmitriy had sent me some explanations which sessions represent the material to be moved to HOL in either case, but I never tried it out myself. It is high time to do that now. In particularly I would like to get a

Re: [isabelle-dev] New (Co)datatypes: Status Plan 2

Am 20.11.2013 um 17:17 schrieb Makarius makar...@sketis.net: We have a bad state in Isabelle/d983a020489d: * HOL-BNF_Example fails like this: *** Theory loader: failed to load Gram_Lang (unresolved DTree) *** Theory loader: failed to load Parallel (unresolved DTree) *** Extra variables

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

Hi Alex, (Briefly reviving an old thread...) Am 06.08.2013 um 00:36 schrieb Alexander Krauss kra...@in.tum.de: In summary, except for the size functions which are somewhat special (and only used for termination proofs), the function package never uses any inductiveness and would happily

Re: [isabelle-dev] Isabelle/jEdit doesn't process theories

Am 25.09.2013 um 13:03 schrieb Makarius makar...@sketis.net: On Wed, 25 Sep 2013, Jasmin Christian Blanchette wrote: Isabelle/jEdit is currently unwilling to process theories The file is correctly opened, but nothing is processed -- no imports are processed, the theory text has a pink

Re: [isabelle-dev] The coming release

Am 24.09.2013 um 22:10 schrieb Makarius makar...@sketis.net: OK, I will tell you when we are getting close to the fork point. Thanks. We'll try to maintain the ready to be forked invariant, but it's always good to have advance notice, if nothing else so that we avoid bigger changes right

Re: [isabelle-dev] Total failure of sledgehammer

Hi Larry, Am 13.09.2013 um 21:17 schrieb Lawrence Paulson l...@cam.ac.uk: That fixed it. One of the Australians has run into the same issue with MaSh. The issue should be addressed starting with Isabelle/8d9f4e89d8c8. If you're willing to give MaSh a second try, you could try to set MASH=yes

Re: [isabelle-dev] Missing letters in jEdit

Am 18.09.2013 um 16:51 schrieb Makarius makar...@sketis.net: OK, just a few more details: The jEdit Global Options / Text Area pane has various tuning parameters that affect the font style. What are your preferences for the following? Anti Aliased smooth text Fractional font metrics

Re: [isabelle-dev] Missing letters in jEdit

Hi Makarius, This looks really bad, and needs to be investigated further. I've not seen such a bad visual drop-out in the past 1-2 years, despite many minor mistakes in the painting of Java on many different platforms. I might be also responsible myself, potentially doing some text

Re: [isabelle-dev] Total failure of sledgehammer

Am 13.09.2013 um 09:34 schrieb Lawrence Paulson l...@cam.ac.uk: None of them work. Can you reproduce it in Proof General? As an additional test, you could try playing with options like debug and see if the output says anything interesting. Just to make sure it's not MaSh-related somehow, I

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

Hi Florian, An example could be something like primitive_recursion card :: 'a set = nat where card {} = 0 card (insert x A) = Suc (card A) proof - show !!x y. insert x o insert y = insert y o insert x show !!x. insert x o insert x = insert x qed thm card.simps -- {* card {} =

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

Hi Alex, - The package registers a datatype interpretation to generate congruence rules the case combinator for each type. I guess it would make sense to have the package do that, or is there a specific reason why it is better to do it in a function-related extension? - The pattern

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

Hi Florian, Am 04.08.2013 um 18:57 schrieb Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: has an explicit need for a »nested to mutual« mode ever been articulated? Yes, on a couple of occasions. First, as Dmitriy mentioned, compatibility is important -- I certainly don't want

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

Am 01.08.2013 um 18:15 schrieb Makarius makar...@sketis.net: Another important missing piece is primcorec. What is the proper technical term for that? Isn't it just corec? If the proper name for primrec is primrec, then the proper name for this is primcorec. I wouldn't mind killing the

[isabelle-dev] Build error (isabelle.Build not found)

Hi all, I just updated Isabelle to af8ecf09a58c (from a version that was one or two days old) and whenever I try to build HOL, I get this error: isabelle build -c -b HOL Fehler: Hauptklasse isabelle.Build konnte nicht gefunden oder geladen werden 0:00:00 elapsed time, 0:00:00 cpu

[isabelle-dev] Max threads Sledgehammer

Hi Makarius, Change cb5cdbb645cd (clarified bootstrapping of Pure) altered the semantics of Multithreading.max_threads_value () with Poly/ML. Namely, all of a sudden the function returns 1 instead of 4 on a 4-CPU machine, which seems strage as a default for a function called

[isabelle-dev] SMT in Isabelle2013 (was: Re: AFP: Session AVL-Trees broken)

is incomplete with respect to Joe Hurd's Metis, even though the prover has only six simple well-documented proof rules.) Incompleteness can strike any time. Anfang der weitergeleiteten E-Mail: Von: Jasmin Blanchette jasmin.blanche...@gmail.com Datum: 29. Oktober 2012 13:11:49 MEZ An: Sascha

Re: [isabelle-dev] AFP: Session AVL-Trees broken

Am 01.01.2013 um 22:38 schrieb Makarius: Anyway, since the smt method seems to work right now, I propose to wire up a test where smt_certificates and smt_read_only_certificates are left unchanged if ISABELLE_FULL_TEST is enabled. Does that make sense, according to the meaning of these

Re: [isabelle-dev] AFP: Session AVL-Trees broken

Am 01.01.2013 um 14:29 schrieb Makarius: Testing it briefly myself, it works except for SMT_Word_Examples: Solver z3: Z3 proof parser (line 2): unknown sort: bv Could you give me some details about how/where this occurs exactly? The SMT_Word_Examples.thy file starts with declare

Re: [isabelle-dev] Permission denied

Am 10.12.2012 um 15:28 schrieb Makarius: See also this old thread: http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03001.html Interesting. Unfortunately, I get the same errors with macbroy20, 21, 22, 23... Jasmin ___

Re: [isabelle-dev] Two problems

Am 08.12.2012 um 14:07 schrieb Makarius: In your observations above, are you sure that nondeterministically means physical nondeterminism, say due to parallel loading of theories? Or theories that you have visited before in Proof General, before starting the above one? Each time I

Re: [isabelle-dev] Status of HOL/SMT

Am 04.12.2012 um 15:06 schrieb Makarius: If you provide a state where the SMT_Examples session can reproduce its proofs, I'll try to. Last time I regenerated the certificate, there were a couple of cases where I was not successful with 3.2 (on my Mac) and had to use 4.0. But I need to dig

Re: [isabelle-dev] Status of HOL/SMT

Am 04.12.2012 um 15:29 schrieb Makarius: The question which SMT/Z3 version to ship with the release basically has time until the new year. I'm a big fan of if it ain't broken don't fix it, so let's defaut on 3.2, and in the unlikely event that both the parser issue with 4.0 and rewr_conv are

Re: [isabelle-dev] Status of HOL/SMT

Am 04.12.2012 um 18:11 schrieb Johannes Hölzl: I remove the SMT certificates in HOL-Multivariate_Analysis in Isabelle/4b4fe0d5ee22. Thanks! I didn't mean to apply pressure on you, though. ;) Jasmin ___ isabelle-dev mailing list

Re: [isabelle-dev] Two problems

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

Re: [isabelle-dev] Two problems

Am 04.12.2012 um 07:51 schrieb Lars Noschinski: Did you try starting jEdit with -f to force a fresh build? That did the trick. Thanks! Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de

[isabelle-dev] isabelle components -a does nothing

Hi all, I am trying to get the JDK 1.7 using the command isabelle components -a but the command returns immediately. The diagnosis command isabelle components -l prints Available components: /Users/blanchet/isabelle /Users/blanchet/isabelle/src/Tools/Code

Re: [isabelle-dev] isabelle components -a does nothing

Hi Makarius, There is still something missing, as far as I can tell from your components -l printout before. You need to init components from the Admin/components/* space explicitly to claim them, and the let components -a resolve them. The general attitude is to provide various parts

Re: [isabelle-dev] Speed of @{thm}

Am 11.08.2012 um 23:44 schrieb Makarius: On Fri, 10 Aug 2012, Jasmin Blanchette wrote: Now, here's something really strange. If I replace fun thm_bind kind a i = val ^ a ^ = the_ ^ kind ^ (ML_Context.the_local_context ()) ^ string_of_int i ^ ;\n; with fun my_ctxt

Re: [isabelle-dev] Speed of @{thm}

Am 10.08.2012 um 23:43 schrieb Makarius: On Fri, 10 Aug 2012, Jasmin Blanchette wrote: The slowdown is neither in put_thms nor the_thm(s), but apparently rather in the compiler somehow. The ML code in ml appears to be executed two orders of magnitude slower than normal ML code

[isabelle-dev] Speed of @{thm}

Hi all, In the new codatatype package, which we aim at integrating into Isabelle soon, there are 1277 @{thm} annotations spread over about 10 000 lines of ML. On my machine, each @{thm} costs about 30 ms, which means that 40 s of CPU time is spent alone looking up theorems whenever we load or

Re: [isabelle-dev] Speed of @{thm}

Am 10.08.2012 um 20:02 schrieb Makarius: 30ms for the conjuring trick with fully abstract @{thm} is odd, it should not happen. Can you spend some time to figure out the time hole? The delta between @{thm} and @{fasthm} is really just a couple of lines of code: val i = serial ();

Re: [isabelle-dev] Speed of @{thm}

Am 10.08.2012 um 22:21 schrieb Makarius: On Fri, 10 Aug 2012, Jasmin Blanchette wrote: I'm attaching my test files for the record. Dmitriy tried these already and confirmed my measurements. OK, I will also look for the fat. The slowdown is neither in put_thms nor the_thm(s

Re: [isabelle-dev] sledgehammer / yices

Am 19.07.2012 um 12:49 schrieb Sascha Boehme: I don't know for sure. It might be that YICES_INSTALLED and friends were added as a sanity check to avoid errors when invoking the solver locally and it doesn't exist. If that's the case, it's probably better to remove YICES_INSTALLED and just

Re: [isabelle-dev] Sledgehammer on Cygwin

Am 24.04.2012 um 17:21 schrieb Makarius: I did not dare to enable overlord mode so far, but doing it on your behalf it reveals the follow in prob_e_1_proof: /cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eproof: line 24:

Re: [isabelle-dev] Isabelle release test website

Hi Makarius, I suppose here that the self-extracting Isabelle_23-Apr-2012.exe archive did extract correctly, to something like 850 MB directory structure? At least it had the expected directory structure. Your existing Cygwin is probably relatively old, such that the poly.exe cannot be

Re: [isabelle-dev] spass: Internal error: exception Empty raised (line 458 of library.ML)

Am 24.04.2012 um 20:58 schrieb Makarius: have also made some more experiments. The Empty exception is from the split_last here http://isabelle.in.tum.de/repos/isabelle/file/ea153f6abdb6/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML#l614 where you don't get any output unexpectedly,

[isabelle-dev] More SPASS with Isabelle

Hi all, The automatic prover SPASS, integrated in Sledgehammer, now includes many enhancements, such as properly oriented term simplification, that should make a difference for Isabelle problems. Thanks to these, SPASS has become more effective than E, Vampire, or Z3 [1], and this is just the

Re: [isabelle-dev] Divergent renames

Hi Makarius, Good question. There is a brief explanation at http://hgbook.red-bean.com/read/mercurial-in-daily-use.html in the section Divergent renames and merging. Did it produce any merge node locally? What does hg out say? lapbroy152:HOL blanchet$ hg out Vergleiche mit

Re: [isabelle-dev] Divergent renames

Am 01.12.2011 um 13:06 schrieb Stefan Berghofer: I just got the very same warnings when updating my copy of the Isabelle sources. I already got similar warning messages warning: detected divergent renames of src/HOL/Tools/Sledgehammer/sledgehammer.ML to:

[isabelle-dev] AFP failure in Lam-ml-Normalization

Hi all, Somewhere between 43ca06e6c168 and 6975db7fd6f0, I seem to have broken the AFP entry Lam-ml-Normalization. However, I cannot reproduce the problem on my machine -- whether in Proof General nor using isabelle make. On the other hand, I do get the following disturbing messages in Proof

Re: [isabelle-dev] AFP failure in Lam-ml-Normalization

Hi Makarius, Am 17.11.2011 um 12:12 schrieb Makarius: This is merely a consequence of changeset: 45486:600682331b79 user:wenzelm date:Mon Nov 14 16:16:49 2011 +0100 files: src/Pure/Isar/runtime.ML description: more detailed exception_trace: in Poly/ML 5.4.x

  1   2   >