[isabelle-dev] Typerep again
Dear all, I have a theory development which used to work not a long time ago. I am now trying to include it into the distribution. At some point I can not merge the theories and get: *** Clash of specifications Permutations.typerep_^_inst.typerep_^_def and Misc.typerep_^_inst.typerep_^_def for constant Typerep.typerep_class.typerep *** At command theory. Since an etiologic solution does not seem to exist, can you give a way to come around these situations temporarily. They just cost time and nerves... I would be happy with the ugliest hack. Amine.
[isabelle-dev] Typerep again
I've moved things up (although this is really artificial). Misc imports Complex_Main anyway, and I made Permutations import Main, the problem persists. Florian Haftmann wrote: Hi Amine, I have a theory development which used to work not a long time ago. I am now trying to include it into the distribution. At some point I can not merge the theories and get: *** Clash of specifications Permutations.typerep_^_inst.typerep_^_def and Misc.typerep_^_inst.typerep_^_def for constant Typerep.typerep_class.typerep *** At command theory. is it possible to make both Permutations and Misc to inherit from Main? Florian
[isabelle-dev] Typerep again
Can you provide me with a theory graph of Permutations and Misc? (Isar command thy_graph, export to ps/pdf)? Florian Amine Chaieb schrieb: I've moved things up (although this is really artificial). Misc imports Complex_Main anyway, and I made Permutations import Main, the problem persists. Florian Haftmann wrote: Hi Amine, I have a theory development which used to work not a long time ago. I am now trying to include it into the distribution. At some point I can not merge the theories and get: *** Clash of specifications Permutations.typerep_^_inst.typerep_^_def and Misc.typerep_^_inst.typerep_^_def for constant Typerep.typerep_class.typerep *** At command theory. is it possible to make both Permutations and Misc to inherit from Main? Florian ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -- next part -- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/0e23d8a6/attachment.pgp
[isabelle-dev] Typerep again
Do you mean thy_deps? It's not working on my machine. Can you do cvs -d haftmann at cvsbroy.informatik.tu-muenchen.de:/usr/wiss/chaieb/.repos co work/Lib The files are then under Multivariate. Amine. PS: Please forgive for still using cvs, but I am applying the first commandment of Computer science. Florian Haftmann wrote: Can you provide me with a theory graph of Permutations and Misc? (Isar command thy_graph, export to ps/pdf)? Florian Amine Chaieb schrieb: I've moved things up (although this is really artificial). Misc imports Complex_Main anyway, and I made Permutations import Main, the problem persists. Florian Haftmann wrote: Hi Amine, I have a theory development which used to work not a long time ago. I am now trying to include it into the distribution. At some point I can not merge the theories and get: *** Clash of specifications Permutations.typerep_^_inst.typerep_^_def and Misc.typerep_^_inst.typerep_^_def for constant Typerep.typerep_class.typerep *** At command theory. is it possible to make both Permutations and Misc to inherit from Main? Florian ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Typerep again
Amine Chaieb schrieb: Do you mean thy_deps? It's not working on my machine. Yes, thy_deps of course (sorry for the slip). But thy doesn't it work? cd lib/browser make should do the job... Florian Can you do cvs -d haftmann at cvsbroy.informatik.tu-muenchen.de:/usr/wiss/chaieb/.repos co work/Lib The files are then under Multivariate. Amine. PS: Please forgive for still using cvs, but I am applying the first commandment of Computer science. Florian Haftmann wrote: Can you provide me with a theory graph of Permutations and Misc? (Isar command thy_graph, export to ps/pdf)? Florian Amine Chaieb schrieb: I've moved things up (although this is really artificial). Misc imports Complex_Main anyway, and I made Permutations import Main, the problem persists. Florian Haftmann wrote: Hi Amine, I have a theory development which used to work not a long time ago. I am now trying to include it into the distribution. At some point I can not merge the theories and get: *** Clash of specifications Permutations.typerep_^_inst.typerep_^_def and Misc.typerep_^_inst.typerep_^_def for constant Typerep.typerep_class.typerep *** At command theory. is it possible to make both Permutations and Misc to inherit from Main? Florian ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -- next part -- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/016553a4/attachment-0001.pgp
[isabelle-dev] Typerep again
Florian Haftmann wrote: Amine Chaieb schrieb: Do you mean thy_deps? It's not working on my machine. Yes, thy_deps of course (sorry for the slip). But thy doesn't it work? cd lib/browser make should do the job... Florian Can you do cvs -d haftmann at cvsbroy.informatik.tu-muenchen.de:/usr/wiss/chaieb/.repos co work/Lib The files are then under Multivariate. Amine. PS: Please forgive for still using cvs, but I am applying the first commandment of Computer science. Florian Haftmann wrote: Can you provide me with a theory graph of Permutations and Misc? (Isar command thy_graph, export to ps/pdf)? Florian Amine Chaieb schrieb: I've moved things up (although this is really artificial). Misc imports Complex_Main anyway, and I made Permutations import Main, the problem persists. Florian Haftmann wrote: Hi Amine, I have a theory development which used to work not a long time ago. I am now trying to include it into the distribution. At some point I can not merge the theories and get: *** Clash of specifications Permutations.typerep_^_inst.typerep_^_def and Misc.typerep_^_inst.typerep_^_def for constant Typerep.typerep_class.typerep *** At command theory. is it possible to make both Permutations and Misc to inherit from Main? Florian ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- next part -- A non-text attachment was scrubbed... Name: Misc Type: video/x-flv Size: 914 bytes Desc: not available URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/7edfb161/attachment.flv -- next part -- A non-text attachment was scrubbed... Name: permutations Type: video/x-flv Size: 715 bytes Desc: not available URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/7edfb161/attachment-0001.flv
[isabelle-dev] Typerep again
OK Florian Haftmann wrote: I have to bother you further: it is necessary to unfold the [HOL] node in the graph (by clicking on it) because we need to inspect the internal structure of the HOL theories. Florian Amine Chaieb schrieb: Florian Haftmann wrote: Amine Chaieb schrieb: Do you mean thy_deps? It's not working on my machine. Yes, thy_deps of course (sorry for the slip). But thy doesn't it work? cd lib/browser make should do the job... Florian Can you do cvs -d haftmann at cvsbroy.informatik.tu-muenchen.de:/usr/wiss/chaieb/.repos co work/Lib The files are then under Multivariate. Amine. PS: Please forgive for still using cvs, but I am applying the first commandment of Computer science. Florian Haftmann wrote: Can you provide me with a theory graph of Permutations and Misc? (Isar command thy_graph, export to ps/pdf)? Florian Amine Chaieb schrieb: I've moved things up (although this is really artificial). Misc imports Complex_Main anyway, and I made Permutations import Main, the problem persists. Florian Haftmann wrote: Hi Amine, I have a theory development which used to work not a long time ago. I am now trying to include it into the distribution. At some point I can not merge the theories and get: *** Clash of specifications Permutations.typerep_^_inst.typerep_^_def and Misc.typerep_^_inst.typerep_^_def for constant Typerep.typerep_class.typerep *** At command theory. is it possible to make both Permutations and Misc to inherit from Main? Florian ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- next part -- A non-text attachment was scrubbed... Name: permutations Type: video/x-flv Size: 7248 bytes Desc: not available URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/9148bfd9/attachment-0002.flv -- next part -- A non-text attachment was scrubbed... Name: Misc Type: video/x-flv Size: 13179 bytes Desc: not available URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/9148bfd9/attachment-0003.flv
[isabelle-dev] Typerep again
OK, seems like you have to change the following: a) add Fact to the imports of Plain b) add Main to the imports of Infinite_Set and to the imports of Finite_Cartesian_Products Our current policy is the Plain, Main and Complex_Main are either ancestors or descendants of any theory. Hope this helps. If problems of this kind persist or reoccur, feel free to send thy_deps without any further comment. Florian -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -- next part -- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/a0cd5eca/attachment.pgp
[isabelle-dev] Typerep again
and the fishing rules... Our current policy is that Plain, Main and Complex_Main are either ancestors or descendants of any theory. But feel free to ask if this is still obscure. This rule does not tell me anything since it is trivally satisfied by any connected graph containing Plain, Main and Complex_Main. Do you mean that in the imports section of any theory one of the words Plain, Main or complex Main should appear? Can you give a precise description of what happens and how we should circumvent these problems. I completely disagree with a rule that obliges to import from a higher theory than necessary. This is just not natural. If this mechanism is so important in HOL then it should be either clarified to the developers and users or it should be done in a manner not be noticed in a negative way. Amine
[isabelle-dev] Typerep again
Our current policy is that Plain, Main (and Complex_Main) are either ancestors or descendants of any theory. This rule does not tell me anything since it is trivally satisfied by any connected graph containing Plain, Main and Complex_Main. The rule rules out the following situation: A / \ B Main \ / C Here B is neither ancestor or descendant of Main, likewise the other way round. But to stick to the problem itself first (by example from an earlier discussion): (*) guess you are in the following thygraph situation: Typrep Real | / \ | |/\| Complex_Main FPS \ / \/ \ / Foo Real defines type real, Typerep class typerep (;-)). Then both in Complex_Main and FPS and instance for typerep on type real is generated automatically (thanks to generic interpretation), which clash on merge into theory Foo. The solution is too arrange that there is only one meeting point of Typrep and Real in the thygraph. Generally, each time such a typerep clash occurs, you can eliminate it by finding a suitable meeting point. Our current policy is that Plain, Main (and Complex_Main) are either ancestors or descendants of any theory. The point here is that parallelized proofs scale better if a huge theory development does not contain to many merges. To reduce their number, it is better to merge theories quite frequently. This has recently be done, by simply asserting that for each HOL theory holds: * Plain is either an ancestor or descendant of any HOL theory. * Main is either an ancestor or descendant of any HOL theory. This gives funny wasp-waists in the thy graph. The policy also avoids the typerep problem since if any theory which is not part of Main imports Main, the situation (*) above does not occur. As a kind of stylized comment, this technical imports of Plain and Main are appended to the import list rather then prepended, but this is a matter of taste. Hope this helps Florian -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -- next part -- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/af48875d/attachment-0001.pgp
[isabelle-dev] problems with the class-package
Dear all, Florian Haftmann wrote: sorry for the inconvenience. Currently there is major upheaval going on in the locale/class area. Im working hard on solving the remaining problems. I would like to hear of any problems that are due to the new locales implementation. So far, I have not received any messages, but I have seen that modifications to fairly intricate parts were made. Cheers, Clemens
