[isabelle-dev] Mac App
Recent Isabelle applications for Mac don't seem to recognise the .thy filename extension, and Mac OS is unwilling to assign them as the default application for theory files. I believe that the fix is as follows: (1), to use the attached version of Info.plist and (2), to include the attached icon file (for theory files, which is different from the application icon) in the Resources folder. Larry Info.plist Description: Binary data inline: Isabelle theory.icns___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Comment in Efficient_Nat
On 07/22/2012 10:29 AM, Florian Haftmann wrote:
text {*
FIXME -- Evaluation with @{text Quickcheck_Narrowing} does not work, as
@{text code_module} is very aggressive leading to bad Haskell code.
Therefore, we simply deactivate the narrowing-based quickcheck from here on.
*}
I do not unserstand this. What does code_module mean here? And why
is it aggressive?
I do recall not the exact details anymore. But I believe that the setup
with code_modulename caused the narrowing-based quickcheck to produce
non-executable code.
(If I remember correctly, it produced one file with multiple modules,
which is not valid Haskell code. code_modulename was just to aggressive.)
If you are looking into this and would fix it, that would be great. We
can discuss the details offline.
Probably related, with the changeset 6efff142bb54, the narrowing-based
quickcheck fails to generate valid code.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Mac App
Thanks from all information! By “today do you mean literally today, or the 2012 release? I'm puzzled that you have two things released today. I just made the two small changes mentioned in my e-mail, and they allow drag-and-drop. I don't see document icons working yet, which is puzzling, because they worked with the old application. I didn't do this with platypus. I just did it. I looked up somewhere how you get icons for documents and how you associate them with applications. The issue of multiple applications winning is a classic one on any Mac, and users should be able to know how to deal with that. Larry On 23 Jul 2012, at 17:41, Makarius wrote: On Mon, 23 Jul 2012, Lawrence Paulson wrote: Recent Isabelle applications for Mac don't seem to recognise the .thy filename extension, and Mac OS is unwilling to assign them as the default application for theory files. I believe that the fix is as follows: (1), to use the attached version of Info.plist and (2), to include the attached icon file (for theory files, which is different from the application icon) in the Resources folder. This already has a longer history. Around 2008 I had picked up your experimental .app to include it into the official Isabelle distribution, in a manner that works for most users. See Admin/MacOS/App1 in current Isabelle/4ad6182d5bb9. The README and mk define a documented and repeatabke procedure to create Isabelle.app, without hand-editing. Some notes on the history of this: (1) http://isabelle.in.tum.de/repos/isabelle/rev/de5b29c25af9 (2008) first systematic attempt based on your initial experiments (2) http://isabelle.in.tum.de/repos/isabelle/rev/ca28610a0e7e (2008) attempt to support .thy file type via AppHack 1.1 (3) http://isabelle.in.tum.de/repos/isabelle/rev/9343d4b7c5bf (2009) give up file type / dropability for now -- does not work reliably (4) http://isabelle.in.tum.de/repos/isabelle/rev/6d9c43f51e60 (today) updated to Platypus 4.7 (5) http://isabelle.in.tum.de/repos/isabelle/rev/4ad6182d5bb9 (today) try droppable application using Platypus functionality -- in contrast to earlier AppHack (cf. 9343d4b7c5bf) The problems leading to (3) were manyfold: unclarity which Isabelle application wins when many of them are on the system (which happens routinely); unclarity what happens due to nested applications (Platypus wrapper, Emacs or Java Runtime etc.) Current (5) is an experiment to see what it does. As far as I can tell on the spot, it allows to drop .thy files on the application icon, e.g. in the finder or dock. Maybe you find out more, so that we can make some actual progress with production quality .app bundling. (At some later stage one might try to give up Platypus, and make the thing a native application based on the JVM app wrapper, in the relative sense of native for Java on Mac OS -- things are again changing with Java 7.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation with definitions [was Locale interpretation with mixins]
Hi Florian,
I appreciate that you now follow my reasoning that changes to the
locales core machinery are not necessary for getting this
functionality. However, I don't think we should change how locale
expressions work. Currently we have:
locale loc = fixes x assumes about_x: x = x
interpretation const: loc less_eq by unfold_locales (rule refl)
thm const.about_x -- {* op \le = op \le *}
interpretation var: loc less_eq for less_eq by unfold_locales (rule refl)
thm var.about_x -- {* ?less_eq = ?less_eq *}
Also, I'm afraid I fail to understand the difference between 'where x
= t' and 'where x is t'.
Clemens
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
Hi Clemens, hi Makarius,
let me continue concerning syntax:
The current syntax in Tools/interpretation_with_defs.ML is just a proof
of concept:
interpretation L inst
where
bar = t
defines f is foo
A much better idea could be to give the new defs in a for-clause:
interpretation L inst
for f :: T
where
foo = f
bar = t
where the implicit definitions (f) are mentioned in the for-clause.
One could also think about hiding away the full generality of a) from
the user (for which there might be good reasons) and have something like
interpretation L inst
for f :: T
where
f is foo
t is bar
Or the where clause could be integrated completely into the locale
expression using named syntax:
interpretation L (| f := foo, t := bar |)
for f :: T
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Mac App
On Mon, 23 Jul 2012, Lawrence Paulson wrote: By “today do you mean literally today, or the 2012 release? I'm puzzled that you have two things released today. I have merely pushed two changesets: (4) http://isabelle.in.tum.de/repos/isabelle/rev/6d9c43f51e60 (today) (5) http://isabelle.in.tum.de/repos/isabelle/rev/4ad6182d5bb9 (today) For extra convenience I have added the full URL and some hint about the dates. The full information is already given by the changeset ids (abbreviated SHA1 keys), so with the Mercurial front-end of your choice you can retrieve all these details, and more. The above merely gives you the updated Admin/MacOS/App1/README and mk script to repeat the process yourself. I just made the two small changes mentioned in my e-mail, and they allow drag-and-drop. I don't see document icons working yet, which is puzzling, because they worked with the old application. Here are your edits after according to diff -w: keyCFBundleDocumentTypes/key array dict keyCFBundleTypeExtensions/key array stringthy/string /array keyCFBundleTypeIconFile/key stringIsabelle theory.icns/string keyCFBundleTypeName/key stringIsabelle theory/string keyCFBundleTypeRole/key stringEditor/string /dict /array I didn't do this with platypus. I just did it. The Info.plist edited here was generated by Platypus 4.0. The main thing is the executable application wrapper of Platypus, and the plist needs to correspond to that. After updating to Platypus 4.7 I've got a different Info.plist, which was not very surprising. Editing generated files only works one-shot, not for long-term maintenance. I looked up somewhere how you get icons for documents and how you associate them with applications. Do you have some concrete links with explanations how this works? The issue of multiple applications winning is a classic one on any Mac, and users should be able to know how to deal with that. Our situation is not quite classic: The problems leading to (3) were manyfold: unclarity which Isabelle application wins when many of them are on the system (which happens routinely); unclarity what happens due to nested applications (Platypus wrapper, Emacs or Java Runtime etc.) Where nested means that the shell script invokes another application, which was some Emacs.app in 2009 when I disabled the attempt with the document--application connection at that time, see again Isabelle/9343d4b7c5bf with the Mercurial changeset browser of your choice. BTW, since you are now one of the Proof General maintainers, you may have to understand its integration with Isabelle.app, and potentially find ways to avoid some of its oddities caused by Isabelle.app invoking Emacs.app via a shell script. For Isabelle/jEdit there might be ways in the future to avoid all that, running more directly some .jar application. But that reform is not imminent. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
