Re: [isabelle] [ExternalEmail] Unwanted dependency documents in AFP



In fact, if you are building on existing AFP entries, you should of course re-use their session images. You canât merge sessions, so we need to pick one, e.g.:

chapter AFP

session Parity_Game_Base (AFP) = Coinductive +
options [timeout = 600]
theories [document = false]
  "../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

> On 16.02.2017, at 10:21, gerwin.klein at data61.csiro.au wrote:
> 
> 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
> 
>> On 16.02.2017, at 03:33, Christoph Dittmann <f-isabellelist at yozora.eu> wrote:
>> 
>> 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
>> 
> 



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