Re: [isabelle-dev] Consolidation of manual naming
When inspecting the ROOT file I saw the session name for »ZF-Logics« and gave that some authority. Maybe it is best if I will move on »ZF_Logics« etc. in yet another iteration to get rid of these historic names. At least that made the confusion apparent. I still don't understand what the confusion actually is. These things are really old, especially the logics manuals, which used to be just one latex document a long time ago. It is not always possible to have immediately obvious canonical names for everything -- there are often conflicting side-conditions etc. Being in the role of an occasional bypasser in src/Doc, the lack of any apparent »standard scheme« to glimpse from produces more diversion over time. E.g. I myself attributed some official status to the session name »ZF-Logics« which was just an historical accident. You might call this an instance of the broken-window syndrome. 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] Consolidation of manual naming
I consider this twofold renaming of directories pointless, and as you know, it required a twofold update in some other theories of mine. I guess I should have stated my displeasure earlier but thought that since Makarius had already stated he didn't even see the problem, this would discourage you. Obviously I underestimated you ;-) Nuff said. Tobias On 11/04/2014 15:54, Florian Haftmann wrote: When inspecting the ROOT file I saw the session name for »ZF-Logics« and gave that some authority. Maybe it is best if I will move on »ZF_Logics« etc. in yet another iteration to get rid of these historic names. At least that made the confusion apparent. I still don't understand what the confusion actually is. These things are really old, especially the logics manuals, which used to be just one latex document a long time ago. It is not always possible to have immediately obvious canonical names for everything -- there are often conflicting side-conditions etc. Being in the role of an occasional bypasser in src/Doc, the lack of any apparent »standard scheme« to glimpse from produces more diversion over time. E.g. I myself attributed some official status to the session name »ZF-Logics« which was just an historical accident. You might call this an instance of the broken-window syndrome. 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
Re: [isabelle-dev] Consolidation of manual naming
On Mon, 7 Apr 2014, Makarius wrote: Getting acquainted with Isabelle/Scala is definitely a good thing. The isabelle_scala_script wrapper makes it easy to get started without interference of the Pure.jar build process. In this particular case I've accidentally done the work already, when passing by some other doc related details. See bc61161a5bd0, which may also serve here is mini-tutorial how to convert a shell script into some Isabelle/Scala function. Maybe you are interested to see how your Isabelle/ML operations for tmp dirs (with rm_tree) now look in Isabelle/Scala: http://isabelle.in.tum.de/repos/isabelle/annotate/57b5c8db55f1/src/Pure/System/isabelle_system.scala#l398 Thanks to the Java 7 Files module, it is now possible to do it without rm -r -f in an external process. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Consolidation of manual naming
On Mon, 7 Apr 2014, Florian Haftmann wrote: Nevertheless I still think its a good idea to spend half an hour to establish a more strict name correspondance while keeping the (lowercase) document names stable, e.g. foo-bar -:- Foo_Bar I now see b266e7a86485 with foo-bar -:- Foo-Bar. It is still unclear to me what the actual confusion was, and what is the improvement. A - within a session name is obsolete for a long time -- it is in conflict with session-qualified theory names and plain long_id token syntax. (That is not very relevant for Doc sessions, though.) When inspecting the ROOT file I saw the session name for »ZF-Logics« and gave that some authority. Maybe it is best if I will move on »ZF_Logics« etc. in yet another iteration to get rid of these historic names. At least that made the confusion apparent. I still don't understand what the confusion actually is. These things are really old, especially the logics manuals, which used to be just one latex document a long time ago. It is not always possible to have immediately obvious canonical names for everything -- there are often conflicting side-conditions etc. We do have a tradition to get things right eventually, but for that there needs to be a clear direction, and some level of significance for a change to be considered: it needs 2-3 good reasons, not just half a reason. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Consolidation of manual naming
Maybe it is best if I will move on »ZF_Logics« etc. in yet another iteration to get rid of these historic names. At least that made the confusion apparent. See now http://isabelle.in.tum.de/reports/Isabelle/rev/856492b0f755 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] Consolidation of manual naming
On Thu, 3 Apr 2014, Florian Haftmann wrote: Otherwise any reform of this little aministrative problem of Isabelle repository versions is one of the build_doc command line: there is no need to specify the session here, it could just name the document_variant instead (but that would mean to rewrite the shell script in Isabelle/Scala, where this information is available). Maybe at some time I would attempt such a rewrite as small Scala exercise. Getting acquainted with Isabelle/Scala is definitely a good thing. The isabelle_scala_script wrapper makes it easy to get started without interference of the Pure.jar build process. In this particular case I've accidentally done the work already, when passing by some other doc related details. See bc61161a5bd0, which may also serve here is mini-tutorial how to convert a shell script into some Isabelle/Scala function. Nevertheless I still think its a good idea to spend half an hour to establish a more strict name correspondance while keeping the (lowercase) document names stable, e.g. foo-bar -:- Foo_Bar I now see b266e7a86485 with foo-bar -:- Foo-Bar. It is still unclear to me what the actual confusion was, and what is the improvement. A - within a session name is obsolete for a long time -- it is in conflict with session-qualified theory names and plain long_id token syntax. (That is not very relevant for Doc sessions, though.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Consolidation of manual naming
Nevertheless I still think its a good idea to spend half an hour to establish a more strict name correspondance while keeping the (lowercase) document names stable, e.g. foo-bar -:- Foo_Bar I now see b266e7a86485 with foo-bar -:- Foo-Bar. It is still unclear to me what the actual confusion was, and what is the improvement. A - within a session name is obsolete for a long time -- it is in conflict with session-qualified theory names and plain long_id token syntax. (That is not very relevant for Doc sessions, though.) When inspecting the ROOT file I saw the session name for »ZF-Logics« and gave that some authority. Maybe it is best if I will move on »ZF_Logics« etc. in yet another iteration to get rid of these historic names. At least that made the confusion apparent. 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] Consolidation of manual naming
Otherwise any reform of this little aministrative problem of Isabelle repository versions is one of the build_doc command line: there is no need to specify the session here, it could just name the document_variant instead (but that would mean to rewrite the shell script in Isabelle/Scala, where this information is available). Maybe at some time I would attempt such a rewrite as small Scala exercise. Nevertheless I still think its a good idea to spend half an hour to establish a more strict name correspondance while keeping the (lowercase) document names stable, e.g. foo-bar -:- Foo_Bar etc. 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] Consolidation of manual naming
On Wed, 26 Mar 2014, Florian Haftmann wrote: since ancient times there is a glitch in the naming of manuals vs. their originating sessions, e.g. isar-ref vs. IsarRef. Would it be worth an effort to consolidate this? I regularly get confused about that. This is one of these recurrent (low priority) questions from distant past. Just a few days ago I was again thinking of it, but did not get the right idea where to move. The short doc identifiers like isar-ref have a semi-formal status; they are relevant to isabelle doc, the Isabelle/jEdit Documentation panel, and are published as global URLs (already for decades). Changing that would cause a lot of confusion. Session names cannot be changed either without violating increasingly important naming conventions: capitalized words usually separated by underscore. Renaming IsarRef to Isar_Ref would make it look more modern, but still disagree with the document name isar-ref. (Note that a - within a session name is a legacy feature for many years alread.) So what is actually the problem here? The main practical situation where this connection of divergent names needs to be resolved is isabelle build_doc. That could be smarter, or actually somehow be automatic as part of the document viewer. But we are talking about the Isabelle repository here, not a proper release. I often just do isabelle build_doc -a -j4 before viewing anything within the repository. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Consolidation of manual naming
On Fri, 28 Mar 2014, Makarius wrote: So what is actually the problem here? The main practical situation where this connection of divergent names needs to be resolved is isabelle build_doc. That could be smarter, or actually somehow be automatic as part of the document viewer. But we are talking about the Isabelle repository here, not a proper release. If the confusion was caused by other reasons than the command line of build_doc, you should put them forward here. Otherwise any reform of this little aministrative problem of Isabelle repository versions is one of the build_doc command line: there is no need to specify the session here, it could just name the document_variant instead (but that would mean to rewrite the shell script in Isabelle/Scala, where this information is available). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Consolidation of manual naming
Hi, since ancient times there is a glitch in the naming of manuals vs. their originating sessions, e.g. isar-ref vs. IsarRef. Would it be worth an effort to consolidate this? I regularly get confused about that. 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] Consolidation of manual naming
+1 Fortunately, nowadays the list of manuals shown in jEdit is very helpful here. Am Mittwoch, den 26.03.2014, 22:07 +0100 schrieb Florian Haftmann: Hi, since ancient times there is a glitch in the naming of manuals vs. their originating sessions, e.g. isar-ref vs. IsarRef. Would it be worth an effort to consolidate this? I regularly get confused about that. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
