Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Hi again, the current state of affairs concerning 'a set can be followed there: https://isabelle.in.tum.de/isanotes/index.php/Having_%27a_set_back Although I'd appreciate to see progress there, I do not ask to distract any attention from tasks for the upcoming release. Two remarks concerning the Isabelle distribution itself: * In HOL-Nominal-Examples, equivariance in theory Fsub fails. My knowledge about equivariance is too restricted to decide whether this is a mistake in the (adjustion of the) implementation or maybe needs additional declarations etc. I'm happy about any hints concerning this. * The remaining issues mainly are concerned with particular tools at which the corresponding maintainers should have a closer look at (if not done already). Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bash subcommand completion for isabelle
On 26/09/2011, at 6:43 PM, Florian Haftmann wrote: An aside: have there ever been thoughts about adding subcommand completion for isabelle in bash? At first sight this looks as a nice thing to have, but maybe there have been deeper consideration *not* to attempt this. I've been using the attached for a few years. Just load as part of your ~/.bashrc or similar. It does 'isabelle make' target completion as well (code based on make completion from bash back then). It probably needs a thorough code review before it can be put anywhere official. I've mostly used it just for myself, even though I think I sent it to isabelle-users at some point. Cheers, Gerwin isabelle-completions Description: Binary data PGP.sig Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bash subcommand completion for isabelle
On Mon, 26 Sep 2011, Florian Haftmann wrote: An aside: have there ever been thoughts about adding subcommand completion for isabelle in bash? At first sight this looks as a nice thing to have, but maybe there have been deeper consideration *not* to attempt this. There are no deeper reasons why it was not done so far. When the old isatool now isabelle wrapper was introduced in 1996, bash completion was not as configurable as it is now. Even the list of the available subcommands was crude and slow -- I have rewritting it in perl only a few months ago to make it more smooth. Generally, my tendency is to reduce the importance of command line tools. Pretty soon there should be the Isabelle/Scala based isabelle build tool, which would also work directly in the Prover IDE. This does not mean that the terminal will disappear, but many users on Mac OS and Windows do not know what it is in the first place. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bayesian statistics
Hi David, as far as I know there is no such development, however Kevin Van Horn asked half a year ago a similar question: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-March/msg00033.html There is already Probability theory in Isabelle/HOL: http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/HOL-Probability/index.html in the next Isabelle version contains a improved version of this, mostly about infinite products and independent functions. Greetings, Johannes On Sun, 25 Sep 2011, David Blubaugh wrote: Has anyone ever developed theories with Isabelle HOL regarding Bayesian statistics ?? Thanks, David ___ 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
Re: [isabelle-dev] Isabelle_11-Sep-2011
On Fri, 23 Sep 2011, René Thiemann wrote: Dear Makarius, A preliminary test distribution is now available from http://www4.in.tum.de/~wenzelm/test/Isabelle_11-Sep-2011/download.html A preliminary test distribution is now available from http://www4.in.tum.de/~wenzelm/test/Isabelle_20-Sep-2011/download.html the Emacs version of the distribution of 11-Sep (Emacs 23.2) works nicely with Mac OS Lion. However, testing Isabelle_20-Sep-2011 with Emacs 23.3, there seems to be a problem for Mac OS Lion users: Many special characters like == \in, = are not displayed correctly which makes working inconvenient. Under http://cl-informatik.uibk.ac.at/~thiemann/emacs.html I put two small screenshots where one can observe the problem. I don't know what the advantages of 23.3 are, but this display problem is a real disadvantage, so one might consider which version should be shipped in final MacOS distribution 2011-1. This looks bad. I still do not have Lion desktop access to try it myself. It is probably worth filing a report at http://proofgeneral.inf.ed.ac.uk/trac/ Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] back to post-release mode
The main isabelle repository http://isabelle.in.tum.de/repos/isabelle/ is now back to post-release mode, see http://isabelle.in.tum.de/repos/isabelle/rev/20b3377b08d7 This means the flow of changes for the next release, after the current one, can continue. I merely ask to avoid huge upheavals right now, until Isabelle2011-1 is officially shipped (probably mid October) and the release reposity merged back. Makarius ___ 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
