Re: [isabelle-dev] Isabelle release test website
On 04/26/2012 02:09 PM, Makarius wrote: The website itself is starting to take shape. Thanks to Johannes Hölzl we now have nice download buttons that detect the platform of the web browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4 buttons are shown if the platform cannot be detected. Please report any problems with your exotic browser and exotic operating system. The idea is that the user can get through with a few standard clicks most of the time, and can ignore the detailed Installation instructions by default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev Hi! My operating system is detected as 32-bit Linux for the following user agent strings, which is wrong. Mozilla/5.0 (X11; Linux x86_64) AppleWebKit/536.4 (KHTML, like Gecko) Chrome/19.0.1079.0 Safari/536.4 SUSE/19.0.1079.0 Opera/9.80 (X11; Linux x86_64; U; en) Presto/2.10.229 Version/11.61 Ondrej ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release test website
On Thu, 2012-04-26 at 14:09 +0200, Makarius wrote: The website itself is starting to take shape. Thanks to Johannes Hölzl we now have nice download buttons that detect the platform of the web browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4 buttons are shown if the platform cannot be detected. There is the (uncommon, perhaps, but not completely absurd) use case where a user wants to download a version for another platform, different from the one she is currently running. To support this, it might be better to have a drop-down list that is initialized to the detected platform, or to add an explicit download link to the other versions. That they are available (only) under Installation instructions is somewhat counter-intuitive. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release test website
On 26.04.2012 14:32, Tjark Weber wrote: On Thu, 2012-04-26 at 14:09 +0200, Makarius wrote: The website itself is starting to take shape. Thanks to Johannes Hölzl we now have nice download buttons that detect the platform of the web browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4 buttons are shown if the platform cannot be detected. There is the (uncommon, perhaps, but not completely absurd) use case where a user wants to download a version for another platform, different from the one she is currently running. Despite my system being mainly 64 bits, I always use the 32-bit version of Isabelle -- AFAIK, with 6GB of RAM I'm still below the point where 64-bit would be an advantage for Isabelle. To support this, it might be better to have a drop-down list that is initialized to the detected platform, or to add an explicit download link to the other versions. That they are available (only) under Installation instructions is somewhat counter-intuitive. Yes, I second that a prominent download for other system button/whatever would be a good idea. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release test website
On Thu, 26 Apr 2012, Lars Noschinski wrote: On 26.04.2012 14:32, Tjark Weber wrote: On Thu, 2012-04-26 at 14:09 +0200, Makarius wrote: The website itself is starting to take shape. Thanks to Johannes Hölzl we now have nice download buttons that detect the platform of the web browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4 buttons are shown if the platform cannot be detected. There is the (uncommon, perhaps, but not completely absurd) use case where a user wants to download a version for another platform, different from the one she is currently running. Despite my system being mainly 64 bits, I always use the 32-bit version of Isabelle -- AFAIK, with 6GB of RAM I'm still below the point where 64-bit would be an advantage for Isabelle. I do it myself as well, but it requires some extra expertise and tinkering of the Linux installation. For Isabelle2011-1 many experienced Linux users were reporting problems with the 32bit version on the 64bit platform, which explains the default to offer 64bit for 64bit now. To support this, it might be better to have a drop-down list that is initialized to the detected platform, or to add an explicit download link to the other versions. That they are available (only) under Installation instructions is somewhat counter-intuitive. Yes, I second that a prominent download for other system button/whatever would be a good idea. The idea was that these users would find their way to the Installation page in the main navigator panel quickly. There is always the problem that too many buttons and links cause an overload of the reader, and are getting ignored. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release test website
On Thu, 26 Apr 2012, Ondřej Kunčar wrote: My operating system is detected as 32-bit Linux for the following user agent strings, which is wrong. Mozilla/5.0 (X11; Linux x86_64) AppleWebKit/536.4 (KHTML, like Gecko) Chrome/19.0.1079.0 Safari/536.4 SUSE/19.0.1079.0 Opera/9.80 (X11; Linux x86_64; U; en) Presto/2.10.229 Version/11.61 I have have added more a checks in js/osdetect.js. Does it work for you now? Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release test website
It works for me, and the auto-detect is nice. The option to download for arbitrary platforms is occasionally useful, but isn't worth making a big effort. A simple link or button labelled “other platforms or “show all platforms should be sufficient. Larry On 26 Apr 2012, at 13:09, Makarius wrote: The website itself is starting to take shape. Thanks to Johannes Hölzl we now have nice download buttons that detect the platform of the web browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4 buttons are shown if the platform cannot be detected. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release test website
The current state of the Download-button can be seen here: http://www21.in.tum.de/~hoelzl/test/ * If the detection does not work all platforms are shown as button * If the detection works then the suggested platforms are shown as buttons, and the other ones as normal links - Johannes Am Donnerstag, den 26.04.2012, 14:09 +0200 schrieb Makarius: The website itself is starting to take shape. Thanks to Johannes Hölzl we now have nice download buttons that detect the platform of the web browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4 buttons are shown if the platform cannot be detected. Please report any problems with your exotic browser and exotic operating system. The idea is that the user can get through with a few standard clicks most of the time, and can ignore the detailed Installation instructions by default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] record: fold_congs/unfold_congs
On Wed, 18 Apr 2012, Thomas Sewell wrote: 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. OK, I knew that the get/map form (called x and x_update here) is fundamentally better that get/put. 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. No need to take action. We leave the status-quo. I have recorded the conclusion of this mail thread in Isabelle/0eadfb89badb in the historically correct wording. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit
Dear all,
with the current repo head (changeset fe43977e434f) I obtain the
following error when trying to start jEdit (after a successful ./build
-b HOL):
### Building Isabelle/jEdit ...
Changed files:
src/isabelle_sidekick.scala
src/isabelle_sidekick.scala:109: error: trait ListCellRenderer takes
type parameters
new ListCellRenderer {
^
src/isabelle_sidekick.scala:113: error: class JList takes type parameters
list: JList, value: Any, index: Int,
^
src/isabelle_sidekick.scala:109: error: type mismatch;
found : AnyRef{}
required: javax.swing.ListCellRenderer[?: Nothing : Any]
new ListCellRenderer {
^
three errors found
Is this related to the recent change from Java 1.7 to 1.6? In other
words, should I locally fall back to Java 1.6 when using the development
repository?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit
Maybe I should have tried it myself before posting ;). Yes, it works
with jdk1.6.0_32.
cheers
chris
On 04/27/2012 01:33 PM, Christian Sternagel wrote:
Dear all,
with the current repo head (changeset fe43977e434f) I obtain the
following error when trying to start jEdit (after a successful ./build
-b HOL):
### Building Isabelle/jEdit ...
Changed files:
src/isabelle_sidekick.scala
src/isabelle_sidekick.scala:109: error: trait ListCellRenderer takes
type parameters
new ListCellRenderer {
^
src/isabelle_sidekick.scala:113: error: class JList takes type parameters
list: JList, value: Any, index: Int,
^
src/isabelle_sidekick.scala:109: error: type mismatch;
found : AnyRef{}
required: javax.swing.ListCellRenderer[?: Nothing : Any]
new ListCellRenderer {
^
three errors found
Is this related to the recent change from Java 1.7 to 1.6? In other
words, should I locally fall back to Java 1.6 when using the development
repository?
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] command value
Sorry, something strange was going on... after loading the file with the
below contents again, the results are different (but I swear that they
have been as shown the first time).
Now the first 'value [simp] revapp xs ys' yields
fold op # xs [] @ ys :: 'a list
which is still strange, since rev_conv_fold is not a simplification rule
but explains the latter three results (which are as expected after [code
del] on rev_conv_fold {why does this have any effect on [simp]?}).
cheers
chris
PS: Sorry for the heavy traffic.
On 04/27/2012 02:33 PM, Christian Sternagel wrote:
Hi all,
after
fun revapp :: 'a list ⇒ 'a list ⇒ 'a list where
revapp [] ys = ys |
revapp (x#xs) ys = revapp xs (x#ys)
lemma revapp [simp, code]: revapp xs ys = rev xs @ ys
by (induct xs arbitrary: ys) auto
value [simp] revapp xs ys
what would you expect as the result of calling value?
I expected rev xs @ ys, but obtained revapp xs ys. What's the reason?
Moreover the outcome of
declare rev.simps [code del, simp del]
declare revapp.simps [code del, simp del]
declare append.simps [code del, simp del]
value [code] revapp [1::nat] [2]
value [simp] revapp [1::nat] [2]
value [nbe] revapp [1::nat] [2]
seems also strange to me. I get
[1, 2] :: nat list
[Suc 0] @ [Suc (Suc 0)] :: nat list
[Suc 0] @ [Suc (Suc 0)] :: nat list
but would expect
an error message about missing code equations
rev [Suc 0] @ [Suc (Suc 0)]
I have no clue what nbe actually does ;)
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
