Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] a question about Build/export_theory.scala

Email Gateway (Feb 27 2025 at 06:30):

From: lacramioara <lacramioara.astefanoaei@gmail.com>
Hello,

Build/export_theory.scala contains a class Thm with deps as a
List[Thm_Name]. I wanted to use these deps to construct a call graph for an
arbitrary theory. This approach seemed to be inline with the one at
https://github.com/Dacit/afp-complex-networks/blob/main/source/graph/src/graph/edge_importer.scala#L173.

Say i have a theory DemoFib.thy (from codegen.pdf) and a basic ROOT
containing session "TestDemoFib" = HOL + theories Demo_Fib. I call isabelle build -o browser_info -b TestDemoFib after adding some prints in read_thms.
What puzzles me is that read_thms seems to fill in deps only for Pure, the
other theorems seem to be entities with an empty content. So my question is:
am i overlooking a build option which would lead to having non-empty deps for
theorems in a theory file?

Thank you,
Lacramioara

PS
Such a call graph could be used to update theory associated tex files with
uses clauses s.t. one can then generate blueprints like they do for Lean.
(If i understand correctly, the tex files corresponding to a Lean project are
manually written and with the help of uses, like
at https://github.com/fpvandoorn/carleson/blob/master/blueprint/src/chapter/main.tex#L299,
graphs
like https://florisvandoorn.com/carleson/blueprint/dep_graph_document.html can
be created.)

Email Gateway (Feb 27 2025 at 07:03):

From: Frédéric Blanqui <frederic.blanqui@inria.fr>
Hi. There is some code in
https://github.com/Deducteam/isabelle_dedukti/blob/master/src/rootfile.scala
to build the dependency graph of a session. This might be useful to you.

Le 27/02/2025 à 07:30, lacramioara a écrit :

Hello,

Build/export_theory.scala contains a class Thm with deps as a
List[Thm_Name]. I wanted to use these deps to construct a call graph for an
arbitrary theory. This approach seemed to be inline with the one at
https://github.com/Dacit/afp-complex-networks/blob/main/source/graph/src/graph/edge_importer.scala#L173.

Say i have a theory DemoFib.thy (from codegen.pdf) and a basic ROOT
containing session "TestDemoFib" = HOL + theories Demo_Fib. I call isabelle build -o browser_info -b TestDemoFib after adding some prints in read_thms.
What puzzles me is that read_thms seems to fill in deps only for Pure, the
other theorems seem to be entities with an empty content. So my question is:
am i overlooking a build option which would lead to having non-empty deps for
theorems in a theory file?

Thank you,
Lacramioara

PS
Such a call graph could be used to update theory associated tex files with
uses clauses s.t. one can then generate blueprints like they do for Lean.
(If i understand correctly, the tex files corresponding to a Lean project are
manually written and with the help of uses, like
at https://github.com/fpvandoorn/carleson/blob/master/blueprint/src/chapter/main.tex#L299,
graphs
like https://florisvandoorn.com/carleson/blueprint/dep_graph_document.html can
be created.)

--
Frédéric Blanqui
Research director at INRIA
Chair of EuroProofNet
https://blanqui.gitlabpages.inria.fr/

Email Gateway (Feb 27 2025 at 08:43):

From: Fabian Huch <huch@in.tum.de>

On 2/27/25 07:30, lacramioara wrote:

Hello,

Build/export_theory.scala contains a class Thm with deps as a
List[Thm_Name]. I wanted to use these deps to construct a call graph for an
arbitrary theory.
The name "Call graph" doesn't really make sense in this context, I would
say "dependency graph" or "formal entity graph".
This approach seemed to be inline with the one at
https://github.com/Dacit/afp-complex-networks/blob/main/source/graph/src/graph/edge_importer.scala#L173.

Say i have a theory DemoFib.thy (from codegen.pdf) and a basic ROOT
containing session "TestDemoFib" = HOL + theories Demo_Fib. I call isabelle build -o browser_info -b TestDemoFib after adding some prints in read_thms.
What puzzles me is that read_thms seems to fill in deps only for Pure, the
other theorems seem to be entities with an empty content. So my question is:
am i overlooking a build option which would lead to having non-empty deps for
theorems in a theory file?

Yes, you need to add "-o export_theory".

Fabian

Email Gateway (Feb 27 2025 at 17:58):

From: Lacramioara Astefanoaei <lacramioara.astefanoaei@gmail.com>
Thank you Fabian, indeed, i obtain what i want by adding -o export_theory. I think i 've seen "-o export_theory" mentioned in an
Isabelle-users response, i remember having looked it up in the docs and,
as i couldn't find it, i thought it should have been -e for
export_files and with -e i had the same output.

I wonder if it was worth it adding the option export_theory to
“system.pdf”. (It doesn’t seem to be documented, isabelle options -l -t build doesn’t show it and pdfgrep export_theory docs/*.pdf gives no
result).

Regarding your remark with respect to "call graphs", i used it more to
differentiate what i was looking for from the existing dependency graphs
generated at the level of theories. Indeed, i see the point you're making
if i think in terms of "the validity of a lemma depends on the validity of
another lemma". But theories contain function definitions as well. So i
indulge, still, in the thought that the terminology "call graph" can make
sense, at least under the proofs-as-programs paradigm.

On Thu, 27 Feb 2025 at 09:42, Fabian Huch <huch@in.tum.de> wrote:

On 2/27/25 07:30, lacramioara wrote:

Hello,

Build/export_theory.scala contains a class Thm with deps as a
List[Thm_Name]. I wanted to use these deps to construct a call graph
for an
arbitrary theory.
The name "Call graph" doesn't really make sense in this context, I would
say "dependency graph" or "formal entity graph".
This approach seemed to be inline with the one at

https://github.com/Dacit/afp-complex-networks/blob/main/source/graph/src/graph/edge_importer.scala#L173
.

Say i have a theory DemoFib.thy (from codegen.pdf) and a basic ROOT
containing session "TestDemoFib" = HOL + theories Demo_Fib. I call
isabelle build -o browser_info -b TestDemoFib after adding some prints in
read_thms.
What puzzles me is that read_thms seems to fill in deps only for
Pure, the
other theorems seem to be entities with an empty content. So my question
is:
am i overlooking a build option which would lead to having non-empty
deps for
theorems in a theory file?

Yes, you need to add "-o export_theory".

Fabian

Last updated: Mar 09 2025 at 12:28 UTC