Email Gateway (Aug 22 2022 at 09:48): Email Gateway (Aug 22 2022 at 09:48):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
code_deps eliminates circles internally by collapsing to one node. I
have considerable confidence that it will not expose any problems.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 10:08):From: Dmitriy Traytel <traytel@in.tum.de>
Hi,
I have just introduced the following locale dependencies
locale foo = fixes m :: nat
locale bar = m!: foo m + n!: foo n for m n :: nat
sublocale foo < bar m m by unfold_locales
This works well, even though it is cyclic, and I get the expected
theorems of bar inside of foo.
Now, using the new graph browser in Isabelle2015-RC3, I (and anybody who
will import my theory) cannot look at the locale graph anymore (it just
says "Cyclic graph"). The old browser used to ignore cyclic arrows.
I guess this is what Florian meant by "but cycles make problems here" in
this thread [1], but is there some workaround such as filtering (similar
to what is now available for class_deps)?
Dmitriy
[1]
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg05849.html
Email Gateway (Aug 22 2022 at 10:09):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dmitriy,
I have just introduced the following locale dependencies
locale foo = fixes m :: nat
locale bar = m!: foo m + n!: foo n for m n :: nat
sublocale foo < bar m m by unfold_localesThis works well, even though it is cyclic, and I get the expected
theorems of bar inside of foo.Now, using the new graph browser in Isabelle2015-RC3, I (and anybody who
will import my theory) cannot look at the locale graph anymore (it just
says "Cyclic graph"). The old browser used to ignore cyclic arrows.
yes, this is what bites here.
I guess this is what Florian meant by "but cycles make problems here" in
this thread [1], but is there some workaround such as filtering (similar
to what is now available for class_deps)?
I guess in the short run the best you can do is to replace
Graph_Display.display_graph by Graph_Display.display_graph_old.
If we want to maintain locale_deps seriously, we have to come up with a
different concept.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 10:10):From: Makarius <makarius@sketis.net>
On Thu, 7 May 2015, Florian Haftmann wrote:
Hi Dmitriy,
I have just introduced the following locale dependencies
locale foo = fixes m :: nat
locale bar = m!: foo m + n!: foo n for m n :: nat
sublocale foo < bar m m by unfold_localesThis works well, even though it is cyclic, and I get the expected
theorems of bar inside of foo.Now, using the new graph browser in Isabelle2015-RC3, I (and anybody who
will import my theory) cannot look at the locale graph anymore (it just
says "Cyclic graph"). The old browser used to ignore cyclic arrows.yes, this is what bites here.
The algorithm behind both graph browsers is the same, and specifically for
acyclic graphs. The original paper by Georg Sander (DIMACS GD'94
published 1995) discusses this restriction initially and proposes a simple
preprocessor to allow cycles as well. When Stefan Berghofer implemented
the browser first in 1996, we were discussing this detail and left out the
preprocessor on purpose, because our graphs were always acyclic.
So as far as I can say, the behaviour of the old browser is undefined /
arbitrary / unspecified for cyclic graphs. The new Graphview properly
checks that and shows nothing that an error message.
I guess this is what Florian meant by "but cycles make problems here" in
this thread [1], but is there some workaround such as filtering (similar
to what is now available for class_deps)?I guess in the short run the best you can do is to replace
Graph_Display.display_graph by Graph_Display.display_graph_old.If we want to maintain locale_deps seriously, we have to come up with a
different concept.
The locale_deps command was first advertized in Isabelle2013 (February
2013). Was it actually ever used productively? Trying it in Isabelle/HOL
Main, it merely shows a big mess.
Anyway, for now in
https://bitbucket.org/isabelle_project/isabelle-release/commits/83de10e27007
I've switched locale_deps back to Graph_Display.display_graph_old. It is
a bit depressing, because the new Graphview started out as a locale graph
browser project.
So we have the following situation:
Graph_Display.display_graph_old:
locale_deps
thm_deps
Graph_Display.display_graph:
thy_deps
class_deps
code_deps
Both locale_deps and thm_deps may be considered as never quite finished
experiments, so using the old browser merely emphasizes the bad state.
Hopefully thy_deps, class_deps, code_deps are all in good shape. I've
hade a close look at thy_deps and class_deps recently. Is code_deps
beyond doubt and properly usable?
Makarius
Last updated: Apr 20 2024 at 04:19 UTC