Stream: Beginner Questions

Topic: Using the ISA AFP


view this post on Zulip Robert Soeldner (Aug 13 2021 at 13:29):

I would like to use some published theories from the AFP. After downloading and extracting the afp-current.tar.gz package, I tried importing them using isabelle components -u /home/rsoeldner/repo/afp-2021-08-08/thys/ which fails with *** Bad component directory: "/home/rsoeldner/repo/afp-2021-08-08". I'm using Isabelle Isabelle2021: February 2021

view this post on Zulip Katharina Kreuzer (Aug 13 2021 at 13:46):

I had a similar problem. Are you sure, the theorem files lie at /home/rsoeldner/repo/afp-2021-08-08/thys/? I think I needed to rename the folder so that it matches the exact description on the website. But I don't know why...

view this post on Zulip Robert Soeldner (Aug 13 2021 at 14:13):

Yes, should be the case :)

view this post on Zulip Katharina Kreuzer (Aug 13 2021 at 14:28):

Did you try isabelle components -u /home/rsoeldner/repo/afp-2021-08-08, ie without the /thys at the end?

view this post on Zulip Robert Soeldner (Aug 13 2021 at 14:35):

yes, same error.

view this post on Zulip Katharina Kreuzer (Aug 13 2021 at 14:37):

With and without the trailing /?

view this post on Zulip Robert Soeldner (Aug 13 2021 at 14:39):

Yes

view this post on Zulip Katharina Kreuzer (Aug 13 2021 at 14:44):

Oh, ok. isabelle components -u /home/kreuzer/afp worked for me, but if it doesn't for you, then I'm at the end of my wits.
Maybe have a look at https://isabelle.in.tum.de/dist/library/Doc/System/Misc.html, section Managing Isabelle components, if that can help you.
Anyone else has a suggestion?

view this post on Zulip Robert Soeldner (Aug 13 2021 at 14:45):

Thank you Katharina

view this post on Zulip Mathias Fleury (Aug 13 2021 at 15:01):

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-May/msg00055.html is related to your issue


Last updated: Aug 15 2022 at 04:16 UTC