date:20120417

On 04/18/2012 03:42 PM, Lawrence Paulson wrote:

How do you do “show me", “commands", “find theorem", “settings", etc? I believe
you're supposed to remember commands for all of those items and type them explicitly. That's not
what a user interface is supposed to do.
Actually I did never use these in emacs either... but I see your point
(which is of course valid).

A further problem is you cannot cut and paste between the “proof" window and
the main window, so good luck creating any structured proofs (unless you love typing
lots of formal text and never make mistakes). And on a Mac, the keyboard shortcuts
are different from the usual.
I don't get it. Copying and pasting between the output buffer and the
main buffer works just fine for me (a bit odd is that you have to use
Ctrl+C and Ctrl+V, since the linux-typical marking with mouse and middle
click does not work (yet (?))). But maybe this is different in Mac OS.

cheers

chris

Larry

On 18 Apr 2012, at 02:53, Christian Sternagel wrote:

Just for the record: I exclusively use jEdit for several weeks now and did
quite a lot of actual proofs. My personal opinion: the user experience is much
nicer than with emacs

* I did not have any complete hangs yet (as with emacs)
* the whole appearance is much nicer (remember, this is my personal
opinion): font, highlighting, ...
* not to forget the browsability (from constants to their
definitions; from ML functions to their modules)
* checking a single theory (in non-batch mode) is MUCH faster than
with emacs

I would not for the world go back to emacs. (Maybe I should mention that before Isabelle
I did not use emacs at all, so it was quite annoying to have to learn an "operating
system" when I just needed an editor ;)).

cheers

chris

On 04/18/2012 01:08 AM, Lawrence Paulson wrote:

I certainly care about it. Jedit is great for browsing existing theory
developments, but there is no support for actually doing proofs.
Larry

On 17 Apr 2012, at 16:56, Makarius wrote:

Anyway, who is maintaining Isabelle ProofGeneral now? The repository version
does not work with Emacs 23 for several months already. It seems that nobody
cares about it anymore.

For the release, I will package up official ProofGeneral-4.1 as last time. It
is then up to its users to test it and report problems in the usual testing
stage before the release.

___
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

2012-04-17 Thread Michael Norrish

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] record: fold_congs/unfold_congs

2012-04-17 Thread Thomas Sewell

The fold_congs theorems are not an accident. They are used as congruence 
rules to perform conversions such as
"rec (| x := rec x + 1 |) = x_update (%x. x + 1) rec". Note this removes 
the duplicated mention of the name rec.


The name fold_congs is somewhat arbitrary, since either direction above 
could be argued to be "folding".


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 fold_congs can be provided manually to the simplifier if anyone 
knows to do so. I am probably the only person in the world who knows 
when to do so. This is usually done to equate the two forms given above, 
either of which may be the result of other simplification. There are 88 
uses of fold_congs in the L4.verified proofs at this time.


The unfold_congs are meant to perform the reverse substitution, but the 
simplifier doesn't reliably play along. There are 5 uses in the 
L4.verified proofs at this time, and I suspect they can be easily removed.


Yours,
Thomas.

On 18/04/12 00:37, Makarius wrote:

This is probably mainly relevant to NICTA users of the record package.

When doing some cleanup and performance tuning of the record package, I
discovered the following mysterious fold_congs and unfold_congs:
http://isabelle.in.tum.de/repos/isabelle/file/d52da3e7aa4c/src/HOL/Tools/record.ML#l334

They appear to go back to the initial NICTA contribution 50406c4951d9. I
have also seen traces of that feature in the L4.verified C parser tool
that became publicly available recently.

Do these fold_congs/unfold_congs still have any purpose?  In the reachable
set of Isabelle and AFP applications they don't, as far as I can see.  So
it looks like a candidate for garbage collection on the sources.


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


Dear Makarius,

it's very nice that after sledgehammer found a proof command to finish a 
proof, I can simply click on this command in the output buffer to 
include it in the main buffer! A slight oddity is that this merges 
lines. E.g.,


  lemma "⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys"
  sledgehammer
  end

After sledgehammer reports

  "remote_e": Try this: by (metis append_eq_conv_conj) (21 ms).

In the output buffer. I click on "by (metis append_eq_conv_conj)" and 
the result is.


  lemma "⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys"
  by (metis append_eq_conv_conj)end

Maybe this could be changed such that "end" stays on its own line?

cheers

chris


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

Re: [isabelle-dev] <-> and <-->

+1 for <--> (since it would agree, as Tobias pointed out, with the 
established =>, ==>, ->, -->).


Concerning convenience of input and automatic replacement:

I would not use automatic replacement at all, since it is at least as 
often a problem as it is of help (e.g., ML code inside theories "=>" in 
case statements, the mentioned "~~/" for imports, and I am sure that 
there are many other examples [LaTeX inside @text blocks]).


Still it is very convenient if one can just type and does not have to 
click (or browse with the keyboard) any popups.


In jEdit you can do the following (see also 
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-November/msg00089.html 
):


Under "Plugins -> Plugin Options -> Sidekick -> General" set "Show 
completion popups where possible" and "Automatic completion popups get 
focus" and use "\n" as "Accept character for completion popup" and "" 
(the empty string) as "Accept characters to insert after completion".


The resulting behavior is as follows:
If you type faster than indicated by the "After popup trigger keystroke, 
wait (seconds)" option the text stays just as you type it (of course you 
can set this option such that the popup always appears).
Otherwise, the popup appears as soon as you have completed a symbol that 
can be replaced, e.g., "=>", and have waited long enough. If you want to 
replace the ASCII input by the first symbol (usually the one you want) 
you just have to type , if you want to stay with the ASCII 
variant just go along by typing either space (if the line still 
continues this is the natural thing to do) or pressing  once.


This means that you just have to press 1 additional key (i.e., ) 
when you want replacement and just keep on typing as usual otherwise (of 
course, you could as well reverse this behavior, as you prefer).


I found this setup rather convenient.

cheers

chris


On 04/18/2012 02:51 AM, Makarius wrote:

On Tue, 17 Apr 2012, Alexander Krauss wrote:


On 04/17/2012 05:41 PM, Tobias Nipkow wrote:

This is what I would call unwieldy: instead of typing<--> or<-> (and
having them converted to the appropriate symbols) you always type<->,
but then you have to select from a menue. I don't see the progress.


Could not agree more. These arrows are very common, and I want to be
able to type them without menu interaction. The selection idea is the
equivalent of "instead of having to use the shift key, you simply type
the letter and then select from the menu whether you want the capital
or the small letter".

Of course we should not forget that the eager replacement done by
PG/Emacs is also problematic: try to type ~~/src and see how many
keystrokes you need :-)


We all know these bad jokes of both Emacs and jEdit. But the general
problem of mathematical input has been studied by other people before --
I often see snippets of that at the CICM conference. Even just for plain
JVM-based IDE-style editing there are better solutions than the Sidekick
popup that I am still using in Isabelle/jEdit (which was easy to set up
in 30min).

Anybody who feels like contributing constructively, should do a survey
of the possibilities on the JVM platform and propose an suitable
improvement of the Isabelle/jEdit completion mechanism. Ideally with a
little Scala implementation.


Concerning the situation in Isabelle/ProofGeneral right now: it is
unmaintained so nothing can move there for this release.


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] <-> and <-->

Just for the record: I exclusively use jEdit for several weeks now and 
did quite a lot of actual proofs. My personal opinion: the user 
experience is much nicer than with emacs


* I did not have any complete hangs yet (as with emacs)
* the whole appearance is much nicer (remember, this is my personal
opinion): font, highlighting, ...
* not to forget the browsability (from constants to their
definitions; from ML functions to their modules)
* checking a single theory (in non-batch mode) is MUCH faster than
with emacs

I would not for the world go back to emacs. (Maybe I should mention that 
before Isabelle I did not use emacs at all, so it was quite annoying to 
have to learn an "operating system" when I just needed an editor ;)).


cheers

chris

On 04/18/2012 01:08 AM, Lawrence Paulson wrote:

I certainly care about it. Jedit is great for browsing existing theory 
developments, but there is no support for actually doing proofs.
Larry

On 17 Apr 2012, at 16:56, Makarius wrote:



Anyway, who is maintaining Isabelle ProofGeneral now?  The repository version 
does not work with Emacs 23 for several months already.  It seems that nobody 
cares about it anymore.

For the release, I will package up official ProofGeneral-4.1 as last time. It 
is then up to its users to test it and report problems in the usual testing 
stage before the release.



___
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] Relations vs. Predicates


Sorry for the inconveniences.

On 04/17/2012 11:55 PM, Makarius wrote:

Here is another follow-up to the relcomp story so far:

changeset: 47508:85c6268b4071
tag: tip
user: wenzelm
date: Tue Apr 17 16:48:37 2012 +0200
files: doc-src/TutorialI/Sets/Relations.thy
description:
updated rel_comp ~> relcomp (cf. e1b761c216ac);

doc-src/TutorialI/Sets/Relations.thy


This is only to make the manual compile again.
This one didn't show up during 'isabelle makeall all'. Shouldn't 
documentation be part of "all"? I guess then that a test should also 
include "./Admin/build doc"? Anything else besides


  isabelle makeall all
  ./Admin/build doc

to test a changeset (apart from external dependencies like the AFP)?


I hope it is not one of
the theories that need generated latex copied to another place by hand.

Just out of curiosity: what do you mean by the above statement?


Moreover NEWS in that version has oddities like this:

rel_comp_def ~> rel_comp_unfold

and later

rel_comp_unfold ~> relcomp_unfold


In the time immediately before the relase (which is now) the NEWS should
reflect the perspective for end-users of the official stable system that
is delivered.
I observed this oddities but left them deliberately since I was not 
aware of the above convention (which is of course very sensible).


cheers

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

Re: [isabelle-dev] Towards the next release

2012-04-17 Thread Gerwin Klein

On 18/04/2012, at 12:29 AM, Makarius wrote:

> On Tue, 17 Apr 2012, Gerwin Klein wrote:
> 
>> - I would like to add a size limit to records beyond which no code generator 
>> setup is performed. The main reason is that on sizes > 200 fields or so, the 
>> setup does not make any sense, but consumes very large amounts of memory 
>> (and time). Switching it off gets rid of almost all of the mysterious memory 
>> blowup that we had and enables us to run our proofs within 4GB on Linux 
>> (32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal, 
>> but I don't see a better workaround, because the code generator setup *is* 
>> useful for small records. There is a question on how to implement the limit:
> 
>> 1) as an option available the user at record definition time
>> 2) as an option/flag to the internal record definition function only
>> 3) as a configuration option
>> 4) as a compile time constant
>> 
>> I'm currently in favour of 4, because the limit is very specialised and will 
>> only really occur for records that are somehow automatically generated in 
>> which case the code generator setup is very unlikely to make sense. Options 
>> 1 and 3 would require adding syntax/configuration names which is not really 
>> worth it. Option 2 threads yet another obscure parameter through a rather 
>> large package.
> 
> If 3) means "configuration option" in the sense of Config.T, here is the 
> canonical 1-liner to make one for a package:
> 
>  val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 
> 9);

Yes, that's what I meant. It's easy to set up, but pollutes the config name 
space a little more for users. Of course it also means that it can be changed 
at runtime. If there is a slight preference for this, I'm happy to go that road.


> Concerning performance issues in general, I've recently made a lot of 
> measurements.  It seems indeed that the code generator is responsible for 
> quite a bit of it, although I did not look any further into its depths. 
> Instead I've made some performance tuning for the critical infrastructure for 
> localizing big packages with big application.

Yes, this looks very promising. After the record package/code generator find 
we're now almost done updating things to Isabelle2011-1. Just in time for 
Isabelle2012 ;-)


> Moreover, David Matthews is right now reforming the Poly/ML runtime system, 
> such that we might see an improvement of an order of magnitude soon. 

We'll be very keen on that one, too.

Cheers,
Gerwin

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

Re: [isabelle-dev] Future of ProofGeneral


On Tue, 17 Apr 2012, Lawrence Paulson wrote:

I didn't intend to be tactless or demanding, but at least something 
analogous to the “Isabelle" menu (offering access to show 
me/commands/prover settings) is needed. Unless it's there somewhere and 
I overlooked it.


No it is one of the known things that are still not there yet, and are 
officially specified as a feature in the README:


  General lack of various conveniences known from Proof General.


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

Re: [isabelle-dev] Future of ProofGeneral

Sorry, I didn't intend to be tactless or demanding, but at least something 
analogous to the “Isabelle" menu (offering access to show me/commands/prover 
settings) is needed. Unless it's there somewhere and I overlooked it.
Larry

On 17 Apr 2012, at 17:18, Makarius wrote:

> On Tue, 17 Apr 2012, Lawrence Paulson wrote:
> 
>> I certainly care about it. Jedit is great for browsing existing theory 
>> developments, but there is no support for actually doing proofs.
> 
> As I've said already 4 years ago, the double burden to keep ProofGeneral 
> alive and make Isabelle/jEdit a full replacement (and more) slows things down 
> considerably.
> 
> After long struggles, the Isabelle2011-1 version of Isabelle/jEdit is defined 
> as first stable release, with many things still missing, but it can be used 
> for many more things than just browsing.
> 
> The situation is improving further for the coming release, but I am still 
> encumbered by ProofGeneral Emacs, since nobody has ever stepped forward to 
> take over the responsibility for 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

Re: [isabelle-dev] <-> and <-->


On Tue, 17 Apr 2012, Alexander Krauss wrote:


On 04/17/2012 05:41 PM, Tobias Nipkow wrote:
This is what I would call unwieldy: instead of typing<--> or<-> (and 
having them converted to the appropriate symbols) you always type<->, 
but then you have to select from a menue. I don't see the progress.


Could not agree more. These arrows are very common, and I want to be 
able to type them without menu interaction. The selection idea is the 
equivalent of "instead of having to use the shift key, you simply type 
the letter and then select from the menu whether you want the capital or 
the small letter".


Of course we should not forget that the eager replacement done by 
PG/Emacs is also problematic: try to type ~~/src and see how many 
keystrokes you need :-)


We all know these bad jokes of both Emacs and jEdit.  But the general 
problem of mathematical input has been studied by other people before -- I 
often see snippets of that at the CICM conference.  Even just for plain 
JVM-based IDE-style editing there are better solutions than the Sidekick 
popup that I am still using in Isabelle/jEdit (which was easy to set up in 
30min).


Anybody who feels like contributing constructively, should do a survey of 
the possibilities on the JVM platform and propose an suitable improvement 
of the Isabelle/jEdit completion mechanism.  Ideally with a little Scala 
implementation.



Concerning the situation in Isabelle/ProofGeneral right now: it is 
unmaintained so nothing can move there for this release.



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

Re: [isabelle-dev] Future of ProofGeneral


On Tue, 17 Apr 2012, Peter Lammich wrote:

Anyway, who is maintaining Isabelle ProofGeneral now?  The repository 
version does not work with Emacs 23 for several months already.  It 
seems that nobody cares about it anymore.


For the release, I will package up official ProofGeneral-4.1 as last 
time. It is then up to its users to test it and report problems in the 
usual testing stage before the release.


I guess most of the PG users work on the release version, and would be 
quite annoyed if the next release contains a buggy PG.


(I've switched the thread of this, because the Future of ProofGeneral is a 
serious issue in its own right.)


The plan for the comining release (which will happen within a couple of 
weeks) is to keep the status-quo of Isabelle2011-1.  This means 
ProofGeneral will be not more buggy than everybody is used to anyway. 
Today I've made some quick tests with Emacs on Mac OS X already, and it 
looks not worse than last fall.


In the longer run, the proponents of ProofGeneral need to find a solution 
for themselves, and organize a maintenance scheme -- I have pointed this 
out several times before.  BTW, there is quite a lot of recent activity on 
the ProofGeneral CVS, so it is not quite dead yet.



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

Re: [isabelle-dev] <-> and <-->

2012-04-17 Thread Alexander Krauss


On 04/17/2012 05:41 PM, Tobias Nipkow wrote:

This is what I would call unwieldy: instead of typing<-->  or<->  (and having
them converted to the appropriate symbols) you always type<->, but then you
have to select from a menue. I don't see the progress.


Could not agree more. These arrows are very common, and I want to be 
able to type them without menu interaction. The selection idea is the 
equivalent of "instead of having to use the shift key, you simply type 
the letter and then select from the menu whether you want the capital or 
the small letter".


Of course we should not forget that the eager replacement done by 
PG/Emacs is also problematic: try to type ~~/src and see how many 
keystrokes you need :-)


Maybe the "Isabelle Keyboard" from 2008 needs a revival in jEdit: It has 
an extra modifier key (a modded Windows key) which opens up a whole 
range of characters. But this is probably hard to do cross-platform.


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

Re: [isabelle-dev] <-> and <-->

Am 17/04/2012 17:56, schrieb Makarius:
> Why then the proposal to change the prover syntax?

What I meant was not just the prover syntax but also the input syntax. In fact,
primarily the input syntax. One could change merely the latter (which is what PG
does), but that introduces an inconsistency: if you type <--> and allow the
editor to change it to \, you are fine, but if you leave it
in ASCII, it yields a parser error. That is not so nice.

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

Re: [isabelle-dev] <-> and <-->

2012-04-17 Thread Peter Lammich

> Anyway, who is maintaining Isabelle ProofGeneral now?  The repository 
> version does not work with Emacs 23 for several months already.  It seems 
> that nobody cares about it anymore.
> 
> For the release, I will package up official ProofGeneral-4.1 as last time. 
> It is then up to its users to test it and report problems in the usual 
> testing stage before the release.


I guess most of the PG users work on the release version, and would be
quite annoyed if the next release contains a buggy PG.

Peter



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

Re: [isabelle-dev] <-> and <-->

2012-04-17 Thread Peter Lammich


> Anyway, who is maintaining Isabelle ProofGeneral now?  The repository 
> version does not work with Emacs 23 for several months already.  It seems 
> that nobody cares about it anymore.
> 
> For the release, I will package up official ProofGeneral-4.1 as last time. 
> It is then up to its users to test it and report problems in the usual 
> testing stage before the release.


I guess most of the PG users work on the release version, and would be
quite annoyed if the next release contains a buggy PG.


Peter


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

[isabelle-dev] Future of ProofGeneral


On Tue, 17 Apr 2012, Lawrence Paulson wrote:

I certainly care about it. Jedit is great for browsing existing theory 
developments, but there is no support for actually doing proofs.


As I've said already 4 years ago, the double burden to keep ProofGeneral 
alive and make Isabelle/jEdit a full replacement (and more) slows things 
down considerably.


After long struggles, the Isabelle2011-1 version of Isabelle/jEdit is 
defined as first stable release, with many things still missing, but it 
can be used for many more things than just browsing.


The situation is improving further for the coming release, but I am still 
encumbered by ProofGeneral Emacs, since nobody has ever stepped forward to 
take over the responsibility for it.



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

Re: [isabelle-dev] <-> and <-->

I certainly care about it. Jedit is great for browsing existing theory 
developments, but there is no support for actually doing proofs.
Larry

On 17 Apr 2012, at 16:56, Makarius wrote:

> 
> Anyway, who is maintaining Isabelle ProofGeneral now?  The repository version 
> does not work with Emacs 23 for several months already.  It seems that nobody 
> cares about it anymore.
> 
> For the release, I will package up official ProofGeneral-4.1 as last time. It 
> is then up to its users to test it and report problems in the usual testing 
> stage before the release.
> 

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

Re: [isabelle-dev] <-> and <-->


On Tue, 17 Apr 2012, Tobias Nipkow wrote:


Am 17/04/2012 16:27, schrieb Lawrence Paulson:

I think you are right that ASCII syntax is almost completely irrelevant now. 
Hardly anybody sees it.


It is relevant as an input method, and that is exactly what my 
suggestion is about. I am not interested in ASCII art but in a smooth 
input method. When I type, I would prefer to keep on typing.


Why then the proposal to change the prover syntax?

Anyway, who is maintaining Isabelle ProofGeneral now?  The repository 
version does not work with Emacs 23 for several months already.  It seems 
that nobody cares about it anymore.


For the release, I will package up official ProofGeneral-4.1 as last time. 
It is then up to its users to test it and report problems in the usual 
testing stage before the release.



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

Re: [isabelle-dev] <-> and <-->

Am 17/04/2012 16:27, schrieb Lawrence Paulson:
> I think you are right that ASCII syntax is almost completely irrelevant now. 
> Hardly anybody sees it.

It is relevant as an input method, and that is exactly what my suggestion is
about. I am not interested in ASCII art but in a smooth input method. When I
type, I would prefer to keep on typing.

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

Re: [isabelle-dev] <-> and <-->

Am 17/04/2012 16:13, schrieb Makarius:
> On Tue, 17 Apr 2012, Tobias Nipkow wrote:
>> and would also leave room for an ASCII syntax for \ (namely 
>> <->).
> 
> Using <--> for <-> and making room for another <-> would also mean that the 
> user
> has to type/read the longer unwieldy sequence by default.

Calling "--" as opposed to "-" unwieldy is a bit of a joke. And provided the
editor supports the conversion to proper symbols nicely, it is merely a question
of typing, not reading.

> Anyway, what is the role of the ASCII replacement syntax today?  We use it 
> both
> for prover syntax and input methods of the editor, which I always find 
> difficult
> to explain to new users.

I have not experienced those difficulties.

> In practice the alternative ASCII input is mainly
> passed to the prover because the editor completion mechanisms are still 
> require
> an effort to change focus and press extra keys.

Not in ProofGeneral. I type -->  and it becomes \.

> A really smooth input method in the editor could overcome the need for ASCII
> replacement syntax altogether. Such input method could also admit multiple
> associations, e.g the user typing short <-> would get a selection of arrows to
> be inserted into the text.

This is what I would call unwieldy: instead of typing <--> or <-> (and having
them converted to the appropriate symbols) you always type <->, but then you
have to select from a menue. I don't see the progress.

> I have seen pretty good mathematical input methods somewhere before, maybe in
> TeXmacs, maybe in some computer-algebra system.

I checked out TeXmacs and, surprise, surprise, when you type <-> it is converted
into \leftrightarrow, and when you type <--> it becomes \longleftrightarrow.

Tobias

> This would mean a conceptual
> advance, not just a variation of old conventions.  I.e. we could overcome
> alternative syntax tables eventually.
> 
> 
> 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] Relations vs. Predicates


Here is another follow-up to the relcomp story so far:

changeset:   47508:85c6268b4071
tag: tip
user:wenzelm
date:Tue Apr 17 16:48:37 2012 +0200
files:   doc-src/TutorialI/Sets/Relations.thy
description:
updated rel_comp ~> relcomp (cf. e1b761c216ac);

doc-src/TutorialI/Sets/Relations.thy


This is only to make the manual compile again.  I hope it is not one of 
the theories that need generated latex copied to another place by hand.



Moreover NEWS in that version has oddities like this:

  rel_comp_def ~> rel_comp_unfold

and later

  rel_comp_unfold ~> relcomp_unfold


In the time immediately before the relase (which is now) the NEWS should 
reflect the perspective for end-users of the official stable system that 
is delivered.



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

[isabelle-dev] record: fold_congs/unfold_congs


This is probably mainly relevant to NICTA users of the record package.

When doing some cleanup and performance tuning of the record package, I 
discovered the following mysterious fold_congs and unfold_congs: 
http://isabelle.in.tum.de/repos/isabelle/file/d52da3e7aa4c/src/HOL/Tools/record.ML#l334


They appear to go back to the initial NICTA contribution 50406c4951d9. I 
have also seen traces of that feature in the L4.verified C parser tool 
that became publicly available recently.


Do these fold_congs/unfold_congs still have any purpose?  In the reachable 
set of Isabelle and AFP applications they don't, as far as I can see.  So 
it looks like a candidate for garbage collection on the sources.



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

Re: [isabelle-dev] Towards the next release


On Tue, 17 Apr 2012, Gerwin Klein wrote:

- I would like to add a size limit to records beyond which no code 
generator setup is performed. The main reason is that on sizes > 200 
fields or so, the setup does not make any sense, but consumes very large 
amounts of memory (and time). Switching it off gets rid of almost all of 
the mysterious memory blowup that we had and enables us to run our 
proofs within 4GB on Linux (32bit) and ~8GB on Darwin (64bit). Having 
limits like these is not ideal, but I don't see a better workaround, 
because the code generator setup *is* useful for small records. There is 
a question on how to implement the limit:



1) as an option available the user at record definition time
2) as an option/flag to the internal record definition function only
3) as a configuration option
4) as a compile time constant

I'm currently in favour of 4, because the limit is very specialised and 
will only really occur for records that are somehow automatically 
generated in which case the code generator setup is very unlikely to 
make sense. Options 1 and 3 would require adding syntax/configuration 
names which is not really worth it. Option 2 threads yet another obscure 
parameter through a rather large package.


If 3) means "configuration option" in the sense of Config.T, here is the 
canonical 1-liner to make one for a package:


  val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 
9);

You then merely export that in the signature, and use it with Config.get 
in the package implementation, on the context that is already there 
anyway. (For non-localized packages Config.get_global approximates that.)



Concerning performance issues in general, I've recently made a lot of 
measurements.  It seems indeed that the code generator is responsible for 
quite a bit of it, although I did not look any further into its depths. 
Instead I've made some performance tuning for the critical infrastructure 
for localizing big packages with big application.


Moreover, David Matthews is right now reforming the Poly/ML runtime 
system, such that we might see an improvement of an order of magnitude 
soon.  Maybe even a renaissance of 32bit mode for reasonable big 
applications -- if this works for the infamous JinjaThreads is still to be 
seen (right now it cannot be tested because it is still broken in 
AFP/8469825f5d1b).



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

Re: [isabelle-dev] <-> and <-->

As regards motivation, remember, back then it was a thing of beauty. I could 
easily remember the day when it was possible to use lowercase letters.

I think you are right that ASCII syntax is almost completely irrelevant now. 
Hardly anybody sees it. Even on my MacBook where the Unicode characters are off 
by one (I wish I could fix this), I have been using symbolic identifiers 
because I know that my main work will be done on machines without that bug.

Larry

On 17 Apr 2012, at 15:13, Makarius wrote:

> A brief look at the history and source archive shows that this ASCII art has 
> already been there since Isabelle86. Larry might still remember his 
> motivations in the depths of time.  I've always understood <-> as "visually 
> appropriate" counterpart of --> in the sense of the physical length, despite 
> the optical distortion since ASCII < > are not proper arrow heads.

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

Re: [isabelle-dev] <-> and <-->


On Tue, 17 Apr 2012, Tobias Nipkow wrote:

In HOL, the ASCII syntax for \ is defined to be <-> 
but visually <--> would be more appropriate, closer to -->


A brief look at the history and source archive shows that this ASCII art 
has already been there since Isabelle86. Larry might still remember his 
motivations in the depths of time.  I've always understood <-> as 
"visually appropriate" counterpart of --> in the sense of the physical 
length, despite the optical distortion since ASCII < > are not proper 
arrow heads.


Our default symbol mapping then associates long arrows of the same length 
accordingly, this time without optical distortions due to good quality 
IsabelleText or STIX fonts.



and would also leave room for an ASCII syntax for \ 
(namely <->).


Using <--> for <-> and making room for another <-> would also mean that 
the user has to type/read the longer unwieldy sequence by default.



Anyway, what is the role of the ASCII replacement syntax today?  We use it 
both for prover syntax and input methods of the editor, which I always 
find difficult to explain to new users.  In practice the alternative ASCII 
input is mainly passed to the prover because the editor completion 
mechanisms are still require an effort to change focus and press extra 
keys.


A really smooth input method in the editor could overcome the need for 
ASCII replacement syntax altogether.  Such input method could also admit 
multiple associations, e.g the user typing short <-> would get a selection 
of arrows to be inserted into the text.  (I used to have this in 
etc/symbols until some NICTA guys asked to make it unique again, to 
accomodate WWW_Find.)


I have seen pretty good mathematical input methods somewhere before, maybe 
in TeXmacs, maybe in some computer-algebra system.  This would mean a 
conceptual advance, not just a variation of old conventions.  I.e. we 
could overcome alternative syntax tables eventually.



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

Re: [isabelle-dev] NEWS: auxiliary contexts


On Tue, 17 Apr 2012, Lawrence Paulson wrote:

I look forward to seeing some documentation on these increasingly 
mysterious constructs… :-)


It is pretty close to the original concept of "section" that you've 
introduced with Florian Kammüller in 1998/1999, so it is much more basic 
than locales + locale interpretation.


The Isabelle/a83b25e5bad3 changeset of the announcement also covers the 
documentation in the isar-ref manual.  It is quite compact, but that is it 
for now.  For the user it is mainly a new presentation of long established 
concepts anyway.



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

Re: [isabelle-dev] IH in induction-wrapper

Well this was just a stripped-down version of my real proof, in which 
the term seems to be necessary. Here is a less stripped-down version.


notepad
begin
   fix  P :: "bool" and Q :: "(nat ⇒ 'a set) ⇒ bool"
   fix f :: "nat =>  'a set" and n :: nat
   assume "finite (f n)" and "Q f"
   hence "P"
   proof (induction "f n" arbitrary: f rule: finite_psubset_induct)
 case (psubset g)
 thm psubset.IH (* this fact does not exist *)
 show ?case sorry
   qed
end

If I drop the "f n", then in the fact psubset I have

  ?B ⊂ g ⟹ Q ?f ⟹ P (i.e., ?B and ?f are not related)


Otherwise I have

  ?f n ⊂ g n ⟹ Q ?f ⟹ P

cheers

chris

On 04/17/2012 04:44 PM, Tobias Nipkow wrote:

Revised answer.

I was a bit surprised that it did not work and tried to get to the bottom of it
with some tracing, but everything seemed to be fine. Then I realised that your
inductions are overkill: your inductions are over a predicate, you do not need
to give a variable or term as well. If you drop "f 0" below, everything works 
fine.

Best regards
Tobias

Am 17/04/2012 07:26, schrieb Christian Sternagel:

Hi all,

I think the possibility to refer to the induction hypothesis via, e.g., Suc.IH
(for natural numbers) is a nice feature offered by the "induction"-wrapper
around "induct". I was wondering if there is an inherent problem in the
following example, or if the "induction"-wrapper could be adapted to deal with 
it?

notepad
begin
   fix A :: "'a set" and P :: "bool"
   assume "finite A"
   hence "P"
   proof (induction A rule: finite_psubset_induct)
 case (psubset B)
 thm psubset.IH (* as expected *)
 show ?case sorry
   qed
   fix f :: "nat =>  'a set"
   assume "finite (f 0)"
   hence "P"
   proof (induction "f 0" arbitrary: f rule: finite_psubset_induct)
 case (psubset g)
 thm psubset.IH (* this fact does not exist *)
 show ?case sorry
   qed
end

cheers

chris
___
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 mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] IH in induction-wrapper

Revised answer.

I was a bit surprised that it did not work and tried to get to the bottom of it
with some tracing, but everything seemed to be fine. Then I realised that your
inductions are overkill: your inductions are over a predicate, you do not need
to give a variable or term as well. If you drop "f 0" below, everything works 
fine.

Best regards
Tobias

Am 17/04/2012 07:26, schrieb Christian Sternagel:
> Hi all,
> 
> I think the possibility to refer to the induction hypothesis via, e.g., Suc.IH
> (for natural numbers) is a nice feature offered by the "induction"-wrapper
> around "induct". I was wondering if there is an inherent problem in the
> following example, or if the "induction"-wrapper could be adapted to deal 
> with it?
> 
> notepad
> begin
>   fix A :: "'a set" and P :: "bool"
>   assume "finite A"
>   hence "P"
>   proof (induction A rule: finite_psubset_induct)
> case (psubset B)
> thm psubset.IH (* as expected *)
> show ?case sorry
>   qed
>   fix f :: "nat => 'a set"
>   assume "finite (f 0)"
>   hence "P"
>   proof (induction "f 0" arbitrary: f rule: finite_psubset_induct)
> case (psubset g)
> thm psubset.IH (* this fact does not exist *)
> show ?case sorry
>   qed
> end
> 
> cheers
> 
> chris
> ___
> 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] Publishing contributions as an external

2012-04-17 Thread Alexander Krauss


A completely different question is whether we can open testboard to
externals. This might reduce some communication overhead we are seeing
at the moment ("I'm currently testing...", "I have pushed...", etc.)
Essentially, this is just a matter of setting up a proper push-via-https
repository


Since the apache/hg setup on TUM machines is really awkward and 
error-prone, I simply outsourced all these problems and created a mirror 
on Bitbucket:


https://bitbucket.org/akrauss/isabelle-testboard

Interested externals can therefore submit changes for testing and review:

- Create an account at bitbucket
- Send me a short email so that I can give you push permissions.
- Push your changes to the above url.

A cron job at TUM will automaticall pull these changes into testboard.

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

Re: [isabelle-dev] <-> and <-->

I don't really mind, and I imagine that there aren't many uses at the moment, 
so you could get away with it.

On the other hand, it does create an incompatibility between HOL and FOL (and 
therefore ZF).

Larry

On 17 Apr 2012, at 07:35, Tobias Nipkow wrote:

> In HOL, the ASCII syntax for \ is defined to be <-> but
> visually <--> would be more appropriate, closer to --> and would also leave 
> room
> for an ASCII syntax for \ (namely <->).
> 
> Any views on such a change?
> 
> Tobias
> ___
> 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] Towards the next release

2012-04-17 Thread Gerwin Klein

On 12/04/2012, at 7:02 PM, Makarius wrote:
> we need to get to a more concrete release schedule.  Presently I would like 
> to aim for late May, which means we need to start consolidating and 
> converging about now.
> 
> Are there any further big things in the pipeline?

There are two small things from the NICTA side in the pipeline (should be in by 
end of April):

- Tom would like to add a tactic for bit-wise proofs on machine words, based on 
Sacha's and his work a while back. This is one is ready, I'll push it to the 
test board later and add it to the repository if everything works.

- I would like to add a size limit to records beyond which no code generator 
setup is performed. The main reason is that on sizes > 200 fields or so, the 
setup does not make any sense, but consumes very large amounts of memory (and 
time). Switching it off gets rid of almost all of the mysterious memory blowup 
that we had and enables us to run our proofs within 4GB on Linux (32bit) and 
~8GB on Darwin (64bit). Having limits like these is not ideal, but I don't see 
a better workaround, because the code generator setup *is* useful for small 
records. There is a question on how to implement the limit:
 1) as an option available the user at record definition time
 2) as an option/flag to the internal record definition function only
 3) as a configuration option
 4) as a compile time constant 

I'm currently in favour of 4, because the limit is very specialised and will 
only really occur for records that are somehow automatically generated in which 
case the code generator setup is very unlikely to make sense. Options 1 and 3 
would require adding syntax/configuration names which is not really worth it. 
Option 2 threads yet another obscure parameter through a rather large package. 

I'm open to other ideas/comments/feedback, though.

There is a third small thing that I will discuss separately with Florian: there 
is a bug in the code generator setup in Isabelle2011-1 somewhere in generating 
narrowing lemmas. It is triggered for records with more than ~530 fields where 
it constructs a lemma of the form  "f ty = g a b .. aa ab .. tw tx ty tz .." 
where the ty on the rhs is different to the ty on the left. It should be easy 
to fix once I manage to trace down where it is actually constructed and I 
haven't checked yet if it still occurs in the development version.

Cheers,
Gerwin

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

Re: [isabelle-dev] NEWS: auxiliary contexts