Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Cannot load theory when building


view this post on Zulip 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

view this post on Zulip 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: Sep 25 2021 at 09:17 UTC