Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
HOL4 and HOL Light both support the (sym) syntax to remove concrete syntax fixities. I don't think HOL Light supports comments at this level. HOL4 does, using SML's (* ... *). So, if you want to write the escaped *, you have to use our older syntax for the same (using a $ for "op": $*), or you can just add spaces and write ( *), or ( * ). Michael > On 6 Oct 2015, at 23:12, Makarius wrote: > > On Tue, 22 Sep 2015, Tobias Nipkow wrote: > >> The "op" noation is idiosyncratic, but there are examples (not in individual >> formulae) where I find some such notation convenient. I would welcome >> Haskell's "(+)", but that has a problem with "(*)". Unless we can make that >> notation work, I don't think we profit much by a change. Hence I am inclined >> to leave things as they are. > > "(*)" does not work, because it is in conflict with "(* comment *)" in inner > syntax. I have recently encountered a situation where it would have been > better to replace inner comments by "-- ‹comment›", as known in outer syntax, > but the double-minus was in conflict with some infix operators. The next idea > was to replace "-- ‹comment›" by "— ‹comment›" with a newly introduced > Isabelle symbol for the mdash. > > So many clouds of dust, caused by trying to clean up obscure corners ... > > At the moment I am also inclined to leave things unchanged. > > > Makarius___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Deprecating legacy ASCII symbols?
> On 1 Jul 2015, at 00:57, Makarius wrote: > > On Tue, 30 Jun 2015, Larry Paulson wrote: > >> It is interesting to look at competing systems and note that every one of >> them appears to be fully committed to a plain ASCII syntax as the only way >> of writing a formula. I think it may still be premature to abolish having >> ASCII even as an alternative syntax. > > Maybe some HOL4 guy can explain the details. They certainly do have ways to > use non-ASCII, probably not as pervasive as for Isabelle. (I think they also > have blue, green, brown variables.) > We’ve had support for arbitrary user-chosen UTF8-encoded Unicode symbols since 2008, both in input and output. Emacs has pretty reasonable support for inputting Unicode if you turn on the TeX-input-method. Our emacs and vim editing modes further provide keybindings for common symbols (C-S-1 for ∀ is one more modifier key to press than S-1 (assuming that ! is shift-1)). We keep material under src/ as pure ASCII, but our examples/ directory is full of Unicode. E.g., val oleast_intro = store_thm( "oleast_intro", ``∀Q P. (∃α. P α) ∧ (∀α. (∀β. β < α ==> ¬ P β) ∧ P α ==> Q α) ==> Q ($oleast P)``, rw[oleast_def] >> SELECT_ELIM_TAC >> conj_tac >- (match_mp_tac ordlt_WF0 >> metis_tac[]) >> rw[]); val ordSUC_def = Define` ordSUC α = oleast β. α < β ` I’m not sure why I used the ASCII implication above rather than the Unicode version, but it does illustrate the way in which the input symbols can be freely mixed. Perhaps as a leap of faith, we believe that UTF8-encoded Unicode will be just as readable as ASCII to the archaeologists of the future. Certainly, in the present day, it’s nice to be able to read and access sources with tools such as less, grep etc. and to see stuff like the above. Michael The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ 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
Apart from one of my own that I found, there are also a number of possibly bad
uses in hoare-package/hoare.ML, such as
fun add_declaration name decl thy =
thy
|> Named_Target.init name
|> Local_Theory.declaration {syntax = false, pervasive = false} decl
|> Local_Theory.exit
|> Proof_Context.theory_of;
I assume this should have the last two lines replaced by
|> Local_Theory.exit_global;
I will certainly test this out.
I see that the Simpl entry in the current AFP still has this code too, and in
the version on SourceForge tagged with Isabelle2014.
Do the regression tests for this package need improving, or are uses such as the
above sometimes alright after all?
Best,
Michael
On 26/08/14 13:12, Michael Norrish wrote:
> I already have the patch you sent me offline in my history.
> I will examine the remaining uses of theory_of and see if they're legitimate.
> Thanks,
> Michael
> On 25/08/14 17:32, Lars Noschinski wrote:
>> 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 mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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] porting code to isabelle2014 and getting "unfinished linear change" errors
I already have the patch you sent me offline in my history. I will examine the remaining uses of theory_of and see if they're legitimate. Thanks, Michael On 25/08/14 17:32, Lars Noschinski wrote: > 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 > 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] porting code to isabelle2014 and getting "unfinished linear change" errors
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") 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? Thanks, Michael 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] Hg sourcetree
This is my experience as well. Michael > On 19 Dec 2013, at 8:23, "Gerwin Klein" wrote: > > I have it installed and it's nice for browsing through history, but for > normal daily operation I still find myself using primarily the command line, > mostly because it's quick and I'm used to it. > > Cheers, > Gerwin > >> On 19 Dec 2013, at 6:26, "Makarius" wrote: >> >> Since I am presently on travel and only briefly looking through pending >> mails, here is a "publicized" version of an ongoing internal discussion: >> on Mac OS X, you may also try this recent high-end application for both Git and Mercurial: https://www.atlassian.com/software/sourcetree/overview >> >> This was highly recommended to me from some people at Edinburgh last spring, >> but I did not find time yet to try it out. >> >> It is particularly relevant to full-time Mac OS X users. >> >> Anyone wants to report on experience with this high-end Mercurial client? >> >> >> 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 The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ 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 not yet a version of the C parser for Isabelle 2013, but there will be soon. Michael On 26/03/2013, at 4:01, Lars Noschinski wrote: > On 25.03.2013 17:21, Makarius wrote: >> On Mon, 11 Mar 2013, Lars Noschinski wrote: >> >>> Indeed and I'm in happy situation that I'm able to share my sources. >>> Unfortunately, due to necessary background theory, this example is quite >>> large and depends on autocorres[1] and hence Isabelle 2012. >>> >>> [1] http://ssrg.nicta.com.au/projects/TS/autocorres/ >> >> Is there a version for Isabelle2013? Note that Isabelle2012 -> >> Isabelle2013 involves unusually few incompatibilities, so the update >> would spare anybody from struggling with old IsaMakefiles again. > > Not that I know of. But maybe David has already ported it? > > -- Lars > ___ > 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] record: fold_congs/unfold_congs
On 18/04/12 1:46 PM, Thomas Sewell wrote: > This is used in our modified version of the Schirmer Hoare VCG. I > suppose that we've released the c-parser sources (which load extra > fold_congs) but not the modified Hoare package (which uses them). The > point is to avoid an exponential time/space explosion when updates of > the form "% rec. rec (| x := rec x + 1 |)" are performed in sequence. > (The problem is the repeated rec.) The modified Hoare package *is* part of our released c-parser. All this will soon (I have the release candidate running already) be available for use on top of isabelle2011-1 (at the moment, the released code only runs on isabelle2009). Michael 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] (Re-)introducing set as a type constructor rather than as mere abbreviation
On 26/08/11 7:26 AM, Florian Haftmann wrote: > Hi Andreas, > >> Let me ask something stupid: >> why exactly do you guys axiomatize 'a set? >> Sure it's admissable and all, but why not do this definitionally >> via the obvious typedef? > > the answer is rather technical: »typedef« in its current implementation > needs set syntax / set type as prerequisite. Of course you could change > »typedef« to be based on predicates, but there is some kind of unspoken > agreement not to set one's hand on that ancient and time-honoured Gordon > HOL primitive. HOL88, hol90, hol98 and HOL4 all have new_type_definition. This principle takes a theorem of the form ?x. P x HOL Light takes a theorem of the form P x (removing the dependency on the existential quantifier). To the best of my knowledge, none of these systems ever used sets in this role. Michael 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] Isabelle release
On 7/01/11 8:05 PM, Alexander Krauss wrote: But then we need a Marketing division to come up with a new name every 8 months :-}. Year numbers are very comfortable. You either come up with a set of names to use, or just do what most software projects do (commercial and open source both), and use numbers. Does the gcc project have this problem? Does Linux? Does emacs? Decide retroactively that everything up until this point was Isabelle 1, and announce the release of Isabelle 2. Or whatever set of numbers floats your boat... Michael ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release
On 7/01/11 7:53 PM, Tobias Nipkow wrote: I don't see any good reason for the skewed naming scheme of 2009-x in 2010 or 2011. We should use the year that the release was made in, period. That avoids unproductie arguments on how major or minor a release is. Or dispense with year numbers entirely. Even Microsoft gave up on that idea for Windows. Michael ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff
On 08/09/10 05:04, Brian Huffman wrote: OK, this makes sense. It is nice to have the pair of lemmas "foo_ext" and "foo_ext_iff" for each function-like type "foo". So do you propose that we rename all of the expand_*_eq lemmas that I listed before? (It would also be good to make sure there is a properly-named *_ext lemma corresponding to each one.) Why not keep both sets of names in play? Michael ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle/HOL axiom ext is redundant
Makarius wrote: > On Thu, 12 Nov 2009, Lucas Dixon wrote: >> this is interesting to me: I don't understand why you couldn't just >> use the --> and ALL of HOL to do exactly what ==> and !! are doing? >> Isn't that what SPL by Zammit did? The dependencies (in Isabelle, >> stored in hyps) can all be recorded outside the logic (as they are in >> SPL). If done correctly, like Isar, the final theorems can be >> re-constructed easily enough from the recorded structure of the proof >> text... or so it seems to me. :) > The hyps are not involved at this point. This is about what I've called > "the visible part of ND reasoning" before. The nice thing of explicitly > outlined ND rules via ==> and !! is that the system knows how to combine > them from their shape. It is not about "two versions" of certain > connectives, but a ND rule calculus that is used together with a fully > featured object-logic. Because, as discussed, the notions correspond in HOL, one could emulate ND by defining new constants equal to the existing object logic implication and universal quantification. One would then prove the ND rules in terms of these. As Makarius said, one would then also have to "reinvent" the implementation of things like resolution over these connectives in order to get that nice uniformity that Isaballe already has. Of course, I also believe that one might emulate this nice uniformity in theorems and reasoning by writing sufficiently clever ML code (which would be parameterised by appropriate theorems, say). When the logic reaches its limits (for example, in the construction of algebraic datatypes we can't express the idea of type existence as a theorem), this is the last recourse that all the HOL systems must stoop to. Michael.
[isabelle-dev] Bug Tracking
Tjark Weber wrote: > But of course a bug tracker is just a tool; in the end its people who > have to work with (or without) it. HOL4's bug tracker (which is > provided by SourceFourge) is not exactly a blazing success either. Indeed. We only really use it for collecting bugs from users who aren't aware of, or refuse to use, the mailing list. My impression is that the tracker provided by S/F was not considered "best of breed", and that the admins there are soon to provide (or already have provided) something better. Michael.
