Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Theory loader: cannot update finished theory "...

view this post on Zulip Email Gateway (Aug 18 2022 at 09:43):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>

with_path "Integ" update_thy "Main";

Theory loader: cannot update finished theory "Main"

What does this message mean? Why, when I change a theory file, can I
sometimes do update_thy without problems, and sometimes not? When is a
theory "finished"?

Thanks for any help

Jeremy

view this post on Zulip Email Gateway (Aug 18 2022 at 09:44):

From: Makarius <makarius@sketis.net>
After finishing a session, i.e. when usedir has succefully compiled
everything. You can bootstrap HOL interactively like this:

- copy HOL/ROOT.ML to HOL/root.ML
- replace with_path "Integ" use_thy "Main";'' by add_path "Integ";''
- delete the subsequent lines
- start Isabelle Pure
- issue ``use "root.ML"''

Now you can assert arbitrary theories from the HOL sources.

Makarius

Last updated: May 03 2024 at 04:19 UTC