Compiling a .thy file? · Beginner Questions

Importing theory files from the AFP can take a while since every dependency has to be proven. How do you compile a theory, like it is done for theory HOL for instance, so that it imports more quickly?

Wenda Li (Nov 30 2023 at 12:22):

On the right of your Isabelle/jEdit, there is a Theories tab, within which you can select a logic session to start with:
image.png
Select the target AFP entry and restart your Isabelle/jEdit.

David Wang (Nov 30 2023 at 12:34):

Wenda Li said:

On the right of your Isabelle/jEdit, there is a Theories tab, within which you can select a logic session to start with:
image.png
Select the target AFP entry and restart your Isabelle/jEdit.

image.png
Thank you. However, I cannot see any AFP entry in the dropdown. I know that the AFP has been imported, because theory files that depend on AFP entries are validated without issues. How do I add AFP entries there?

Wenda Li (Nov 30 2023 at 12:43):

Ahh, you need to have the AFP library properly installed first. See the instructions(i.e., via isabelle components -u).

David Wang (Nov 30 2023 at 12:59):

Wenda Li said:

Ahh, you need to have the AFP library properly installed first. See the instructions(i.e., via isabelle components -u).

~/bin/afp/afp-2023-11-28$ isabelle components -u thys/ Unchanged component "/home/david-wang/bin/afp/afp-2023-11-28/thys"

I did that before. Importing still takes ages.

image.png

Nothing seems to have changed.

David Wang (Nov 30 2023 at 13:01):

David Wang said:

Wenda Li said:

Ahh, you need to have the AFP library properly installed first. See the instructions(i.e., via isabelle components -u).

~/bin/afp/afp-2023-11-28$ isabelle components -u thys/ Unchanged component "/home/david-wang/bin/afp/afp-2023-11-28/thys"

I did that before. Importing still takes ages.

image.png

image.png

Nothing seems to have changed.

Never mind. I did not see the scroll bar. Thank you.

Lukas Stevens (Nov 30 2023 at 14:16):

At some point you probably should write a file named ROOT which would look something like:

session YOUR_SESSION = HOL +
  sessions
    "Propositional_Proof_Systems"
  theories
    YOUR_THEORY

and then you can launch Isabelle with isabelle jedit -d . -R YOUR_SESSION which instructs Isabelle to load the ROOT file from the current directory with -d . and tells it to prebuild all requirements of YOUR_SESSION with -R YOUR_SESSION which in this case just would be the session Propositional_Proof_Systems

Last updated: Apr 27 2024 at 12:25 UTC

Stream: Beginner Questions