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!!!
isabelle mkroot creates a skeleton
It even creates a root.tex file
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]
session Paper = Test +
options [document = pdf, document_output = "output"]
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")
sessions cannot share directories
Last updated: Dec 07 2023 at 08:19 UTC