Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] update_thy

Email Gateway (Aug 18 2022 at 10:43):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
I've just obtained a recent development version of Isabelle, and find
that update_thy is missing.

Is this intentional? Is there something to use in its place? To exit
and restart Isabelle, and do use_thy, wastes a lot of time

Jeremy

Email Gateway (Aug 18 2022 at 10:43):

From: Makarius <makarius@sketis.net>
This is what the official Isabelle/NEWS file (of the current development
snapshot) says:

• Theory loader: be more serious about observing the static theory
  header specifications (including optional directories), but not the
  accidental file locations of previously successful loads. The strict
  update policy of former update_thy is now already performed by
  use_thy, so the former has been removed; use_thys updates several
  theories simultaneously, just as 'imports' within a theory header
  specification, but without merging the results. Potential
  INCOMPATIBILITY: may need to refine theory headers and commands
  ROOT.ML which depend on load order.

Anyway, neither use_thy nor former update_thy should occur in regular
interactive use of Isabelle at all: when processing a theory header
interactively, the system already updates all required theories. Invoking
use_thy (or its simultaneous version use_thys) mostly occurs in batch mode
ROOT.ML files, until we replace these by plain ROOT header specifications
using existing theory syntax.

Makarius

Last updated: May 03 2024 at 04:19 UTC