Email Gateway (Jan 02 2021 at 08:23): Email Gateway (Jan 02 2021 at 08:23):From: Kawin Worrasangasilpa <kw448@cam.ac.uk>
Hi,
I am having a problem using Isabelle document preparation and curious if
this is common. One of the theories in this directory I want to create a
document for imports "HOL-Probability.Probability_Mass_Function". When I
used command isabelle build -D, there is a following error message:
[image: Screenshot 2021-01-02 at 08.12.53.png]
This is Root file:
session alltheories = HOL +
options [document = pdf, document_output = "output"]
theories [quick_and_dirty]
Forkable_Strings_Are_Rare
document_files
"root.tex"
I have checked on other theories that import other theories,
e.g., "~~/src/HOL/Library/Multiset", and the command works just fine.
Thank you,
Kawin
Screenshot 2021-01-02 at 08.12.53.png
Email Gateway (Jan 02 2021 at 10:04):From: Makarius <makarius@sketis.net>
On 02/01/2021 09:23, Kawin Worrasangasilpa wrote:
Hi,
I am having a problem using Isabelle document preparation and curious if this
is common. One of the theories in this directory I want to create a document
for imports "HOL-Probability.Probability_Mass_Function". When I used command
isabelle build -D, there is a following error message:Screenshot 2021-01-02 at 08.12.53.png
This is Root file:
session alltheories = HOL +
options [document = pdf, document_output = "output"]
theories [quick_and_dirty]
Forkable_Strings_Are_Rare
document_files
"root.tex"
Just try this before 'theories':
sessions "HOL-Probability"
I have checked on other theories that import other theories,
e.g., "~~/src/HOL/Library/Multiset", and the command works just fine.
You should not "steal" theory files from other sessions like that. The proper
way is to import "HOL-Library.Multiset" and ensure that the cumulative import
session graph contains "HOL-Library".
NB: Isabelle2018 (August 2018) is really old, Isabelle2020 (April 2020) is
current, and we are approaching Isabelle2021 (February 2021).
Makarius
Makarius
Last updated: Jan 04 2025 at 20:18 UTC