Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] loading ML files

Email Gateway (Aug 18 2022 at 11:13):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Using Isabelle2007 I find that, where I have files MSA.thy and MSA.ML,
use_thy "MSA" sometimes reloads them both and sometimes only reloads
MSA.thy.

What is meant to happen here?

Jeremy

Email Gateway (Aug 18 2022 at 11:13):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Jeremy,

the loading of a file FOO.ML after a theory FOO.thy is an ancient theory
loader feature. I don't what its actual semantics in Isabelle2007 is
supposed to be, but you can circumvent this incertainty by using
explicit dependencies:

theory Foo
imports ...
uses ("foo.ML")
begin

...

use "foo.ML"

end

Hope this helps
Florian
florian.haftmann.vcf
signature.asc

Email Gateway (Aug 18 2022 at 11:13):

From: Stefan Berghofer <berghofe@in.tum.de>
Jeremy Dawson wrote:
This is what the NEWS file says:

• Theory loader: old-style ML proof scripts being attached to a thy
  file (with the same base name as the theory) are considered a legacy
  feature, which will disappear eventually. Even now, the theory loader
  no longer maintains dependencies on such files.

Greetings,
Stefan

Email Gateway (Aug 18 2022 at 11:14):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Florian Haftmann wrote:
Florian,

Thanks, this seems OK. But if this is what I should be doing, then the
Isar Reference Manual, page 26, needs to be updated.

Regards,

Jeremy

Last updated: May 03 2024 at 12:27 UTC