Email Gateway (Aug 22 2022 at 15:05): Email Gateway (Aug 22 2022 at 15:05):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hi,
I noticed that all dependencies show up on this page:
https://devel.isa-afp.org/browser_info/current/AFP/Parity_Game/index.html
This is not supposed to happen, but I don't see what I did wrong.
The ROOT file of Parity_Game is completely analogous to every other ROOT
file in the AFP, as far as I can tell:
chapter AFP
session Parity_Game (AFP) = HOL +
options [timeout = 600]
theories [document = false]
"../Coinductive/Coinductive_List"
"../Graph_Theory/Digraph_Isomorphism"
theories
PositionalDeterminacy
AttractorInductive
Graph_TheoryCompatibility
document_files
"root.tex"
"root.bib"
Why do the dependencies show up?
What can I do to fix this?
Thanks,
Christoph
Email Gateway (Aug 22 2022 at 15:05):From: Gerwin.Klein@data61.csiro.au
The HTML will always show all theories that were processed in the current session (it is not affected by the ‘document’ option). I’m not aware of a mechanism to suppress them. I.e. this is supposed to happen.
The only thing you could do is a parent session that contains the ones you don’t want to see - they will still show up in the HTML of that parent session, though, but at least there’d be some visual separation.
E.g.:
chapter AFP
session Parity_Game_Base (AFP) = HOL +
options [timeout = 600]
theories [document = false]
"../Coinductive/Coinductive_List"
"../Graph_Theory/Digraph_Isomorphism"
session Parity_Game (AFP) = Parity_Game_Base +
options [timeout = 600]
theories
PositionalDeterminacy
AttractorInductive
Graph_TheoryCompatibility
document_files
"root.tex"
“root.bib"
Cheers,
Gerwin
Last updated: Apr 25 2024 at 16:19 UTC