Re: [isabelle] Visualization of partial orders in Isabelle/HOL; use of external tools in the AFP entries



Dear All,

This is a partial reply to one of my own old questions on the list:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-December/msg00058.html.
I thought that it may be worth making an attempt to resurrect this thread
in light of a recent paper by Clemens Ballarin for the Isabelle Workshop:
https://files.sketis.net/Isabelle_Workshop_2020/Isabelle_2020_paper_2.pdf.
This paper provides a positive answer to Question 2 from the thread that I
started. Thus, once again, I would like to thank the author (indeed, this
is the second time a publication from Clemens Ballarin provides an answer
to one of my questions on the list:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-April/msg00077.html
).

Undeniably, I am very interested in whether there exist any active projects
related to the extraction of diagrams from theories or auto-generation of
theories from diagrams (to the point of designing my own prototype for the
extraction of diagrams for one particular application area, not directly
related to locales), as well as finding the answers to Questions 1 and 3
from the aforementioned thread. Therefore, I would be very pleased to
receive any comments in relation to the aforementioned matters.

Kind Regards,
Mikhail Chekhov


> Dear All,
> I would like to ask several questions with regard to the availability of
> tools for the visualization of orders based on theorems stated in
> Isabelle/HOL and certain other related questions:
>    1. Are there any tools already available for the visualization of orders
>    or relationships between predicates (apart from the locale_deps and
>    class_deps)? Are there any ongoing efforts dedicated to the development
> of
>    such tools?
>    2. Is it possible to extract (with ease) arbitrary subsets of the
>    diagrams produced by class_deps/locale_deps and add them to the formal
>    proof documents?
>    3. I would like to understand what is the policy on the inclusion of
>    external tools in the build process for the submission of articles to
> the
>    AFP. In particular, I would like to understand if it would be acceptable
>    for the build process to call any commands associated with graphviz.
> -----------------
> Background
> I sketched a graphviz-based snippet for the visualization of certain types
> of partial orders in the form of the Hasse-like diagrams (more precisely,
> at the moment, I allow the edges shown in such diagrams to form an
> arbitrary subset of the edges of the traditional Hasse diagram for a given
> ordered set) from theorems stated in Isabelle/HOL for a particular
> application. I am thinking about whether it is worth taking this
> development one step further and create a small package from it.
> Unfortunately, it relies on graphviz and I am not certain whether this
> could be allowed in the AFP submissions. Furthermore, before taking this
> tool with any degree of seriousness, I would like to understand if anything
> similar already exists or is being developed. I attached a couple of
> screenshots taken from the formal proof documents amended with the diagrams
> created by the (sketched) tool for a reference.
> Thank you,
> Mikhail Chekhov



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.