Stream: General

Topic: ROOT help


view this post on Zulip Christian Urban (Feb 04 2022 at 14:36):

Hi All

Can I ask for some help with ROOT files? I cannot find anything relevant and the system manual tells me to look at the code :o(

I have a formalisation and want to now add a separate theory for a paper. I want to generate a heapfile for the formalisation, such that whenever I make changes to the paper, I do not get the whole formalisation re-checked (since I did not make changes there). I understand this can be made work with a dedicated session for the formalisation in ROOT and another session that builds on top of this for the paper. Do you happen to have a skeleton ROOT file for setting up something like this?

Thanks a lot!!!
Christian

view this post on Zulip Mathias Fleury (Feb 04 2022 at 14:55):

isabelle mkroot creates a skeleton

view this post on Zulip Mathias Fleury (Feb 04 2022 at 14:56):

It even creates a root.tex file

view this post on Zulip Christian Urban (Feb 04 2022 at 16:21):

Thanks a lot! This gives indeed a skeleton ROOT file, but does not help with the setup of heap + another session building on this heap, I think. I hoped something like this would work

session Test = HOL +
theories[document = false]
A
B

session Paper = Test +
options [document = pdf, document_output = "output"]
theories
C
document_files
"root.tex"

but I clearly do not yet understand something, because it gives the error

*** Duplicate use of directory "/Users/cu/tmp/tmp"
*** for session "Test" (line 1 of "/Users/cu/tmp/tmp/ROOT")
*** vs. session "Paper" (line 7 of "/Users/cu/tmp/tmp/ROOT")

view this post on Zulip Mathias Fleury (Feb 04 2022 at 17:41):

sessions cannot share directories


Last updated: Dec 07 2023 at 08:19 UTC