CODEWITHSUNDEEP
isabelle
simonzack
simonzack

Reputation: 20938

Bad theory import in isabelle

The following gives bad theory import "Multivariate_Analysis"

imports Multivariate_Analysis

Importing Main works fine, how do I import modules?

Upvotes: 8

Views: 3261

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5108

For theory imports, you usually have to specify the full or relative path to the theory file. So for Multivariate_Analysis, this is <path to isabelle distrib>/src/HOL/Multivariate_Analysis/Multivariate_Analysis. The path may be only omitted if the theory is already part of the session image. So as Main is part of the default image HOL, you can import it without a path. Opinions diverge whether it is better to import theories from session images with or without paths.

The path may also contain environment variables like $ISABELLE_HOME or $AFP, which users can set in their local settings file such that the theories work across different installations. For everything from the Isabelle distribution, it is custom to use ~~ for the path of the Isabelle distribution folder.

In summary, your import should read as follows:

theory My_Theory
imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
begin

As Multivariate_Analysis is a fairly large module, it might be sensible to change the default session image, though, such that all these theories are not loaded at every start of Isabelle/jEdit afresh. You can do so by specifying -l HOL-Multivariate_Analysis at the command line upon invocation or by selecting this session in the theory panel and restarting Isabelle/jEdit.

Update: Since Isabelle2017, it is preferable to import theories from other sessions via session names instead of relative path names. That is, the theory Multivariate_Analysis would be imported as

theory My_Theory
imports "HOL-Multivariate_Analysis.Multivariate_Analysis"
begin

Upvotes: 12

Related Questions