Re: [isabelle-dev] The coming release of Isabelle2017
On 2017-07-05 22:09, Manuel Eberl wrote: > I still want to take care of two really tiny things: […] and the proper > printing > of "nat" values as numerals instead of successor notation. This is now done as of adf3155c57e2. I should note that I was somewhat imprecise, by ‘printing of "nat" values’ I was only referring to what you get when you type "value" etc. Now you won't get a screen full of "Suc" when you do "value (1000 :: nat)", although computing with large "nat" values is still relatively slow, as it uses "Suc" internally. I am no expert on code generation, but I would imagine getting rid of that (e.g. in favour of binary arithmetic, as is done for "int") is probably non-trivial. What do our code generatione experts say? In any case, it's probably not very important; "value" without Code_Target_Numeral is mostly used for small-scale testing and the current solution works fine for that. Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
I’ve been using it a bit and it’s pretty useful! Thanks Larry > On 9 Jul 2017, at 17:16, Fabian Immlerwrote: > > A while ago, Florian Haftmann sent a command that does something like this to > the mailing list [1]. I attach a version that works with current > Isabelle2016-1 (not sure if I got all the modifications right, but it seems > to work at least on the example in the .thy file). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
A while ago, Florian Haftmann sent a command that does something like this to the mailing list [1]. I attach a version that works with current Isabelle2016-1 (not sure if I got all the modifications right, but it seems to work at least on the example in the .thy file). Fabian [1] http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04443.html Explorer.thy Description: Binary data > Am 09.07.2017 um 16:58 schrieb Lawrence Paulson: > > What I’m requesting requires no sophistication at all. It is merely to > automate what we currently do by copying from one window and pasting to > another, while inserting “fix”, “assume” and “show” in the obvious places. > Larry > >> On 9 Jul 2017, at 16:32, Lars Hupel wrote: >> >> I currently supervise a student who's investigating proof refactoring. One >> possible outcome of this would be a tool that also does what you suggested. >> It's a little too early to tell, though. > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME cryptographic signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
I currently supervise a student who's investigating proof refactoring. One possible outcome of this would be a tool that also does what you suggested. It's a little too early to tell, though. Cheers Lars On 8 July 2017 23:28:42 CEST, Lawrence Paulsonwrote: >No, that’s precisely what I’d like to avoid. I prefer texts that you >can actually read. It would be great to have something automatically >generated, even if it needed manual tweaking (e.g. to rename >variables). > >And I’ve gone to some effort purging instances of “guess” from existing >proofs. > >Larry > >> On 8 Jul 2017, at 22:16, Peter Lammich wrote: >> >> We already have proof goal_cases. Is that what you mean? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
No, that’s precisely what I’d like to avoid. I prefer texts that you can actually read. It would be great to have something automatically generated, even if it needed manual tweaking (e.g. to rename variables). And I’ve gone to some effort purging instances of “guess” from existing proofs. Larry > On 8 Jul 2017, at 22:16, Peter Lammichwrote: > > We already have proof goal_cases. Is that what you mean? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
I am always using the new auto-complete facility for proof (cases “...”) and for induction. But could this be done for “proof" with any method, simply copying out the states of the subgoals? Then people would make a lot less use of “subgoals”, etc. Larry > On 5 Jul 2017, at 21:04, Makariuswrote: > > Is there anything else to take into account for this late-summer release > process? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
Hi Makarius, > Is there anything else to take into account for this late-summer release > process? Simon Cruanes (cc:) and I are still working on Nunchaku, which we intend to become Nitpick's successor. I have some patches locally that move the current "Nunchaku.thy" to Main (it's not much code and doesn't slow up building Main noticeably), but we're also working on the "nunchaku" component itself, which we will repack and update. We'll also add an "smbc" component, for another OCaml tool also developed by Simon Cruanes [*], which provides a "SAT solver + narrowing" backend to the "nunchaku" tool. I will also update the "Nitpick_Examples" to also perform regression tests on Nunchaku. I'm aiming at doing all the necessary changes by the end of August at the latest. Jasmin [*] https://cedeela.fr/~simon/files/cade_17_paper.pdf ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
Nothing fancy, just a couple of code_post rules to rewrite successor notation into numeral notation after evaluation and before printing. I don't know if there's a better way to do that, but I think we discussed this on the mailing list a while ago and came to the conclusion that code_post is indeed the way to go. Of course, I am always open to better solutions, perhaps avoiding the successor notation entirely, but I don't know the code generator well enough to say if this is possible (or where the successor stuff comes from in the first place) In any case, I would argue that even those code_post rules to rewrite successor notation to numerals is a lot better than what we have at the moment. Manuel On 2017-07-05 21:45, Lawrence Paulson wrote: > What’s the idea here? > Larry > >> On 5 Jul 2017, at 21:09, Manuel Eberlwrote: >> >> the proper printing of "nat" values as numerals instead of successor >> notation. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
What’s the idea here? Larry > On 5 Jul 2017, at 21:09, Manuel Eberlwrote: > > the proper printing of "nat" values as numerals instead of successor notation. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] The coming release of Isabelle2017
I still want to take care of two really tiny things: the "subseq" situation and the proper printing of "nat" values as numerals instead of successor notation. Just mentioning that for the sake of completeness. Manuel On 2017-07-05 21:04, Makarius wrote: > Dear all, > > we are now almost 7 months after Isabelle2016-1 (December 2016). > Following the standard schedule, the Isabelle2017 release should appear > at the start of October 2017. > > During the last 3 weeks in July, I will be in Cambridge. That is also a > possibility to show me old and new problems in my areas of > responsibility. Afterwards, I want to finish the reform of > session-qualified theory names, and put Isabelle/VSCode into shape for > its 1.0 release. > > > Is there anything else to take into account for this late-summer release > process? > > It is important to recall that the deadline for significant changes is > actually 6 weeks before the final lift-off, i.e. at the point where the > fork of isabelle-dev and isabelle-release repositories happens. > > > 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] The coming release of Isabelle2017
Dear all, we are now almost 7 months after Isabelle2016-1 (December 2016). Following the standard schedule, the Isabelle2017 release should appear at the start of October 2017. During the last 3 weeks in July, I will be in Cambridge. That is also a possibility to show me old and new problems in my areas of responsibility. Afterwards, I want to finish the reform of session-qualified theory names, and put Isabelle/VSCode into shape for its 1.0 release. Is there anything else to take into account for this late-summer release process? It is important to recall that the deadline for significant changes is actually 6 weeks before the final lift-off, i.e. at the point where the fork of isabelle-dev and isabelle-release repositories happens. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev