Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
I've just been trying to get the proofs working, not to simplify them or even to understand them. Incidentally, let there be no illusions about people accidentally stumbling into a mixture of sets and predicates. Some of these theories were clearly designed from the ground upwards on the premise that sets and predicates were the same thing. Larry On 23 Aug 2011, at 22:24, Alexander Krauss wrote: Shouldn't one remove quite a bit of duplication first? The classes distributive_complete_lattice and complete_boolean_algebra are now part of HOL (the former as complete_distrib_lattice) (see the FIXME). The set instances for those should be in/go into Florian's HOL repository as well... (but maybe you already did this???) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Dead code smells
Some notes concerning the following recent changes: 082edd97ffe1 huffman comment out dead code to avoid compiler warnings 6f28f96a09bf huffman avoid warnings A priori, warnings are really just warnings, not errors. When Poly/ML acquired this very useful warning for unused identifiers, I did go through all my code and cross-checked if I agree with the compiler. There were typically one of the following cases: (1) There is genuine unused stuff that is better removed altogether. (Maybe 90% of the time.) (2) Certain unused arguments indicate a deeper problem in the code -- it requires some care and understanding how things work exactly to amend this. Removing the offending identifiers merely makes things worse, because semantic unclarities are swept under the carpet. (May happens a few % of the time.) (3) Small named arguments that actually improved readability and uniformity. (Up to 10% of the time.) Here is a trivial example from src/Pure/library.ML: fun fst (x, y) = x; fun snd (x, y) = y; Replacing everything by _ blindly is not really progress in code quality. I have occasionally tried to clean up things like positivstellensatz.ML myself, but failed to do it right without substantial involvement. (Without the latter the preferred style of the original author takes precedence, even if it happens to be suboptimal.) Dead code really starts smelling quickly and should not be introduced at all. Either it is left in and statically checked, or removed from the text. (The history is 100% persistent so interested parties can retrieve old material any time.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
maybe also declare them [no_atp], to avoid sledgehammer-generated proofs that we know are going to break one release later...? Maybe better now, as long as there are real sledgehammer-generated proofs depending on it. 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
[isabelle-dev] Separated heaps for different Isabelle instances [was: get_relmap (no relation map function found for type Set.set)]
Hi Larry, And I'm finding it very difficult to work with two different versions of Isabelle. I need to keep compiling one version or the other in order to run tests. I know that we have ISABELLE_IDENTIFIER to eliminate that problem, but it's empty in both versions. I achieve this by having the following in my ~/.isabelle/etc/settings if [ -z $ISABELLE_IDENTIFIER ] then ISABELLE_OUTPUT=$ISABELLE_HOME/heaps ISABELLE_BROWSER_INFO=$ISABELLE_HOME/browser_info fi For historical reasons my heaps and browser_info reside within the repository, but you can place it where you want; referring to path relative to $ISABELLE_HOME makes it instance-aware, so to speak. (Btw. I give this answer to the dev mailing list since I think it is *extremely* important that we keep the collective knowledge alive how to actually do system development efficiently. Isabelle provides excellent infrastructure for plugging in development tool script etc, which is very helpful if you know about it). Cheers, 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] [isabelle] (Re-)introducing set as a type constructor rather than as mere abbreviation[SEC=UNCLASSIFIED]
I'm starting to have doubts about this entire procedure. I thought the plan was to get these theories (particularly in the AFP) into a state where they no longer dependent on confusing sets with predicates so that they would work with either version of Isabelle. I'm not sure that's possible. I got DataRefinementIBP working with the set-version, but now it doesn't work with the standard version. For one thing, it needs a class declaration for type set, which obviously cannot work with the standard version, but other proofs also fail to work with the standard version. I don't think it's possible to have it both ways. We need to either say we are making this change (and then pushing it through) or not making this change. Having full compatible versions indeed is illusive. But we can aim for the following: * elimination set/pred mixture from specifications and propositions * figure out problems in the infrastructure * cleanup proofs that they are robust enough to be easily translated (in florid style, replace apply-OF-tac-fancyoption-Proofs by robust Isar proofs). The latter is surely needed, especially concerning mem_def; examples can be found in http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2 Recall most of those affected proofs have already adapted in the Isabelle repository to keep this final transition minimal and compact. 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] (Re-)introducing set as a type constructor rather than as mere abbreviation
A proof works only if I insert before it the following: instance set :: (type) complete_boolean_algebra proof qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def Inf_bool_def Sup_bool_def) this is strange because this exact text already appears in the file Complete_Lattice.thy (I refer to Florian's version of HOL), which is imported by Main, which is indirectly imported by Diagram. And just in case I was mistaken on this last point, I modified Diagram to import Main explicitly, just to be sure. This instance declaration is still necessary. print_classes should give sufficient data to find out what is going here. The duplication is the same I was referring to a few days ago: Complete_Lattices.thy and http://afp.hg.sourceforge.net/hgweb/afp/afp/file/dce6fbc4d6c0/thys/DataRefinementIBP/Preliminaries.thy (btw. it took me considerable time to figure out how the class hierarchy for complete lattices should look like, just to see now that somebody else got to the same conclusion independently already). Indeed the classes in DataRefinement are duplication of work now in Complete_Lattice.thy and have already been marked by Brian as such. Logically they are equivalent and can be removed. Hope this helps, 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] Separated heaps for different Isabelle instances [was: get_relmap (no relation map function found for type Set.set)]
This suggestion looks promising. However, my impression is that ISABELLE_OUTPUT specifies where images will be written to. Does it also specify where images (unless a full path is specified) are read from? I often seem to get the wrong image unless I rename them manually, which is obviously not how things should work. This is controlled by ISABELLE_PATH, which according to etc/settings by default is # Heap input locations. ML system identifier is included in lookup. ISABELLE_PATH=$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps I.e. a »heaps« dir in your repository directory is considered implicitly. Different locations can be added in your ~/.isabelle/etc/settings likewise. 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] (Re-)introducing set as a type constructor rather than as mere abbreviation
Hi all, Shouldn't one remove quite a bit of duplication first? The classes distributive_complete_lattice and complete_boolean_algebra are now part of HOL (the former as complete_distrib_lattice) (see the FIXME). The set instances for those should be in/go into Florian's HOL repository as well... (but maybe you already did this???) concerning Complete_Lattice, of course: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2#l1.7 Can you send me a bundle of your changes, so that I can put them on the web for people to look at? - hg ci # commit your changes locally - hg bundle SOME_FILENAME http://afp.hg.sourceforge.net/hgweb/afp/afp/ - send me the file SOME_FILENAME, created in the previous step The second command will produce a file which contains all your changesets that are not in the central afp repos (i.e., your new changes). I confess our infrastructure at the moment is not that good. When there is time, I will allocate an afp_set repository beside the isabelle_set one. I was driven crazy some months ago when I attempted in vain to enable push access. I don't even know what the problem was (authentication, web server configuration, encrpytion) – maybe I wasn't even able to figure out. If someone of the TUM guys knows better, tell me. So the tool of choice would be that each involved in that story to set up his own repositories and publish them by HTTP. Then we can pull each other's changesets. Are there any obstacles? Cheers, 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
