Re: [isabelle-dev] Isabelle release test website
On Thu, 26 Apr 2012, Christian Sternagel wrote: Referring to http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_25-Apr-2012_bundle_x86_64-linux.tar.gz When calling ./bin/isabelle mirabelle I obtain ... Available OPTIONs for the ACTION sledgehammer: grep: /home/griff/Downloads/Isabelle_25-Apr-2012/src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML: No such file or directory I have amended this in Isabelle/bbc3e7bccc61 -- I was partly responsible for the confusion of Nik Sultana here. I have also made the shell script a bit more robust in 030d3c89eacf, hopefully without breaking it. I was just curious what mirabelle actually is/does, which I still don't know. I don't know how (or if) it is tested. 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
Am 02.05.2012 um 13:55 schrieb Makarius: On Thu, 26 Apr 2012, Christian Sternagel wrote: I was just curious what mirabelle actually is/does, which I still don't know. I don't know how (or if) it is tested. The HOL-Mirabelle session ensures that the ML code compiles. This already catches 98% of what can go wrong. The script itself isn't tested, but I use it frequently, almost weekly, and I never had problems with it before. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] isabelle-release repository
Dear all, we are past point 0 for the Isabelle2012 release. This means: * http://isabelle.in.tum.de/repos/isabelle-release/rev/d9a09f965dab is the starting point for the final phase before roll-out in 2 weeks. There is no push access. Any changes that are essential for the release need to be sent to me via email. * http://isabelle.in.tum.de/repos/isabelle is back in post-release mode right now. Big upheaveals should be avoided, so that the release branch can merged back cleanly in 2-3 weeks; but it is better to publish small changes now than to stockpile for several weeks. * mira tests isabelle, not isabelle-release * isatest tests isabelle-release * nightly development snapshots are from isabelle-release * AFP needs to be understood wrt. isabelle-release (Gerwin will explain his organization of the AFP release for Isabelle2012, based on the afp-devel repository.) * Isabelle2012-RC versions based on isabelle-release will be announced soon. I hope that many people will join the testing efforts on their exotic machines. 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
This is probably the last update of the test website http://www4.in.tum.de/~wenzelm/test/website/ before official release candidates for Isabelle2012 will be announced (also on isabelle-users). The current plan for the deadline for point 0 (the repository fork) is 02-May-2012 -- I will announce it again to make sure that no changeset gets in the wrong place in the critical moment. Afterwards any important amendments need to be sent as individual changesets to me via email. 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 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] Isabelle release test website
Hi all, I spotted this strange line in the NEWS (linked from the test website) symp_def ~ (dropped, use symp_def and sym_def instead) cheers chris On 04/18/2012 10:18 PM, Makarius wrote: In preparation of the release, the following test website is now available: http://www4.in.tum.de/~wenzelm/test/website/ So far this is just for warming up, and to see pending issues of overall system integration. I have already updated many of the contributing components: Scala, Java, Emacs, some ATPs etc. -- so it is worth looking if it already works or not. There are still 2 weeks left to consolidate and converge the main Isabelle repository. This means to wrap up things that are almost ready to be given to end-users, and update NEWS/CONTRIBUTORS accordingly. Things that are not ready should be put in a state where they don't interfere with officially published stable functionality. In the first week of May there will then be the fork to the release repository, which means changes of critical issues can still be sent via email to me, but any other ongoing development will be for the release after the next release on the main Isabelle repository. 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] Isabelle release test website
Referring to http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_25-Apr-2012_bundle_x86_64-linux.tar.gz When calling ./bin/isabelle mirabelle I obtain ... Available OPTIONs for the ACTION sledgehammer: grep: /home/griff/Downloads/Isabelle_25-Apr-2012/src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML: No such file or directory ... (I was just curious what mirabelle actually is/does, which I still don't know). cheers chris On 04/18/2012 10:18 PM, Makarius wrote: In preparation of the release, the following test website is now available: http://www4.in.tum.de/~wenzelm/test/website/ So far this is just for warming up, and to see pending issues of overall system integration. I have already updated many of the contributing components: Scala, Java, Emacs, some ATPs etc. -- so it is worth looking if it already works or not. There are still 2 weeks left to consolidate and converge the main Isabelle repository. This means to wrap up things that are almost ready to be given to end-users, and update NEWS/CONTRIBUTORS accordingly. Things that are not ready should be put in a state where they don't interfere with officially published stable functionality. In the first week of May there will then be the fork to the release repository, which means changes of critical issues can still be sent via email to me, but any other ongoing development will be for the release after the next release on the main Isabelle repository. 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] Isabelle release test website
On Tue, 24 Apr 2012, Jasmin Christian Blanchette wrote: Am 23.04.2012 um 17:22 schrieb Makarius: Here is an update of the test website for warming up a bit more http://www4.in.tum.de/~wenzelm/test/website/ I've spent this cold and wet weekend to produce a monolitic Windows application, which bundles both JDK and Cygwin 1.7.9, see the Download page. (Cygwin 1.7.9 is important here, because in the later version from this year Poly/ML multithreading is a bit unstable.) I use Windows XP on VirtualBox. I downloaded the Isabelle_23-Apr-2012.exe file, moved it to my home directory. Then I started Isabelle.exe and waited over a minute but nothing happened. I suppose here that the self-extracting Isabelle_23-Apr-2012.exe archive did extract correctly, to something like 850 MB directory structure? Then I tried ./bin/isabelle tty but got the message 'Unknown logic HOL -- no heap file found in: /cygdrive/c/.../heaps/polyml-undefined_x86-cygwin Could it be due to Cygwin somehow? I don't know how to launch a terminal for Cygwin 1.7.9, so I'm still using the old terminal for whatever version of Cygwin I had on the machine already. Your existing Cygwin is probably relatively old, such that the poly.exe cannot be started and produce the required version; cf. the undefined above. Starting a terminal for the bundled Isabelle Cygwin now works, but I did not update the 7zip SFX yet. You can do it via http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_23-Apr-2012_bundle_x86-cygwin.tar.gz by untarring that with the existing Cygwin. Then the directory structure can be access via Windows the standard way. There are now Cygwin-Terminal and Cygwin-Setup batch files to be clicked on, which hopefully do the job. You might still have to do a manual incantation from cmd.exe: ...\contrib\cygwin-1.7.9\bin\ash -c /bin/rebaseall This maintenance step requires all Cygwin stuff to be off. 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
Hi Makarius, I suppose here that the self-extracting Isabelle_23-Apr-2012.exe archive did extract correctly, to something like 850 MB directory structure? At least it had the expected directory structure. Your existing Cygwin is probably relatively old, such that the poly.exe cannot be started and produce the required version; cf. the undefined above. Indeed, that must have been it. Starting a terminal for the bundled Isabelle Cygwin now works, but I did not update the 7zip SFX yet. You can do it via http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_23-Apr-2012_bundle_x86-cygwin.tar.gz by untarring that with the existing Cygwin. Then the directory structure can be access via Windows the standard way. There are now Cygwin-Terminal and Cygwin-Setup batch files to be clicked on, which hopefully do the job. That works. Thanks! And indeed, I can reproduce Alex's issue. You might still have to do a manual incantation from cmd.exe: ...\contrib\cygwin-1.7.9\bin\ash -c /bin/rebaseall This maintenance step requires all Cygwin stuff to be off. That didn't seem to be necessary. Jasmin ___ 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
Here is an update of the test website for warming up a bit more http://www4.in.tum.de/~wenzelm/test/website/ I've spent this cold and wet weekend to produce a monolitic Windows application, which bundles both JDK and Cygwin 1.7.9, see the Download page. (Cygwin 1.7.9 is important here, because in the later version from this year Poly/ML multithreading is a bit unstable.) Is there anybody who could lend me a hand to produce a quick download link in JavaScript, like the one on http://mercurial.selenic.com/ that already knows the platform of the user's browser? This could be put prominently on the main index.html, so that download.html only needs to be visited for further details. Last time there was also a surprising number of seasoned Linux users who could not tell if they are running x86 or x86_64; the js magic would help here as well. (For Linux the platform distinction is relevant due common problems caused by C/C++ library dependencies.) 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
Am Montag, den 23.04.2012, 17:22 +0200 schrieb Makarius: Here is an update of the test website for warming up a bit more http://www4.in.tum.de/~wenzelm/test/website/ I've spent this cold and wet weekend to produce a monolitic Windows application, which bundles both JDK and Cygwin 1.7.9, see the Download page. (Cygwin 1.7.9 is important here, because in the later version from this year Poly/ML multithreading is a bit unstable.) The JDK in Isabelle_23-Apr-2012_bundle_x86-linux.tar.gz seams to be the 64-bit version: Isabelle_23-Apr-2012/contrib/jdk-7u3_x86-linux/jdk1.7.0_03/bin/java: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.9, not stripped Is there anybody who could lend me a hand to produce a quick download link in JavaScript, like the one on http://mercurial.selenic.com/ that already knows the platform of the user's browser? This could be put prominently on the main index.html, so that download.html only needs to be visited for further details. Last time there was also a surprising number of seasoned Linux users who could not tell if they are running x86 or x86_64; the js magic would help here as well. (For Linux the platform distinction is relevant due common problems caused by C/C++ library dependencies.) Makarius I already have a download button, I hope it is still on my laptop. I will sent it to you when I'm at home. - Johannes ___ 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 04/23/2012 05:22 PM, Makarius wrote: Here is an update of the test website for warming up a bit more http://www4.in.tum.de/~wenzelm/test/website/ From the monolithic Windows App (with Windows 7): The font in the little symbol replacement popup seems to be wrong: When I enter ==, I just see a little box in that popup. In the main buffer, the symbol is displayed correctly. Alex ___ 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 Mon, 23 Apr 2012, Alexander Krauss wrote: On 04/23/2012 05:22 PM, Makarius wrote: Here is an update of the test website for warming up a bit more http://www4.in.tum.de/~wenzelm/test/website/ From the monolithic Windows App (with Windows 7): The font in the little symbol replacement popup seems to be wrong: When I enter ==, I just see a little box in that popup. In the main buffer, the symbol is displayed correctly. Well-spotted. I've addressed this old Isabelle/jEdit problem in Isabelle/b9e2ed4b1579, but then figured out that it breaks old Java 1.6 on Mac OS X, so I had to revert it. It is one of these moments where it is unclear if Windows or Mac OS X is more annoying. But it seems to be actually a general issue with ListCellRenderer JVM 1.6 vs. 1.7 and Java vs. Scala generics. If I don't get a better idea, I might produce an auxiliary module for ListCellRenderer to be compiled in too variants. 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 Wed, 18 Apr 2012, Johannes Hölzl wrote: When the testboard gives me green light I will tomorrow also push a reworked Probability theory which only takes 2 min to build instead of 5 min as before. I also want to push a new version of the Floats which uses the new lifting infrastructure. Both changes do not change any ML files, and there are only smaller changes to the HOL image, so I hope it is still okay to push this. You still have this convergence interval of 2 weeks. I recommend to push within 1 week, though, since there are usually fine points to be settled afterwards. Concerning the new lifting infrastructure: I've seen many things floating in the past few weeks, but it was never mentioned before, and is not covered in NEWS. So my impression was it is not user-relevant for this release, as the NEWS title calls it. Also, there seem to be certain ongoing things with quotients that are nowhere covered. The time to do so is now. Anything not wrapped for this release, is for the one after it. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle release
Dear all, the release is alreay in place, but before announcing it officially the Sydney mirror needs another round of updating, which will probably happen around midnight GMT. This gives another chance to sport drop-outs on the website. The main Isabelle repository is already in post-release mode: I have merged the release branch in Isabelle/d78ec6c10fa1. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release
I looked for the documentation of HOL-Probability, but it looks like it is missing. It should be under HOL-Multivatiate-Analysis, but there are now further Session. Was there a change in the build-system? - Johannes On Mon, 10 Oct 2011, Makarius wrote: Dear all, the release is alreay in place, but before announcing it officially the Sydney mirror needs another round of updating, which will probably happen around midnight GMT. This gives another chance to sport drop-outs on the website. The main Isabelle repository is already in post-release mode: I have merged the release branch in Isabelle/d78ec6c10fa1. 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] Isabelle release
On Mon, 10 Oct 2011, Johannes Hoelzl wrote: I looked for the documentation of HOL-Probability, but it looks like it is missing. It should be under HOL-Multivatiate-Analysis, but there are now further Session. Was there a change in the build-system? Yes in fc3bb3a42369 by Alex Krauss, to accomodate SML/NJ in mira. I have now updated the library build script accordingly (e54a985daa61) and rebuilt the whole thing. This now takes 4h, which looks more realistic than the 2h before. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle-release repos
Am 26.09.2011 um 20:20 schrieb Makarius: I am about to produce the release clone. The current tip eb7a797ade0f will probably be the fork point. This includes a few changes by Lukas and Jasmin from today, and I understand that these were meant to go into this release, not the next one. Oops, I was among those who was confused about the fork procedure. My changes were intended for the next release. Ah well, they should be fine for this release as well (and the old Kodkodi 1.2.16). Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] isabelle-release repository
The release branch for Isabelle2011-1 is now at http://isabelle.in.tum.de/repos/isabelle-release Any small changes and amendments can be mailed to me (cf. hg export or hg bundle). Things to be added to isabelle-release should *not* be pushed on the main isabelle repository, to avoid the confusion of self-merges with copied changesets. isatest will also test http://isabelle.in.tum.de/repos/isabelle-release within the next few weeks. (In the past I used to have a minimal isatest for http://isabelle.in.tum.de/repos/isabelle but that was superseded by http://isabelle.in.tum.de/reports/Isabelle/ last time. Can we count on this again?) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle-release repository
On 09/26/2011 11:38 PM, Makarius wrote: isatest will also test http://isabelle.in.tum.de/repos/isabelle-release within the next few weeks. (In the past I used to have a minimal isatest for http://isabelle.in.tum.de/repos/isabelle but that was superseded by http://isabelle.in.tum.de/reports/Isabelle/ last time. Can we count on this again?) Yes. Our mira setup will run Isabelle_makeall as usual both for official changes and stuff pushed to testboard. There are also AFP tests etc. Note that before Isabelle and the AFP are released, changes to Isabelle are basically limited to ones that do not break the AFP (unless Gerwin plans to fork, too). Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle-release repository
On 27/09/2011, at 7:45 AM, Alexander Krauss wrote: On 09/26/2011 11:38 PM, Makarius wrote: isatest will also test http://isabelle.in.tum.de/repos/isabelle-release within the next few weeks. (In the past I used to have a minimal isatest for http://isabelle.in.tum.de/repos/isabelle but that was superseded by http://isabelle.in.tum.de/reports/Isabelle/ last time. Can we count on this again?) Yes. Our mira setup will run Isabelle_makeall as usual both for official changes and stuff pushed to testboard. There are also AFP tests etc. Note that before Isabelle and the AFP are released, changes to Isabelle are basically limited to ones that do not break the AFP (unless Gerwin plans to fork, too). I've changed the afp test to point to isabelle-release for now. Unless people tell me they have incoming changes to the AFP that depend on new Isabelle changes before the release, I do not plan to fork. There are 3 new small entries that should come in before the release and 2 entries currently broken (Jinja JinjaThreads). Florian and I are working on the latter. If someone has time, it would be nice to take a look at Jinja. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release
Hi all, (must add my 2ct, too) Concerning the content of the next release: Brian wrote: What exactly makes it major? Judging by the NEWS file, it looks like 2009-2 introduced about as many new features as the upcoming release will. Is there any new feature in particular that is considered a major change? There are certainly many interesting things: Coercions, partial_function (though that is still lacking induction rules so it's a bit unfinished), smt in sledgehammer, big HOLCF cleanup etc. But I find it impossible to assign a 'major' predicate consistently. And what is major for one user is irrelevant for the other. I have the same feeling as Gerwin concerning release naming. When Isabelle 2009-2 came out, several users asked me about the name and I found it hard to give them a consistent answer. Also, in this particular situation, having an Isabelle 2010 release in January looks a bit like they didn't make their planned release date :-) Larry wrote: I'm afraid that I originated the custom of not always linking the release name to the calendar year. The idea was to indicate that the new release consisted of little more than patches from the previous one. Larry, would you say that this is still adequate given how Isabelle evolves today? Are we talking 'just patches' here, given the changes mentioned above (plus countless small improvements everywhere as usual)? Or what is it? To me it is just the next small step in a sequence, and after 10 years we look back and are surprised about the 'major' changes that happened. Michael wrote: Or dispense with year numbers entirely. Even Microsoft gave up on that idea for Windows. But then we need a Marketing division to come up with a new name every 8 months :-}. Year numbers are very comfortable. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release
On 7/01/11 8:05 PM, Alexander Krauss wrote: But then we need a Marketing division to come up with a new name every 8 months :-}. Year numbers are very comfortable. You either come up with a set of names to use, or just do what most software projects do (commercial and open source both), and use numbers. Does the gcc project have this problem? Does Linux? Does emacs? Decide retroactively that everything up until this point was Isabelle 1, and announce the release of Isabelle 2. Or whatever set of numbers floats your boat... Michael ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release
I like the wine connection! Not just French wines, but also Australian ones, and German Rieslings come to mind. Not sure though how the UK fits in, at least not yet, although global warming will fix that in a few decades. Tobias Rafal Kolanski schrieb: I think the yearly naming convention has a rustic charm about it, kind of like french wines. We can all sit down one day and have a big discussion which year was the best vintage. Reminisce about the more intense full-bodied flavour of the second batch of 2009, which is lovely in small sips, but can go a bit awry when large gulps are involved... or the effect on the palate of annually increasing Scala overtones; it shall be grand! On a more serious note, +1 for calling it Isabelle 2011. Rafal Kolanski. On 07/01/11 20:00, Michael Norrish wrote: On 7/01/11 7:53 PM, Tobias Nipkow wrote: I don't see any good reason for the skewed naming scheme of 2009-x in 2010 or 2011. We should use the year that the release was made in, period. That avoids unproductie arguments on how major or minor a release is. Or dispense with year numbers entirely. Even Microsoft gave up on that idea for Windows. Michael ___ 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] Isabelle release
I'm afraid that English wine production has been increasing year by year. Some of them are even said to be good. http://www.english-wine.com/vineyards.html Larry On 7 Jan 2011, at 09:30, Tobias Nipkow wrote: I like the wine connection! Not just French wines, but also Australian ones, and German Rieslings come to mind. Not sure though how the UK fits in, at least not yet, although global warming will fix that in a few decades. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release
On 07/01/11 20:07, Michael Norrish wrote: On 7/01/11 8:05 PM, Alexander Krauss wrote: But then we need a Marketing division to come up with a new name every 8 months :-}. Year numbers are very comfortable. You either come up with a set of names to use, or just do what most software projects do (commercial and open source both), and use numbers. Does the gcc project have this problem? Does Linux? Does emacs? Decide retroactively that everything up until this point was Isabelle 1, and announce the release of Isabelle 2. Or whatever set of numbers floats your boat... Taking a page from a successful marketing campaign, we could also adopt a variation on the Ubuntu way of naming things, two numbers: year and month. So this would be Isabelle 10.01. We can even add silly names like Anomalous Assumption, Bound Beta, Circular Coinduction, Dramatic Datatype, Epic Elimination, etc. I thought this might be a bit too silly to send to the dev list, but a third party encouraged me to do so anyway :) Rafal Kolanski. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release
On Fri, 7 Jan 2011, Rafal Kolanski wrote: Taking a page from a successful marketing campaign, we could also adopt a variation on the Ubuntu way of naming things, two numbers: year and month. So this would be Isabelle 10.01. We can even add silly names like Anomalous Assumption, Bound Beta, Circular Coinduction, Dramatic Datatype, Epic Elimination, etc. I thought this might be a bit too silly to send to the dev list, but a third party encouraged me to do so anyway :) Funny idea :-) :-) I am a user of Ubuntu myself, but never know which version it is, because both the numbers and the names are hard to remember for me. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release
On 07/01/2011, at 3:59 AM, Makarius wrote: Bonne année à tous, this is a reminder that we are approaching the next official Isabelle release. I've got myself caught into too many other tasks over Christmas vacation, and will now see how quick we can get a lift off. If everybody else manages to wrap up until the beginning of next week, we have a good chance to release before the end of the month. Looking forward to it :-) I think a release date of January 2011 still justifies to call the release Isabelle2010. Why would we want to, though? Not that it's that important (which makes it all the easier to have long discussions about it ;-)), but no matter how you look at it, we're suggesting some correlation between release year and name. Then we twist it slightly to mean when we did most of the work on it or what it is most similar to if it is a minor release. I don't think the mythical normal user cares about that. But they do get confused by Isabelle2010 coming out in 2011 and 2009-2 coming out in 2010 etc. There's a fairly simple way of appearing a lot less weird to the outside world. Just take the release date and call it that. If we have more than one release per year, -n makes perfect sense, but otherwise it causes more confusion than what it carries in information for the select few who know what it means. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release
On Thu, Jan 6, 2011 at 8:59 AM, Makarius makar...@sketis.net wrote: If everybody else manages to wrap up until the beginning of next week, we have a good chance to release before the end of the month. This sounds good. I think a release date of January 2011 still justifies to call the release Isabelle2010. I guess naming it Isabelle2010 rather than Isabelle2009-3 signifies that this is a major, rather than a minor release. What exactly makes it major? Judging by the NEWS file, it looks like 2009-2 introduced about as many new features as the upcoming release will. Is there any new feature in particular that is considered a major change? - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle release snapshot
After additional delays due to some confusion how the release process actually works, we have now reached point zero. This means that version 2ca2693a8c10 has been forked to a separate repository clone http://isabelle.in.tum.de/repos/isabelle-release This is meant to become the officially published version within 1-2 weeks. Only fixes of serious problems will be accepted on that branch (by producing clean changesets to be grafted on that tree, cf. hg export or hg bundle). (1) Testing. This is the opportunity to try out if everything works for the end-user, including the delicate system integration on Linux, Mac OS, and Cygwin. An early version of the still emerging website is available here: http://www4.in.tum.de/~wenzelm/test/isa2009-1-test/ We are still hoping for: * a stable version of Proof General 4.0 * a stable version of Cygwin 1.7 Note that the automatic isatest jobs and the development snapshot will refer to http://isabelle.in.tum.de/repos/isabelle-release (2) Ongoing development. The main pull/push area http://isabelle.in.tum.de/repos/isabelle is already open for post-release stuff right now. None of that will affect the coming official Isabelle2009-1. (In the past we used to have up to 2 weeks of zero-entropy, but thanks to Mercurial this is no longer required.) Nonetheless, bigger changes of theory libraries should be avoided. In particular, afp-devel needs to work with the isabelle-release branch, in praparation of the official AFP release for Isabelle2009-1 that happens in parallel. Makarius
[isabelle-dev] Isabelle release
On Fri, 16 Oct 2009, Makarius wrote: Dear Isabelle contributors, we need to approach the next official Isabelle release. The basic plan is to get things done this fall, which means there are only 2-3 weeks left for substantial changes. After that there will be a few more weeks for polishing and fine-tuning -- this phase becomes longer and longer as the system gets more complex. Now is the time to finish things and put them into a state for end-users out there. If there are still major things waiting in your pipeline, please say so. This is already from one month ago. Is there anything left in anybody's pipeline? I would like to freeze the next few days (although it is unusually warm for November in these parts). Makarius
[isabelle-dev] Isabelle release
Dear Isabelle contributors, we need to approach the next official Isabelle release. The basic plan is to get things done this fall, which means there are only 2-3 weeks left for substantial changes. After that there will be a few more weeks for polishing and fine-tuning -- this phase becomes longer and longer as the system gets more complex. Now is the time to finish things and put them into a state for end-users out there. If there are still major things waiting in your pipeline, please say so. Makarius
