Stream: Isabelle/ML

Topic: ✔ Load ML files from other Sessions


view this post on Zulip Kevin Kappelmann (Dec 02 2021 at 16:45):

Is there a good/stable way to load ML files from another session (e.g. the AFP)?

view this post on Zulip Manuel Eberl (Dec 02 2021 at 16:48):

The only way I can think of is: make a theory file that includes it with ML_file. In the respective session. Then import that theory file in your session.

view this post on Zulip Kevin Kappelmann (Dec 02 2021 at 17:13):

I think I sadly can't do that: the ML file I want to load expects the existence of an ML structure of a certain name that I need to create in my session.

view this post on Zulip Kevin Kappelmann (Dec 02 2021 at 17:16):

To provide some background: I wanted to have my own auto2 instance but it loads a bunch of ML files that expect one custom ML structure created in the file auto2_HOL.ML in the AFP entry: https://www.isa-afp.org/browser_info/current/AFP/Auto2_HOL/Auto2_HOL.html
I do not know how I would load the next file util_logic.ML that depends on that structure once I created my replacement for auto2_HOL.ML.

view this post on Zulip Kevin Kappelmann (Dec 03 2021 at 22:04):

The "solution" was that I decided to bite the bullet and do the right thing: fix the setup of the AFP entry that I wanted to use.

view this post on Zulip Notification Bot (Dec 03 2021 at 22:04):

Kevin Kappelmann has marked this topic as resolved.


Last updated: Dec 07 2023 at 16:21 UTC