Christian Urban (Feb 04 2022 at 14:36): 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
Mathias Fleury (Feb 04 2022 at 14:55):isabelle mkroot creates a skeleton
Mathias Fleury (Feb 04 2022 at 14:56):It even creates a root.tex file
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")
Mathias Fleury (Feb 04 2022 at 17:41):sessions cannot share directories
Last updated: Dec 21 2024 at 12:33 UTC