Re: [isabelle-dev] The coming release of Isabelle2017

[Manuel Eberl]

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

[Lawrence Paulson]

I’ve been using it a bit and it’s pretty useful! Thanks
Larry

> On 9 Jul 2017, at 17:16, Fabian Immler  wrote:
> 
> 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

[Fabian Immler]

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

[Lars Hupel]

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 Paulson  wrote:
>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

[Lawrence Paulson]

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

[Lawrence Paulson]

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, Makarius  wrote:
> 
> 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

[Blanchette, J.C.]

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

[Manuel Eberl]

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 Eberl  wrote:
>>
>> 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

[Lawrence Paulson]

What’s the idea here?
Larry

> On 5 Jul 2017, at 21:09, Manuel Eberl  wrote:
> 
> 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

[Manuel Eberl]

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

[Makarius]

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

Re: [isabelle-dev] The coming release

[Makarius]

Dear all,

this is the last call for small amendments and finalization on the main 
Isabelle repository.


Unless there are any last-minute surprises, the fork for Isabelle2013-1 
will happen Thu 03-Oct-2013.


This means the history of the official release will continue on 
https://bitbucket.org/isabelle_project/isabelle-release while release 
candiates are published on isabelle-users.


Right after the fork, the main Isabelle repository continues its way 
towards subsequent releases, independently of Isabelle2013-1. The release 
fork will be merged back when final release has been published.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release

[Makarius]

On Mon, 2 Sep 2013, Makarius wrote:

The first release candidates of Isabelle2013-1 will probably happen in 
the first or second week of October.


How is the general situation?  And especially the situation for HOL-BNF?

Is it feasible to target the first week of October for Isabelle2013-1-RC1?

This means the usual fork of the main repository to 
https://bitbucket.org/isabelle_project/isabelle-release/ with further 
amendments of important issues only via emailed changesets.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release

[Jasmin Christian Blanchette]

 The first release candidates of Isabelle2013-1 will probably happen in the 
 first or second week of October.
 
 How is the general situation?  And especially the situation for HOL-BNF?

HOL-BNF is a long-term construction yard. There happens to be a lot of 
development these days, but it's coincidental and not motivated by the release. 
Our main goal was to have datatype_new, datatype_new_compat, and 
primrec_new at roughly the same level of functionality as the old package for 
the release, and we've achieved that a few weeks ago already. The manual 
(datatypes.pdf) is in a reasonable shape since last week. That primcorec is 
actually usable and useful since last week is a nice bonus, but the main users 
of this command are currently people who use the release version anyway 
(namely, Andreas, Dmitriy, and Johannes).

As far as HOL-BNF is concerned, you can branch any time. What doesn't make it 
in this release will make it into the next one.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release

[Makarius]

On Tue, 24 Sep 2013, Jasmin Christian Blanchette wrote:

As far as HOL-BNF is concerned, you can branch any time. What doesn't 
make it in this release will make it into the next one.


OK, I will tell you when we are getting close to the fork point.

Just formally for a proper release, you need to make sure that there are 
no spurious tracing and debugging messages left.


BTW, Pretty.item allows to make nice square bullets for itemization 
(visible in Isabelle/jEdit only).



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release

[Jasmin Blanchette]

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 before the fork.

 Just formally for a proper release, you need to make sure that there are no 
 spurious tracing and debugging messages left.

54c8dee1295a should address that.

(Lorenz, you can reintroduce the messages once Makarius has forked. 
Alternatively, you can use a configuration option to control the level of 
output. See e.g. the metis_trace option in 
src/HOL/Tools/Metis/metis_generate.ML for how it's usually done.)

 BTW, Pretty.item allows to make nice square bullets for itemization (visible 
 in Isabelle/jEdit only).

Do you have a specific use in mind w.r.t. BNF or is this just a general hint 
(e.g. for Sledgehammer and Nitpick)?

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release

[Makarius]

On Tue, 24 Sep 2013, Jasmin Blanchette wrote:


54c8dee1295a should address that.

BTW, Pretty.item allows to make nice square bullets for itemization 
(visible in Isabelle/jEdit only).


Do you have a specific use in mind w.r.t. BNF or is this just a general 
hint (e.g. for Sledgehammer and Nitpick)?


Nothing specific.  I've just seen attempts passing by to make some 
indentation and a bullet (actually cdot), to be seen also in the above 
changeset.


Pretty.item has become available several weeks ago, and it comes in handy 
to make Pretty.T list layouts more readable.


I had spent several days to make a black caret that works on all platforms 
and all imaginable fonts, so I just want to share that achievement with 
people who need to compose structured text messages.  (Or maybe get more 
hints when it still does not work as anticipated.)



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release

[Makarius]

The French summer vacation period has ended, so I've switched myself now 
into consolidation mode to put things into shape for release.


The first release candidates of Isabelle2013-1 will probably happen in the 
first or second week of October.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release

[Tobias Nipkow]

The earlier the better because, as I told you at ITP, I have a course starting
in the middle of October and they need to use a new Isabelle, in the worst case
a release candidate.

Tobias

Am 02/09/2013 15:37, schrieb Makarius:
 The French summer vacation period has ended, so I've switched myself now into
 consolidation mode to put things into shape for release.
 
 The first release candidates of Isabelle2013-1 will probably happen in the 
 first
 or second week of October.
 
 
 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] The coming release

[Alexander Krauss]

On 08/17/2013 04:05 PM, Makarius wrote:

in the past few weeks the coming release has been mentioned in passing
several times.  So far the precise schedule is not clear, but just from
the distance to Isabelle2013 and the amount of material that is about to
be finished for Isabelle2013-1, it has to be rather soon after the summer.

Since Isabelle is a huge and complex system, things that are relevant
for a release need to be known well in advance.


There is a small extension to the function package pending, which was 
written by Manuel Eberl. It produces elimination rules of a new format, 
and also provides a fun_cases command for ad-hoc elimination that is 
analogous to inductive_cases.


Since there is some user demand for it and it is already functionally 
complete, I'd like to integrate this when I am back from vacation in two 
weeks, even if there are some minor things to be sorted out.


Alex


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] The coming release

[Florian Haftmann]

 So the time to point out further issues or pending projects is now --
 apart from the well-known HOL-BNF and PIDE improvements that are already
 underway.  In general there is no reason to rush anything on any
 particular release train, since they are rather frequent anyway.  A
 release is a limit point of consolidation -- the really new things
 happen after it.

In my pipeline is some polishing of the code generator preprocessor.

If resources are left then, I would take a look again at the issue of
interpretation prefixes inside the existing HOL theories.

That should be all, though.
Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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] The coming release

[Makarius]

Dear all,

in the past few weeks the coming release has been mentioned in passing 
several times.  So far the precise schedule is not clear, but just from 
the distance to Isabelle2013 and the amount of material that is about to 
be finished for Isabelle2013-1, it has to be rather soon after the summer.


Since Isabelle is a huge and complex system, things that are relevant for 
a release need to be known well in advance.  (Even such seemingly trivial 
reforms like subscripts in identifiers have taken much longer than 
anticipated and are not finished yet.)


So the time to point out further issues or pending projects is now -- 
apart from the well-known HOL-BNF and PIDE improvements that are already 
underway.  In general there is no reason to rush anything on any 
particular release train, since they are rather frequent anyway.  A 
release is a limit point of consolidation -- the really new things happen 
after it.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev