Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)
> On 14.10.2015, at 05:56, Makarius wrote: > > On Tue, 13 Oct 2015, Larry Paulson wrote: > >> The only restriction on an unsigned application is that the first time you >> open it, you need to select the “open” menu item rather than simply >> double-clicking on some file. Then you need to confirm that you want the >> application to open. > > In theory it should be like that. In practice, the app did not come up in > the first "open" invocation: after a long timeout it died. > > Current operating systems are very hostile to applications that are not yet > known to the NSA. I’m pretty sure that Isabelle is well known to the NSA ;-) Cheers, Gerwin 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
Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)
On Tue, 13 Oct 2015, Larry Paulson wrote: The only restriction on an unsigned application is that the first time you open it, you need to select the “open” menu item rather than simply double-clicking on some file. Then you need to confirm that you want the application to open. In theory it should be like that. In practice, the app did not come up in the first "open" invocation: after a long timeout it died. Current operating systems are very hostile to applications that are not yet known to the NSA. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Explicit option "open" for code_reflect
Hi Florian, Between Isabelle 2014 and 2015, the option "open" appeared for the command export_code, and by default the reflection minimizes the exported code. Would it be acceptable for code_reflect to also have a similar option "open"? As a draft example, here is a list of modifications needed for implementing the option "open": afp-devel/thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_runtime.thy We basically abstract the parameter "false" of Code_Target.produce_code, and propagate this information to the parsing step. Cheers, Frédéric ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)
I have also upgraded and I find that everything still works the same as before. The only restriction on an unsigned application is that the first time you open it, you need to select the “open” menu item rather than simply double-clicking on some file. Then you need to confirm that you want the application to open. It would certainly be nice to be able to open a theory file simply by double-clicking on it. A long time ago, I had this working by some low level hack, but I haven’t been able to reproduce it. Larry > On 13 Oct 2015, at 15:32, Makarius wrote: > > Apple has released OS X 10.11 (El Capitan) recently. > > I have updated my test machine some days ago and made a few sanity checks. So > far the situation looks good concerning Isabelle. A test version is available > here: http://www4.in.tum.de/~wenzelm/test/Isabelle_07-Oct-2015 > > Are there further observations from full-time users of Mac OS X? > > > We shall probably also shift our base-line of supported OS X versions from > 10.7 (Lion) to 10.8 (Mountain Lion). See also > http://isabelle.in.tum.de/repos/isabelle/file/3c69ea85f8dd/Admin/PLATFORMS#l36 > > > Another note on the OS X "app": I've recently experimented with a current > fork of the JavaAppLauncher https://bitbucket.org/infinitekind/appbundler > that also supports file associations. It somehow worked, but only after one > failed attempt to start the application for the very first time, probably due > to the lack of signed application. > > In http://isabelle.in.tum.de/repos/isabelle/rev/9b4843250e1c I have reverted > this experiment -- users need to be able to start-up properly after a fresh > download of Isabelle. > > If there is anybody who knows how to get this right, and maybe even has > official OS X developer credentials for signed application, we could try > again with the new launcher. > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Mac OS X 10.11 (El Capitan)
Apple has released OS X 10.11 (El Capitan) recently. I have updated my test machine some days ago and made a few sanity checks. So far the situation looks good concerning Isabelle. A test version is available here: http://www4.in.tum.de/~wenzelm/test/Isabelle_07-Oct-2015 Are there further observations from full-time users of Mac OS X? We shall probably also shift our base-line of supported OS X versions from 10.7 (Lion) to 10.8 (Mountain Lion). See also http://isabelle.in.tum.de/repos/isabelle/file/3c69ea85f8dd/Admin/PLATFORMS#l36 Another note on the OS X "app": I've recently experimented with a current fork of the JavaAppLauncher https://bitbucket.org/infinitekind/appbundler that also supports file associations. It somehow worked, but only after one failed attempt to start the application for the very first time, probably due to the lack of signed application. In http://isabelle.in.tum.de/repos/isabelle/rev/9b4843250e1c I have reverted this experiment -- users need to be able to start-up properly after a fresh download of Isabelle. If there is anybody who knows how to get this right, and maybe even has official OS X developer credentials for signed application, we could try again with the new launcher. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Future of permanent_interpretation
Recently in private discussion there was the question what the supposed future of permanent_interpretation is supposed to be. It looks as follows: Step 1) * Put »permanent_interpretation« into Pure directly. Step 2) * Careful revisiting of the documentation to emphasize the presence of permanent_interpretation. * »permanent_interpretation« as leading construct in the distribution and the AFP as far as appropriate Step 3) * Discontinue theory-global »interpretation«, which then is just a degenerated form of »permanent_interpretation«. * Discontinue locale-level »sublocale«, which then is just a degenerated form of »permanent_interpretation«. There will definitely be one release to breath between step 2 and step 3. Cheers, Florian -- 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] Definite name for case combinator on products [was: NEWS]
In fb95d06fb21f, find my attempt to reach a stable status again after opening too many loose ends. * The combinator is named »case_prod« uniformly; no aliasses remain, in order not to obfuscate the now reached state of uniformity. * The most popular theorem names with »split« are retained (see end of HOL/Product_Type.thy); there could be room for further cleanup there, e. g. getting rid of the alias »split« and reducing the variants regarding eta-contraction further. But I did not attempt this at this moment. * Some discontinuities introduced unconsciously in the past (e. g. wrong trigger terms for simprocs) have been repaired silently. * I encountered a borderline case of printing and just reinstallated a print translation believed to be totally obsolete; my conclusion at the moment is that it is not feasible to refine anything regarding the parsing / printing of products without reconsidering / remoulding the eta-expansion issue. This is the state of affairs. Please report any remaning suspicious behaviour. Florian Am 22.09.2015 um 16:20 schrieb Florian Haftmann: > So, the direction is going towards prod_case. > > If this is settled, the consequences are: > * Abbreviation »uncurry« will disappear again. > * Abbreviation »split« will disappear finally (using the distribution > and AFP as indicator whether this is »now« or »later«). > * Theorem names contain »prod_case« instead of »split«; the latter are > retained as aliasses, but documentation etc. is updated to prefer the > first version. > * There is no way to have something like »curry (uncurry f) = f« > printed; entering »curry (prod_case f) = f« prints as »curry (λ(x, y). f > x y) = f« by default. > > Any headache with this? > > Florian > > Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel: >> Hi Florian, >> >> while I very much welcome the simplified printing rules and your effort >> of unifying case_prod/split, I am not sure if adding a third alternative >> name is the way to go. The situation reminds me of the one depicted in [1]. >> >> Clearly, case_prod is the "right" name from the perspective of the >> (co)datatype package. >> >> Dmitriy >> >> [1] https://xkcd.com/927/ >> >> On 10.09.2015 12:02, Florian Haftmann wrote: >>> * Combinator to represent case distinction on products is named >>> "uncurry", with "split" and "prod_case" retained as input abbreviations. >>> >>> Partially applied occurences of "uncurry" with eta-contracted body >>> terms are not printed with special syntax, to provide a compact >>> notation and getting rid of a special-case print translation. >>> >>> Hence, the "uncurry"-expressions are printed the following way: >>> >>> a) fully applied "uncurry f p": explicit case-expression; >>> >>> b) partially applied with explicit double lambda abstraction in >>> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; >>> >>> c) partially applied with eta-contracted body term "uncurry f": >>> no special syntax, plain "uncurry" combinator. >>> This aims for maximum readability in a given subterm. >>> INCOMPATIBILITY. >>> >>> This refers to e6b1236f9b3d. >>> >>> This schema emerged after some experimentation and seems to be a >>> convenient compromise. The longer perspective is to overcome the >>> case_prod/split schism eventually and consolidate theorem names accordingly. >>> >>> The next step after this initial cleanup is to tackle the »let (a, b) = >>> … in …« issue. >>> >>> Florian >>> >>> >>> >>> ___ >>> 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 > -- 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
