Re: [isabelle-dev] Preferences on Mac OS X

[Andrew Boyton]

The fact that Isabelle/jEdit doesn't obey the standard OS X keybindings is 
frustrating but sadly typical for a Java application. For a Mac application I 
expect Command+, to bring up the preferences, but I also expect the preferences 
to be in the menu "jEdit -> Preferences", like every other Mac application. I 
do accept though that Java applications are rarely good citizens on any 
platform, and so am not surprised.

As for your question Larry, the lack of standard Mac keybindings can be 
alleviated by re-enabling the option key, and changing adding the following 
lines in a new file in isabelle/src/Tools/jEdit/dist/startup (I made one called 
Option.bsh) [1]:

Debug.ALT_KEY_PRESSED_DISABLED = false;
Debug.ALTERNATIVE_DISPATCHER = false;

and then, in jEdit -> Utilities -> Options… set the following:

  *   Appearance -> Swing look & feel: -> Mac OS X
  *   Shortcuts -> Choose keymap -> Mac OS X

Whilst this doesn't fix all the keybindings, but it helps. It does fix the 
cursor movement to be standard though, which goes a long way. This should be 
the standard settings on Isabelle/jEdit on a Mac IMHO.

Personally, I'd prefer if Command+F was used for incremental search, as it's 
the one you generally use more than "Find". Either way, I find that switching 
between Isabelle/jEdit and other text editors highly distracting as I get used 
to Command+, being used for search, and then it bringing up Preferences on 
every other program. Making Isabelle/jEdit a better OS X citizen goes a long 
way for making it nicer for people like myself to use. I understand that this 
makes it harder for people who regularly move between platforms though.

Kind regards
Andrew


[1]: This is based on information from 
http://stackoverflow.com/questions/2297727/jedit-mac-os-keyboard-behaviour but 
I've found Isabelle (or something, I'm yet to work out what) often reverts 
changes I make to startup.bsh, so I've found making a new file in the same 
directory safer.



On 25/09/2013, at 8:05 AM, Lawrence Paulson 
mailto:l...@cam.ac.uk>> wrote:

Never tried using this with jEdit.

I won't mind having the Mac cursor-movement keyboard shortcuts.

Larry

On 24 Sep 2013, at 22:43, Makarius 
mailto:makar...@sketis.net>> wrote:

How important is the canonical key sequence "COMMAND comma" as defined by Apple?

___
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

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

[Jasmin Christian Blanchette]

Hi all,

Isabelle/jEdit is currently unwilling to process theories (as of dcefe11f28f2). 
I open up an existing theory file, e.g.

isabelle jedit -l HOL-BNF src/Doc/Datatypes/Datatypes.thy

The file is correctly opened, but nothing is processed -- no imports are 
processed, the theory text has a pink background, etc. The "Theories" tab only 
lists the current theory, with a pink background. Everything was working fine 
on Monday and Tuesday morning, if I remember correctly. Proof General works 
fine. I didn't change any components.

This is on Mac OS X 10.8. I'll be happy to help reproduce the problem.

Jasmin

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

Re: [isabelle-dev] Preferences on Mac OS X

[Lawrence Paulson]

Never tried using this with jEdit. 

I won't mind having the Mac cursor-movement keyboard shortcuts.

Larry

On 24 Sep 2013, at 22:43, Makarius  wrote:

> How important is the canonical key sequence "COMMAND comma" as defined by 
> Apple?

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

Re: [isabelle-dev] Preferences on Mac OS X

[Jasmin Christian Blanchette]

Am 24.09.2013 um 23:43 schrieb Makarius :

> This is a question to hard-core users of Mac OS X.
> 
> How important is the canonical key sequence "COMMAND comma" as defined by 
> Apple?

It's probably important, but I don't use it (for lack of having memorized it).

> Alternatively, I am open to suggestions for a replacement key for the default 
> keymap, one that works on English, German, French keyboards, or lets say 2 
> out of these 3.

Cmd comma currently pops up an inline search. To me something like Alt Cmd F or 
Shift Cmd F would make sense, since it can be seen as a variation of Cmd F.

Jasmin

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

[isabelle-dev] Preferences on Mac OS X

[Makarius]

This is a question to hard-core users of Mac OS X.

How important is the canonical key sequence "COMMAND comma" as defined by 
Apple?


See also 
http://sourceforge.net/tracker/?func=detail&aid=3615047&group_id=588&atid=100588


For me as multiplatform user, it is more annoying to have different ways 
to do the same thing.  C+comma is quite central in jEdit, so my own 
tendency would be to find a way to take it away from Apple, not the other 
way round.


Alternatively, I am open to suggestions for a replacement key for the 
default keymap, one that works on English, German, French keyboards, or 
lets say 2 out of these 3.



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 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] Converting existing proofs from apply-style to "structured" Isar-style

[Makarius]

On Mon, 16 Sep 2013, Josh Tilles wrote:

Interesting—I had assumed that changing the proof of a lemma and/or 
theorem had no functional impact on the code once said lemma/theorem had 
been verified. Am I incorrect about that? (If the explanation is 
complicated, please don't feel obligated to go into complete detail. A 
one-word answer will tell me all I probably *need* to know. Any further 
explanation would just be to satisfy my beginner's curiosity)


Main Isabelle/HOL is a bottle neck in several respects, even just the 
performance of doing the proofs (with or without explicit proof terms).


Below its Main theory any change requires someone with a few years of 
experience to make non-trivial changes -- otherwise the bootstrap process 
might get affected one way or the other.  Between Main and Complex_Main it 
is a bit easier, but a change there still requires to rebuild almost 
anything else (this takes about 1-2h these days, where such things are 
really fast compared to past times).


It is much more relaxed and fun to look through outlying, presently hardly 
maintained areas, where some gems might be uncovered without getting into 
technical difficulties.


In preparation of the Isabelle2013-1 release, I am myself training my 
fingers (and testing the Prover IDE real-time dynamics) on 
HOL/Multivariate_Analysis.  These huge and mostly unformatted theories now 
work out rather smoothly, even on my old 2-core MacBook Pro.



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

Re: [isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style

[Makarius]

On Mon, 16 Sep 2013, Josh Tilles wrote:


On Tue, Jul 30, 2013 at 3:42 PM, Lawrence Paulson  wrote:


This could be a valuable service, especially for long lists of applys.


Thank you for the encouragement! I'm glad to see you agree.


(A proof like "by (induct n) auto" should be left alone.)


Understood. If I come across proofs comprising only two `apply`s, should I
tweak them to use the briefer `by method1 method2` form? Or would that be
considered a pedantic waste of time?


Depends on the situation.  Conceptually, the Isar 'by' command takes first 
an "initial method" to split up the problem in a top-down manner (using 
its facts that are passed to it), and second a "terminal method" to solve 
what comes out of that.


This structured double-step is conceptually different from the sequential 
composition of the two proof methods.  (When facts are involved it is also 
operationally different.)  So when that was the real intention of the 
proof author, even without knowing about such fine points, it is 
appropriate to make just one Isar 'by' step from certain minimal apply 
scripts. In other situations it is a lost cause -- no structure to be 
recovered so easily.


After developing some routine with Isar, you should get an idea what to do 
when.  It requires some practice to develop proper style -- just line wine 
tasting.



Makarius

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

Re: [isabelle-dev] Isabelle_10-Sep-2013

[Makarius]

On Wed, 11 Sep 2013, Gerwin Klein wrote:

An aside: The more AFP entries are used as proper libraries, the more 
we need to think how release processes need to interact etc.


We've been thinking about that from the start. There shouldn't be 
anything special to do. AFP-2013-1 will come out a few days after 
Isabelle-2013-1 and should work together with it.


There is only a minor point to be reconsidered: when exactly to start 
getting in sync with the Isabelle release.  Just ss last time, we will 
have several weeks of public Isabelle release candidates that are mostly 
indistinguishable from the final release.  So users will be invited to 
start using (and porting existing applications) with RC1 already.


This grey period between RC1 ... final will be relatively long this time, 
since I will disappear on my post-summer vacation in the middle of it.



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

Re: [isabelle-dev] Isabelle-10-Sept

[Makarius]

On Tue, 10 Sep 2013, Alfio Martini wrote:

On the other hand, the (propositional) operators of HOL-formulae are 
still not properly shown in the sidekick pane as the image attached 
shows. I am not sure if this is a "feature" or a known bug, but this is 
problem is also present in the current version.


I think this visual glitch has been there all the time -- I did not notice 
it myself so far, since I am not using Windows every day (but still quite 
often to test things). No other Windows user has pointed that out yet, 
maybe because Windows users traditionally think that problems are normal. 
On the other hand the really anoying problems today are on Mac OS X and 
Linux -- this is particularly bad because it used to be better a few years 
ago.


In the longer term I would like to replace SideKick by a more versatile 
tree view (or even graph view) of the PIDE document model.  The completion 
has already been replaced like that for the coming release.  Getting rid 
of Isabelle Sidekick altogether will take longer.



Since I've passed by the SideKick plugin sources today, I've had a brief 
look what they are doing.  In principle it should be reasonably easy to 
modify SideKickTree.Renderer (and the corresponding "Asset") to allow an 
explicit font specification.  This would require to engage with the 
maintainers of the plugin at the jEdit Sourceforge project, and will 
probably take 1 or 2 release cycles of jEdit.


I am presently involved with the jEdit Sourceforge project, but for much 
more elementary things, like getting Java 7 on Mac OS X work smoothly. 
Everybody is hoping to discontinue Java 6 soon, but it is not for free to 
dismantle old stuff.



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

Re: [isabelle-dev] Sledgehammer proof text insertion

[Makarius]

On Thu, 5 Sep 2013, Lars Noschinski wrote:


On 05.09.2013 13:35, Florian Haftmann wrote:

Hi,

after some time playing around with the new sledgehammer panel
(ab4edf89992f), here my feedback:


Regarding this (and also the new Find panel), I would like to see a keyboard 
shortcut, not only to open the panel (those can already be defined), but to 
select the major function of the panel, i.e.


 start sledgehammer for the sledgehammer panel

and

 give focus to the search term input box for the find panel.


I've made several refinements, including the usual Mac OS X add-ons after 
everything seems finished (104a08c2be9f etc.).


The jedit actions isabelle.find-panel and isabelle.sledegehammer-panel 
should popup these panels, and give focus according to normal jEdit window 
manager rules, unless prevented by operating system window manager rules.


Also note that the little action command line (C+ENTER) of jEdit has 
built-in completion via TAB.  (Unfortunately that important jEdit 
functionality is presently broken for Mac OS X, probably due to some 
strange GUI focus effects, that are independent of the focus stuff I've 
done elsewhere.)


jEdit actions can be bound to keyboard shortcuts, menus etc.  In jEdit 
such things are normally not done by default, since the keyboard space is 
relatively limited -- this is not ESCAPE-META-ALT-CONTROL-SHIFT.  (We have 
even some pending problems with important key sequences like COMMAND-comma 
on Mac OS X that need be be remapped, since it clashes with standard 
Preferences functionality according to Apple.  I did not find a reasonable 
free slot on the intersection of English / German / French keyboard yet. 
Another open problem is how to reconcile the recent split into several 
default keymaps -- every jEdit developer now seems to have his very own.)



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

Re: [isabelle-dev] sledgehammer panel problem

[Lawrence Paulson]

Thanks for the response, but my issue has nothing to do with editing the 
surrounding text. On the contrary, it has to do with activating s/h, walking 
away from the computer, and coming back to find that "sendback" does not work. 
So I'm force to watch s/h and choose one of the metis calls before s/h 
terminates. 

Larry

On 24 Sep 2013, at 20:52, Makarius  wrote:

> On Mon, 16 Sep 2013, Lawrence Paulson wrote:
> 
>> Any generated "metis" calls only self-insert if clicked before s/h 
>> terminates. If you ignore your session for a few minutes while s/h runs (as 
>> many people do), then the highlighted links will be inactive when you get 
>> back. I've checked this several times.
> 
> The "sendback" text addresses a particular command in the text, if that is 
> destroyed by editing, it will not work.
> 
> Part of the problem is the old debate what a command span really is.  1.5 
> years ago I've broken with ancient traditions and lessons learned from Proof 
> General and *included* trailing whitespace/comments here.  This had a slight 
> advantage in the total number of command transactions.
> 
> Many other surprises were coming from it, though.  Here the snag is that 
> appending something after a command affects its trailing white space and thus 
> resets it.
> 
> 
> In Isabelle/88c6e630c15f we are now back to the old scheme to *exclude* 
> trailing whitespace/comments and make a separate "ignored" command span 
> instead.  The notion of "current_command" for Output and query operations 
> like Find or Sledgehammer is adapted accordingly.
> 
> So the command where sledgehammer is applied is now more robust against edits 
> of the surrounding text.  Hopefully this scheme is sufficient 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] The coming release

[Jasmin Blanchette]

Am 24.09.2013 um 22:10 schrieb Makarius :

> 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] »Find theorems«-Panel

[Makarius]

On Thu, 5 Sep 2013, Florian Haftmann wrote:


At some stage I would expect some »click and copy to theory buffer«
functionality, e. g.

thm foo

or

from foo have "" .


I would say that is another instance of "structured editing".  Output 
should provide systematic markup about the "Isabelle sublanguage" that is 
being used, e.g. "fact expression".  Copy-pasting that should do the right 
thing, depending on the syntactic context of the target.


This is for *some* future release ...


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

Re: [isabelle-dev] Sledgehammer proof text insertion

[Makarius]

On Thu, 5 Sep 2013, Florian Haftmann wrote:

I also observed that if you use sledgehammer as old-style keyword, the 
proof text is inserted after instead of just replacing


This goes back to Isabelle/a0db255af8c5 from 1 month ago:

  sledgehammer sendback always uses Markup.padding_command: sensible
  default for most practical applications -- old-style in-line replacement
  is superseded by auto mode or panel;
  back to Normal mode: with output_result it is sufficient to determine
  TTY vs. PIDE operation;

I've just got entangled into "too many modes", even nested ones.  So I've 
just made a clear cut, at the cost of loosing some former features, but 
they were intermediate anyway until a proper control panel would arrive.


The "too many modes" problem has already become a new Isabelle insider 
jargon expression in the past few months.  (It needs to be distinguished 
from "too many notes" from Amadeus.)



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

Re: [isabelle-dev] sledgehammer

[Makarius]

On Mon, 2 Sep 2013, Lawrence Paulson wrote:

I agree that the generated proof should start on a fresh line, because 
these calls are often quite lengthy text strings.


The fresh line is there in Isabelle/88c6e630c15f but it is merely
minimalistic tuning.

The concept that is missing here is some structural editing of the text: 
copy-pasting sub-proofs should somehow take the structure into account, 
with proper whitespace, line breaks and indentation according to Isar.


That's left for a future release.


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

Re: [isabelle-dev] sledgehammer

[Makarius]

On Mon, 2 Sep 2013, Tobias Nipkow wrote:


Am 02/09/2013 11:18, schrieb Makarius:

The sledgehammer panel has had only 1-2 rounds of refinements so far, and more
precise observations by testers on this mailing list will be required to make it
work smoothly for the coming release.



Some observations:

- When clicking on the generated proof it is appended to the end of the proof
text preceding the invocation point. It would be better to insert a newline
first - otherwise the proof develops in a horizontal rather than the standard
vertical direction.

- Sometimes I click on the generated proof and it is not pasted into the theory
text. It just doesn't work, even if I click repeatedly.  I cannot reproduce this
reliably.

- Once one has clicked on a proposed proof and it has been pasted into the
theory window, this does two things:
 a) it stops the rest of the running atps.
 b) it disables all the proposed proofs, i.e. no more click-and-paste for any
of them.
Neither is desirable and I thought at least a) was not the case in the past.


All of that has improved in Isabelle/08721d7b2262 (and its vicinity). 
I've made some fine-tuning without fundamental changes to how it all 
works.  Lets see if this is sufficient for the release.



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 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] Find theorems and Sledgehammer Panels

[Makarius]

On Mon, 23 Sep 2013, Makarius wrote:

With Isabelle/322a3ff42b33 there is now completion for the history text 
field behind it.


It is again one of these typical instances of spending 2h to make it 
work on Linux and Windows, and requiring days or weeks to find out why 
Apple/Oracle don't quite manage on Mac OS X: the focus change after 
completion selects all text.  (Problem still pending.)


Apple makes it more difficult to get into its dungeons where the real 
sources are guarded by dragons, but there were people in the past who have 
seen them.  According to some Mark Swingler, Java Runtime Engineer at 
Apple Inc. in 2008, the Java Mac OS X look-and-feel *has* to select all 
text after change of focus of the GUI component.


So despite roaring crowds on the Web shouting "bug", this behaviour is 
normal.  The business model of Mac OS X is to be different.  (Linux 
communities are different without a business model behind it.)


Luckily there was also an explanation by the same guy how to disable 
normal Apple behaviour and imitate Linux and Windows.  Thus our text field 
completion becomes more usable in Isabelle/8d7029eb0c31.



Software development in the 21fst century is a strange adventure game, 
where one needs to solve quests in dark places ...



Makarius

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

Re: [isabelle-dev] sledgehammer panel problem

[Makarius]

On Mon, 16 Sep 2013, Lawrence Paulson wrote:

Any generated "metis" calls only self-insert if clicked before s/h 
terminates. If you ignore your session for a few minutes while s/h runs 
(as many people do), then the highlighted links will be inactive when 
you get back. I've checked this several times.


The "sendback" text addresses a particular command in the text, if that is 
destroyed by editing, it will not work.


Part of the problem is the old debate what a command span really is.  1.5 
years ago I've broken with ancient traditions and lessons learned from 
Proof General and *included* trailing whitespace/comments here.  This had 
a slight advantage in the total number of command transactions.


Many other surprises were coming from it, though.  Here the snag is that 
appending something after a command affects its trailing white space and 
thus resets it.



In Isabelle/88c6e630c15f we are now back to the old scheme to *exclude* 
trailing whitespace/comments and make a separate "ignored" command span 
instead.  The notion of "current_command" for Output and query operations 
like Find or Sledgehammer is adapted accordingly.


So the command where sledgehammer is applied is now more robust against 
edits of the surrounding text.  Hopefully this scheme is sufficient 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] 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 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] Some proposed extensions to the Isabelle library

[Tobias Nipkow]

Am 21/09/2013 03:08, schrieb Alessandro Coglio:
> 
> I also have a general question about library vs. AFP. There seem to be clear
> cases of things that should go into the library (e.g. new theorems on lists or
> sets) and clear cases of things that should go into the AFP (e.g. a theory of
> context-free grammars). But some cases are less clear to me; for example, 
> while
> lattices are in the library, I noticed that categories are in the AFP (well,
> categories are used much less frequently than lattices, so perhaps that's a
> criterion).

It is not alwasy clear, but your analysis is correct.

> More concretely, I've been working on a couple of developments
> (/not/ included in the attached file) that I can imagine going into either 
> place:
> 
>   * A theory of indexed products, modeled via maps and also modeled via 
> functions.
>   * A theory of ranges over orders/lattices, part of which use the indexed
> products mentioned above.
> 
> Does anybody have any guidance? Out of curiosity, have theories ever moved
> between library and AFP, in either direction?

It sounds like it is better for the AFP, but when you submit it and we see it we
may feel differently.

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

Re: [isabelle-dev] Some proposed extensions to the Isabelle library

[Tobias Nipkow]

Am 21/09/2013 03:08, schrieb Alessandro Coglio:
> Hello,
> 
> The attached file contains a fairly heterogeneous collection of potential
> extensions to the Isabelle library, which I've been developing as part of some
> projects that I'm working on. I think that other Isabelle users may find them
> useful.


Thank you for your lemmas.

I found

lemma finite_number_of_maps_with_finite_domain_and_finite_range:
"finite A ==> finite {m::'a \ ('b::finite). dom m = A}"

useful and included it in this more general form

lemma finite_set_of_finite_maps:
assumes "finite A" "finite B"
shows  "finite {m. dom m = A \ ran m \ B}"

with a proof via the finitness of the set of graphs.

I decided against the list ones merely because they are short and easy but will
look at the while_option ones.

Other people should move other lemmas they find interesting.

Thanks again
Tobias

> Please let me know if you'd rather receive these in smaller chunks, if 
> anything
> needs more explanations, if anything should be changed to conform to Isabelle
> library styles/conventions, etc.
> 
> I also have a general question about library vs. AFP. There seem to be clear
> cases of things that should go into the library (e.g. new theorems on lists or
> sets) and clear cases of things that should go into the AFP (e.g. a theory of
> context-free grammars). But some cases are less clear to me; for example, 
> while
> lattices are in the library, I noticed that categories are in the AFP (well,
> categories are used much less frequently than lattices, so perhaps that's a
> criterion). More concretely, I've been working on a couple of developments
> (/not/ included in the attached file) that I can imagine going into either 
> place:
> 
>   * A theory of indexed products, modeled via maps and also modeled via 
> functions.
>   * A theory of ranges over orders/lattices, part of which use the indexed
> products mentioned above.
> 
> Does anybody have any guidance? Out of curiosity, have theories ever moved
> between library and AFP, in either direction?
> 
> Thank you in advance and best regards.
> 
> 
> 
> 
> 
> 
> ___
> 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